Введение

В информатике, конфлюенс — это свойство систем переписывания, описывающее, какие термы в такой системе могут быть переписаны несколькими способами, приводящими к одному и тому же результату. В данной статье рассматриваются свойства в наиболее абстрактном контексте абстрактной системы переписывания.

Общий случай и теория

Система переписывания может быть выражена как ориентированный граф, в котором узлы представляют выражения, а рёбра – переписывания. Так, например, если выражение a может быть переписано в b, то говорят, что b является редукцией a (альтернативно, a редуцируется к b, или a является расширением b). Это представляется с помощью обозначения со стрелкой: a → b указывает, что a редуцируется к b. Интуитивно это означает, что соответствующий граф имеет ориентированное ребро от a к b. Если между двумя узлами c и d существует путь, то он образует последовательность редукций. Так, например, если c → c′ → c′′ → → d′ → d, то мы можем записать c d, указывая на существование последовательности редукций от c к d. Формально, является рефлексивно-транзитивным замыканием →. Используя пример из предыдущего абзаца, у нас есть (11+9)×(2+4) → 20×(2+4) и 20×(2+4) → 20×6, следовательно, (11+9)×(2+4) 20×6. При этом определении, конфлюэнтность можно определить следующим образом: a ∈ S считается конфлюэнтным, если для всех пар b, c ∈ S, таких, что a b и a c, существует d ∈ S с b d и c d (обозначается ). Если каждый a ∈ S является конфлюэнтным, то говорят, что → является конфлюэнтным. Это свойство также иногда называют свойством «алмаза», по форме диаграммы, показанной справа. Некоторые авторы резервируют термин «свойство алмаза» для варианта диаграммы с одношаговыми редукциями повсюду; то есть, если a → b и a → c, то должно существовать d такое, что b → d и c → d. Вариант с одношаговыми редукциями строго сильнее, чем вариант с многошаговыми редукциями.

Сухопутные слияния

Система переписывания терминов называется вполне сходящейся (ground confluent), если каждый основной термин сходится, то есть каждый термин, не содержащий переменных.

Местное слияние

[[Файл:Нециклическая локально, но не глобально конfluentная система переписывания. gif|thumb|Рис. 4: Бесконечная нециклическая, локально сходящаяся, но не глобально сходящаяся система переписывания, отсюда и название свойства. (Тот факт, что лямбда-исчисление обладает этим свойством, также известен как теорема Черча — Россера.) В системе переписывания, обладающей свойством Черча — Россера, задача о слове может быть сведена к поиску общего преемника. В системе Черча — Россера объект имеет не более одной нормальной формы; то есть, нормальная форма объекта уникальна, если она существует, но она может и не существовать. Например, в лямбда-исчислении выражение (λx. xx)(λx. xx) не имеет нормальной формы, поскольку существует бесконечная последовательность β-редукций: (λx. xx)(λx. xx) → (λx. xx)(λx. xx) → …

Система переписывания обладает свойством Черча — Россера тогда и только тогда, когда она является конfluentной. Из-за этой эквивалентности в литературе встречается значительное разнообразие в определениях. Например, в книге "Terese" свойство Черча — Россера и конfluentность определяются как синонимичные и идентичные определению конfluentности, представленному здесь; свойство Черча — Россера, как оно определено здесь, остаётся безымянным, но приводится как эквивалентное свойство; это отклонение от других текстов является преднамеренным.

Полуконфуенция

Определение локальной конфлюэнтности отличается от определения глобальной конфлюэнтности тем, что рассматриваются только элементы, достижимые из данного элемента за один шаг переписывания. Рассматривая один элемент, достижимый за один шаг, и другой элемент, достижимый произвольной последовательностью шагов, мы приходим к промежуточному понятию полуконфлюэнтности: элемент a ∈ S называется полуконфлюэнтным, если для всех b, c ∈ S, таких что a → b и a → c, существует d ∈ S, такой что b → d и c → d; если каждый элемент a ∈ S является полуконфлюэнтным, то говорят, что отношение → является полуконфлюэнтным. Полуконфлюэнтный элемент не обязательно должен быть конфлюэнтным, но полуконфлюэнтная система переписывания обязательно является конфлюэнтной, а конфлюэнтная система тривиально полуконфлюэнтна.

Сильное слияние

Сильное слияние — это еще одна разновидность локального слияния, позволяющая заключить, что система переписывания глобально слитна. Элемент a ∈ S называется сильно сходящимся, если для всех b, c ∈ S, таких что a → b и a → c, существует d ∈ S, для которого b → d и либо c → d, либо c = d; если каждый a ∈ S сильно сходящийся, то говорят, что → сильно слитна. Слитный элемент не обязательно должен быть сильно сходящимся, но сильно сходящаяся система переписывания обязательно является слитной.

Примеры слияний

Сокращение многочленов по модулю идеала является конфлюэнтной системой переписывания, если используется базис Грёбнера. Теорема Мацумото вытекает из конфлюэнтности соотношений кос. β-редукция λ-термов является конфлюэнтной согласно теореме Черча-Россера.