Теорема Чёрча–Россера

Теорема в теоретической информатике

В лямбда-исчислении теорема Чёрча–Россера утверждает, что при применении правил редукции к термам порядок, в котором выбираются редукции, не влияет на конечный результат.

Точнее, если существуют две различные редукции или последовательности редукций, которые можно применить к одному и тому же термину, то существует термин, который достижим из обоих результатов путем применения (возможно, пустых) последовательностей дополнительных редукций. ^[1] Теорема была доказана в 1936 году Алонзо Чёрчем и Дж. Баркли Россером , в честь которых она и названа.

Теорема символизируется соседней диаграммой: Если термин a может быть сведен как к b, так и к c , то должен быть еще один термин d (возможно, равный либо b , либо c ), к которому могут быть сведены как b , так и c . Рассматривая лямбда-исчисление как абстрактную систему переписывания , теорема Чёрча–Россера утверждает, что правила редукции лямбда-исчисления являются конфлюэнтными . Как следствие теоремы, термин в лямбда-исчислении имеет не более одной нормальной формы , что оправдывает ссылку на « нормальную форму» данного нормализуемого термина.

История

В 1936 году Алонзо Чёрч и Дж. Баркли Россер доказали, что теорема справедлива для β-редукции в λI-исчислении (в котором каждая абстрагированная переменная должна появляться в теле термина). Метод доказательства известен как «конечность развёрток», и он имеет дополнительные следствия, такие как теорема о стандартизации, которая относится к методу, в котором редукции могут выполняться слева направо для достижения нормальной формы (если таковая существует). Результат для чистого нетипизированного лямбда-исчисления был доказан Д. Э. Шрёром в 1965 году. ^[2]

Чистое нетипизированное лямбда-исчисление

Одним из типов редукции в чистом нетипизированном лямбда-исчислении, для которого применима теорема Чёрча–Россера, является β-редукция, в которой подтерм формы сокращается посредством подстановки . Если β-редукция обозначается как , а её рефлексивное, транзитивное замыкание — как , то теорема Чёрча–Россера такова: ^[3] ${\displaystyle (\lambda x.t)s}$ ${\displaystyle t[x:=s]}$ ${\displaystyle \rightarrow _{\beta }}$ ${\displaystyle \twoheadrightarrow _{\beta }}$

${\displaystyle \forall M,N_{1},N_{2}\in \Lambda :{\text{if}}\ M\twoheadrightarrow _{\beta }N_{1}\ {\text{and}}\ M\twoheadrightarrow _{\beta }N_{2}\ {\text{then}}\ \exists X\in \Lambda :N_{1}\twoheadrightarrow _{\beta }X\ {\text{and}}\ N_{2}\twoheadrightarrow _{\beta }X}$

Следствием этого свойства является то, что два равных по , члена должны сводиться к общему члену: ^[4] ${\displaystyle \lambda \beta }$

${\displaystyle \forall M,N\in \Lambda :{\text{if}}\ \lambda \beta \vdash M=N\ {\text{then}}\ \exists X:M\twoheadrightarrow _{\beta }X\ {\text{and}}\ N\twoheadrightarrow _{\beta }X}$

Теорема применима также к η-редукции, в которой подтерм заменяется на . Она также применима к βη-редукции, объединению двух правил редукции. ${\displaystyle \lambda x.Sx}$ ${\displaystyle S}$

Доказательство

Для β-редукции один метод доказательства исходит от Уильяма В. Тейта и Пера Мартина-Лёфа . ^[5] Скажем, что бинарное отношение удовлетворяет свойству алмаза, если: ${\displaystyle \rightarrow }$

${\displaystyle \forall M,N_{1},N_{2}\in \Lambda :{\text{if}}\ M\rightarrow N_{1}\ {\text{and}}\ M\rightarrow N_{2}\ {\text{then}}\ \exists X\in \Lambda :N_{1}\rightarrow X\ {\text{and}}\ N_{2}\rightarrow X}$

Тогда свойство Чёрча–Россера является утверждением, которое удовлетворяет свойству алмаза. Мы вводим новую редукцию , рефлексивное транзитивное замыкание которой есть и которая удовлетворяет свойству алмаза. Индукцией по числу шагов в редукции, таким образом, следует, что удовлетворяет свойству алмаза. ${\displaystyle \twoheadrightarrow _{\beta }}$ ${\displaystyle \rightarrow _{\|}}$ ${\displaystyle \twoheadrightarrow _{\beta }}$ ${\displaystyle \twoheadrightarrow _{\beta }}$

