4501
правка
Линеаризуемость: различия между версиями
Перейти к навигации
Перейти к поиску
м
→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 57: | Строка 57: | ||
Порядки <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_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> ложно. | ||
Продолжим доказательство от противного. Если наше предположение неверно, то существуют вызовы методов | Продолжим доказательство от противного. Если наше предположение неверно, то существуют вызовы методов <math>m_0, ..., m_n</math>, такие, что <math>m_0 \to m_1 \to \cdots \to m_n, m_n \to m_0</math>, и каждая пара непосредственно связана с некоторым <math>\to_x</math> или <math>\to_H</math>. | ||
Выберем цикл, длина которого минимальна. Предположим, что все вызовы метода связаны с одним и тем же объектом x. Поскольку | Выберем цикл, длина которого минимальна. Предположим, что все вызовы метода связаны с одним и тем же объектом x. Поскольку <math>\to_x</math> является полным порядком, должны существовать два вызова метода <math>m_{i-1}</math> и <math>m_i</math> такие, что <math>m_{i-1} \to_H m_i</math> и <math>m_i \to_x m_{i-1}</math>, что противоречит условию линеаризуемости x. | ||
Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за m1 и m2 вызовы методов разных объектов (переиндексировав их при необходимости). Пусть x – объект, связанный с m1. Ни один из m 2... m n не может быть вызовом метода x. Утверждение справедливо для m2 по построению. Пусть mi – первый вызов метода в m3; mn, связанный с x. Поскольку m,_i и mi не связаны по ! x, они должны быть связаны по ! H, поэтому ответ m,_i предшествует вызову mi. Вызов m2 предшествует ответу m,_i, поскольку в противном случае mi -1!H m2, что дает более короткий цикл m2 ■ ■ : ; m,_i. Наконец, ответ m1 предшествует вызову m2, поскольку m1 !H m2 по построению. Отсюда следует, что ответ на m1 предшествует вызову mi, следовательно, m1 !H mi, что дает более короткий цикл m\,mi,... , mn. | Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за m1 и m2 вызовы методов разных объектов (переиндексировав их при необходимости). Пусть x – объект, связанный с m1. Ни один из m 2... m n не может быть вызовом метода x. Утверждение справедливо для m2 по построению. Пусть mi – первый вызов метода в m3; mn, связанный с x. Поскольку m,_i и mi не связаны по ! x, они должны быть связаны по ! H, поэтому ответ m,_i предшествует вызову mi. Вызов m2 предшествует ответу m,_i, поскольку в противном случае mi -1!H m2, что дает более короткий цикл m2 ■ ■ : ; m,_i. Наконец, ответ m1 предшествует вызову m2, поскольку m1 !H m2 по построению. Отсюда следует, что ответ на m1 предшествует вызову mi, следовательно, m1 !H mi, что дает более короткий цикл m\,mi,... , mn. | ||