4501
правка
Линеаризуемость: различия между версиями
Перейти к навигации
Перейти к поиску
м
→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 46: | Строка 46: | ||
'''Свойство локальности''' | '''Свойство локальности''' | ||
Свойство является локальным, если все объекты в совокупности удовлетворяют этому свойству при условии, что каждый отдельный объект удовлетворяет ему. Линеаризуемость локальна: | Свойство является ''локальным'', если все объекты в совокупности удовлетворяют этому свойству при условии, что каждый отдельный объект удовлетворяет ему. Линеаризуемость локальна: | ||
'''Теорема 1. История H линеаризуема тогда и только тогда, когда H|x линеаризуема для | '''Теорема 1. История H линеаризуема тогда и только тогда, когда H|x линеаризуема для каждого объекта x.''' | ||
В части «только когда» доказательство является очевидным. | В части «только когда» доказательство является очевидным. | ||
Для каждого объекта x выберем линеаризацию H|x. | Для каждого объекта x выберем линеаризацию H|x. Обозначим за <math>R_x</math> множество ответов, добавленных к H|x для построения этой линеаризации, а за <math>\to_x</math> – соответствующий порядок линеаризации. Обозначим за H' историю, построенную путем добавления к H каждого ответа в <math>R_x</math>. | ||
Порядки | Порядки <math>\to_H</math> и <math>\to_x</math> могут быть «свернуты» в один частичный порядок. Определим отношение <math>\to</math> на вызовах методов из complete(H'): для вызовов методов <math>m</math> и <math>\bar{m}</math> выполняется <math>m \to \bar{m}</math>, если существуют вызовы методов <math>m_0, ..., m_n</math>, такие, что <math>m = m_0, \bar{m} = m_n</math>, и для каждого i между 0 и n - 1 имеет место либо <math>m_i \to_x m_{i+1}</math> для некоторого объекта x, либо <math>m_i \to_H m_{i+1}</math>. | ||
Оказывается, что | Оказывается, что <math>\to</math> является частичным порядком. Очевидно, что <math>\to</math> транзитивен. Осталось показать, что <math>\to</math> антирефлексивен: для всех x утверждение <math>x \to x</math> ложно. | ||
Продолжим доказательство от противного. Если наше предположение неверно, то существуют вызовы методов m0...: mn, такие, что m0 ! m1 ! - - - -> mn;mn ! m0, и каждая пара непосредственно связана с некоторым !x или ! H. | Продолжим доказательство от противного. Если наше предположение неверно, то существуют вызовы методов m0...: mn, такие, что m0 ! m1 ! - - - -> mn;mn ! m0, и каждая пара непосредственно связана с некоторым !x или ! H. | ||