Отношение имеет правила формирования: ${\displaystyle \rightarrow _{\|}}$

• ${\displaystyle M\rightarrow _{\|}M}$
• Если и то и и ${\displaystyle M\rightarrow _{\|}M'}$ ${\displaystyle N\rightarrow _{\|}N'}$ ${\displaystyle \lambda x.M\rightarrow _{\|}\lambda x.M'}$ ${\displaystyle MN\rightarrow _{\|}M'N'}$ ${\displaystyle (\lambda x.M)N\rightarrow _{\|}M'[x:=N']}$

Правило η-редукции можно доказать как правило Чёрча–Россера напрямую. Затем можно доказать, что β-редукция и η-редукция коммутируют в том смысле, что: ^[6]

Если и , то существует такой член , что и . ${\displaystyle M\rightarrow _{\beta }N_{1}}$ ${\displaystyle M\rightarrow _{\eta }N_{2}}$ ${\displaystyle X}$ ${\displaystyle N_{1}\rightarrow _{\eta }X}$ ${\displaystyle N_{2}\rightarrow _{\beta }X}$

Отсюда можно сделать вывод, что βη-редукция является редукцией Чёрча–Россера. ^[7]

Нормализация

Правило редукции, удовлетворяющее свойству Чёрча–Россера, обладает тем свойством, что каждый член M может иметь не более одной отличной нормальной формы, а именно: если X и Y являются нормальными формами M , то по свойству Чёрча–Россера они оба сводятся к одинаковому члену Z. Оба члена уже являются нормальными формами, поэтому . ^[4] ${\displaystyle X=Z=Y}$

Если редукция является строго нормализующей (нет бесконечных путей редукции), то слабая форма свойства Чёрча–Россера влечет полное свойство (см. лемму Ньюмана ). Слабое свойство для отношения имеет вид: ^[8] ${\displaystyle \rightarrow }$

${\displaystyle \forall M,N_{1},N_{2}\in \Lambda :}$если и то существует такой член , что и . ${\displaystyle M\rightarrow N_{1}}$ ${\displaystyle M\rightarrow N_{2}}$ ${\displaystyle X}$ ${\displaystyle N_{1}\twoheadrightarrow X}$ ${\displaystyle N_{2}\twoheadrightarrow X}$

Варианты

Теорема Чёрча–Россера также справедлива для многих вариантов лямбда-исчисления, таких как просто типизированное лямбда-исчисление , многие исчисления с расширенными системами типов и исчисление бета-значений Гордона Плоткина . Плоткин также использовал теорему Чёрча–Россера, чтобы доказать, что оценка функциональных программ (как для ленивой оценки, так и для энергичной оценки ) является функцией от программ к значениям ( подмножество лямбда-терминов).

В более старых исследовательских работах говорится, что система переписывания является системой Чёрча–Россера или имеет свойство Чёрча–Россера, когда она является конфлюэнтной .

Примечания

1. Алама (2017).
2. Барендрегт (1984), стр. 283.
3. Барендрегт (1984), с. 53–54.
4. Барендрегт (1984), с. 54.
5. Барендрегт (1984), с. 59-62.
6. Барендрегт (1984), с. 64–65.
7. Барендрегт (1984), стр. 66.
8. Барендрегт (1984), стр. 58.

Ссылки

• Alama, Jesse (2017). Zalta, Edward N. (ред.). The Stanford Encyclopedia of Philosophy (ред. осень 2017 г.). Исследовательская лаборатория метафизики, Стэнфордский университет.
• Чёрч, Алонзо ; Россер, Дж. Баркли (май 1936 г.), «Некоторые свойства преобразования» (PDF) , Труды Американского математического общества , 39 (3): 472–482, doi : 10.2307/1989762 , JSTOR  1989762.
• Барендрегт, Хендрик Питер (1984), Лямбда-исчисление: его синтаксис и семантика, Исследования по логике и основаниям математики, т. 103 (пересмотренное издание), Северная Голландия, Амстердам, ISBN 0-444-87508-5, архивировано из оригинала 2004-08-23. Опечатки.