Линеаризуемость: различия между версиями

Перейти к навигации Перейти к поиску
Строка 46: Строка 46:
'''Свойство локальности'''
'''Свойство локальности'''


Свойство является локальным, если все объекты в совокупности удовлетворяют этому свойству при условии, что каждый отдельный объект удовлетворяет ему. Линеаризуемость локальна:
Свойство является ''локальным'', если все объекты в совокупности удовлетворяют этому свойству при условии, что каждый отдельный объект удовлетворяет ему. Линеаризуемость локальна:




'''Теорема 1. История H линеаризуема тогда и только тогда, когда H|x линеаризуема для любого объекта x.'''
'''Теорема 1. История H линеаризуема тогда и только тогда, когда H|x линеаризуема для каждого объекта x.'''


В части «только когда» доказательство является очевидным.
В части «только когда» доказательство является очевидным.


Для каждого объекта x выберем линеаризацию H|x. Пусть Rx – множество ответов, добавленных к H|x для построения этой линеаризации, и пусть !x – соответствующий порядок линеаризации. Обозначим за H0 историю, построенную путем добавления к Я каждого ответа в Rx.
Для каждого объекта x выберем линеаризацию H|x. Обозначим за <math>R_x</math> множество ответов, добавленных к H|x для построения этой линеаризации, а за <math>\to_x</math> – соответствующий порядок линеаризации. Обозначим за H' историю, построенную путем добавления к H каждого ответа в <math>R_x</math>.


Порядки ! H и !x могут быть «свернуты» в один частичный порядок. Определим отношение ! на вызовах методов из complete(H0): для вызовов методов m и m,m ! m, если существуют вызовы методов m0;::: mn, такие, что m = niQ,m = mn, и для каждого i между 0 и n - 1, либо mi !x mi+1 для некоторого объекта x, либо mi ! Hm i+1.
Порядки <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>.


Оказывается, что ! является частичным порядком. Очевидно, что ! транзитивен. Осталось показать, что ! антирефлексивен: для всех x утверждение x ! x ложно.
Оказывается, что <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.
Источник — http://pco.iis.nsk.su/wega/index.php/Линеаризуемость