Теорема Черча – Россера - Church–Rosser theorem

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

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

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

История

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

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

Одним из типов редукции в чистом нетипизированном лямбда-исчислении, к которому применима теорема Черча – Россера, является β-редукция, в которой подтерм формы сжимается подстановкой . Если β-редукция обозначается через, а ее рефлексивное транзитивное замыкание - через, то теорема Черча – Россера такова: ${\ 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}$

Следствием этого свойства является то, что два равных члена должны сводиться к общему члену: ${\ 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 {и}} \ N \ twoheadrightarrow _ {\ beta} X}$

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

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

Для β-редукции один метод доказательства исходит от Уильяма В. Тейта и Пера Мартин-Лёфа . Скажите, что бинарное отношение удовлетворяет свойству ромба, если: ${\ 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 М \ rightarrow _ {\ |} М '}$${\ Displaystyle N \ rightarrow _ {\ |} N '}$${\ displaystyle \ lambda xM \ rightarrow _ {\ |} \ lambda x.M '}$${\ displaystyle MN \ rightarrow _ {\ |} M'N '}$${\ displaystyle (\ lambda xM) N \ rightarrow _ {\ |} M '[x: = N']}$

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

Если и тогда существует такой термин , что и . ${\ 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}$

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

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

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

Если редукция является сильно нормализующей (нет бесконечных путей редукции), то слабая форма свойства Черча – Россера влечет полное свойство. Слабым свойством отношения является: ${\ 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: обескураженный параметр ( ссылка ) . Опечатки .