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

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

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

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

История [ править ]

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

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

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

\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

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

\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

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

Доказательство [ править ]

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

\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

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

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

$M\rightarrow _{\|}M$
Если $M\rightarrow _{\|}M'$ и $N\rightarrow _{\|}N'$ затем $\lambda x.M\rightarrow _{\|}\lambda x.M'$ и $MN\rightarrow _{\|}M'N'$ и $(\lambda x.M)N\rightarrow _{\|}M'[x:=N']$

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

Если

M\rightarrow _{\beta }N_{1}

и

M\rightarrow _{\eta }N_{2}

тогда существует термин

X

такой, что

N_{1}\rightarrow _{\eta }X

и

N_{2}\rightarrow _{\beta }X

.

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

Нормализация [ править ]

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

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

\forall M,N_{1},N_{2}\in \Lambda :

если

M\rightarrow N_{1}

и

M\rightarrow N_{2}

тогда существует термин

X

такой, что

N_{1}\twoheadrightarrow X

и

N_{2}\twoheadrightarrow X

.

Варианты [ править ]

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

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

Примечания [ править ]

^ Марк (2017) .
^ Барендрегт (1984) , с. 283.
^ Барендрегт (1984) , с. 53–54.
↑ Перейти обратно: Перейти обратно: ^а ^б Барендрегт (1984) , с. 54.
^ Барендрегт (1984) , с. 59-62.
^ Барендрегт (1984) , с. 64–65.
^ Барендрегт (1984) , с. 66.
^ Барендрегт (1984) , с. 58.

Ссылки [ править ]

Алама, Джесси (2017). Залта, Эдвард Н. (ред.). Стэнфордская энциклопедия философии (изд. осени 2017 г.). Лаборатория метафизических исследований Стэнфордского университета.
Церковь, Алонсо ; Россер, Дж. Баркли (май 1936 г.), «Некоторые свойства преобразования» (PDF) , Transactions of the American Mathematical Society , 39 (3): 472–482, doi : 10.2307/1989762 , JSTOR 1989762 .
Барендрегт, Хендрик Питер (1984), Лямбда-исчисление: его синтаксис и семантика , Исследования по логике и основам математики, том. 103 (пересмотренная редакция), Северная Голландия, Амстердам, ISBN 0-444-87508-5 , заархивировано из оригинала 23 августа 2004 г. Ошибка .

[FOOTNOTEAlama2017-1] Марк (2017) .

[FOOTNOTEBarendregt1984283-2] Барендрегт (1984) , с. 283.

[FOOTNOTEBarendregt198453–54-3] Барендрегт (1984) , с. 53–54.

[FOOTNOTEBarendregt198454-4] Перейти обратно: Перейти обратно: ^а ^б Барендрегт (1984) , с. 54.

[FOOTNOTEBarendregt198459-62-5] Барендрегт (1984) , с. 59-62.

[FOOTNOTEBarendregt198464–65-6] Барендрегт (1984) , с. 64–65.

[FOOTNOTEBarendregt198466-7] Барендрегт (1984) , с. 66.

[FOOTNOTEBarendregt198458-8] Барендрегт (1984) , с. 58.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]