4551
правка
Линеаризуемость: различия между версиями
Перейти к навигации
Перейти к поиску
м
→Основные результаты
Irina (обсуждение | вклад) м (→Нотация) |
Irina (обсуждение | вклад) |
||
| Строка 55: | Строка 55: | ||
Для каждого объекта x выберем линеаризацию H|x. Обозначим за <math>R_x</math> множество ответов, добавленных к H|x для построения этой линеаризации, а за <math>\to_x</math> – соответствующий порядок линеаризации. Обозначим за H' историю, построенную путем добавления к H каждого ответа в <math>R_x</math>. | Для каждого объекта 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_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>\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. Поскольку <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. | Выберем цикл, длина которого минимальна. Предположим, что все вызовы метода связаны с одним и тем же объектом 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. | ||
Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за <math>m_1</math> и <math>m_2</math> вызовы методов разных объектов (переиндексировав их при необходимости). Пусть x – объект, связанный с <math>m_1</math>. Ни один из <math>m_2, ..., m_n</math> не может быть вызовом метода x. Утверждение справедливо для <math>m_2</math> по построению. Пусть <math>m_i</math> – первый вызов метода в <math>m_3, ..., m_n</math>, связанный с x. Поскольку <math>m_{i-1}</math> и <math>m_i</math> не связаны по <math>\to_x</math>, они должны быть связаны по <math>\to_H</math>, поэтому ответ <math>m_{i-1}</math> предшествует | Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за <math>m_1</math> и <math>m_2</math> вызовы методов разных объектов (переиндексировав их при необходимости). Пусть x – объект, связанный с <math>m_1</math>. Ни один из <math>m_2, ..., m_n</math> не может быть вызовом метода x. Утверждение справедливо для <math>m_2</math> по построению. Пусть <math>m_i</math> – первый вызов метода в <math>m_3, ..., m_n</math>, связанный с x. Поскольку <math>m_{i-1}</math> и <math>m_i</math> не связаны по <math>\to_x</math>, они должны быть связаны по <math>\to_H</math>, поэтому ответ <math>m_{i-1}</math> предшествует обращению к <math>m_i</math>. Обращение к <math>m_2</math> предшествует ответу <math>m_{i-1}</math>, поскольку в противном случае имело бы место <math>m_{i-1} \to_H m_2</math>, что дает более короткий цикл <math>m_2, ..., m_{i-1}</math>. Наконец, ответ <math>m_1</math> предшествует обращению к <math>m_i</math>, поскольку по построению <math>m_1 \to_H m_2</math>. Отсюда следует, что ответ на <math>m_1</math> предшествует обращению к <math>m_i</math>, следовательно, <math>m_1 \to_H m_i</math>, что дает более короткий цикл <math>m_1, m_i, ..., m_n</math>. | ||
Поскольку <math>m_n</math> не является вызовом метода x, а <math>m_n \to m_1</math>, из этого следует, что <math>m_n \to_H m_1</math>. Но <math>m_1 \to_H m_2</math> по построению, а так как <math>\to_H</math> транзитивно, то <math>m_n \to_H m_2</math>, что дает более короткий цикл <math>m_2, ..., m_n</math>, так что имеет место противоречие. <math>\square</math> | Поскольку <math>m_n</math> не является вызовом метода x, а <math>m_n \to m_1</math>, из этого следует, что <math>m_n \to_H m_1</math>. Но <math>m_1 \to_H m_2</math> по построению, а так как <math>\to_H</math> транзитивно, то <math>m_n \to_H m_2</math>, что дает более короткий цикл <math>m_2, ..., m_n</math>, так что имеет место противоречие. <math>\square</math> | ||