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

В лямбда - исчислении , то Церковь-Rosser теорема утверждает , что при применении правила сокращения в условия , порядок , в котором выбирается сокращения не делает разницы в конечный результат.

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

Эта теорема символизируется соседней диаграммой: если член a может быть сокращен как до b, так и c , тогда должен быть еще один член d (возможно, равный либо b, либо c ), к которому могут быть сведены как b, так и c . Просмотр лямбда - исчисление как абстрактной системы переписывания , церковь-Rosser теорема утверждает , что правила сокращения лямбда - исчисления вырожденная . Как следствие теоремы, термин в лямбда - исчислении имеет не более одной нормальной формы , оправдывая ссылку на " нормальная форма »данного нормализуемого члена.

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

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

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

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

${\displaystyle \forall M,N_{1},N_{2}\in \Lambda :{\text{if}}\ M\rightarrow _{\beta }N_{1}\ {\text{and}}\ M\rightarrow _{\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 Z=X=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}\rightarrow X}$${\displaystyle N_{2}\rightarrow X}$

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

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

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

Заметки [ править ]

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

• Алама, Джесси (2017). Залта, Эдвард Н. (ред.). Стэнфордская энциклопедия философии (издание осень 2017 г.). Лаборатория метафизических исследований Стэнфордского университета.
• Церковь, Алонсо ; Rosser, J. Баркли (май 1936), "Некоторые свойства преобразования" (PDF) , Труды Американского математического общества , 39 (3): 472-482, DOI : 10,2307 / 1989762 , JSTOR  1989762.
• Барендрегт, Хендрик Питер (1984), Лямбда-исчисление: его синтаксис и семантика , Исследования в области логики и основ математики, 103 (пересмотренное издание), Северная Голландия, Амстердам, ISBN 0-444-87508-5, Архивируются с оригинала на 2004-08-23 CS1 maint: discouraged parameter (link). Опечатки .