В лямбда - исчислении , то Церковь-Rosser теорема утверждает , что при применении правила сокращения в условия , порядок , в котором выбирается сокращения не делает разницы в конечный результат.
Точнее, если есть два различных сокращения или последовательности сокращений, которые могут быть применены к одному и тому же термину, тогда существует термин, достижимый из обоих результатов, путем применения (возможно, пустых) последовательностей дополнительных сокращений. [1] Теорема была доказана в 1936 году Алонзо Черчем и Дж. Баркли Россером , в честь которых она названа.
Теорема символизируется соседней диаграммой: если член a может быть сокращен как до b, так и c , тогда должен быть дополнительный член d (возможно, равный либо b, либо c ), к которому могут быть сведены как b, так и c . Просмотр лямбда - исчисление как абстрактной системы переписывания , церковь-Rosser теорема утверждает , что правила сокращения лямбда - исчисления вырожденная . Как следствие теоремы, термин в лямбда - исчислении имеет не более одной нормальной формы , оправдывая ссылку на " нормальная форма »данного нормализуемого члена.
История
В 1936 году Алонзо Черч и Дж. Баркли Россер доказали, что теорема верна для β-редукции в λI-исчислении (в котором каждая абстрактная переменная должна появляться в теле терма). Метод доказательства известен как «конечность развития», и он имеет дополнительные следствия, такие как теорема стандартизации, которая относится к методу, в котором сокращения могут выполняться слева направо для достижения нормальной формы (если таковая существует). Результат для чистого нетипизированного лямбда-исчисления был доказан Д. Е. Шроером в 1965 г. [2]
Чистое нетипизированное лямбда-исчисление
Одним из типов редукции в чистом нетипизированном лямбда-исчислении, к которому применима теорема Чёрча – Россера, является β-редукция, в которой подтерм вида сокращается заменой . Если обозначить β-редукцию через и его рефлексивное, транзитивное закрытие то теорема Черча – Россера такова: [3]
Следствием этого свойства является то, что два члена равны по должны быть сокращены до общего термина: [4]
Теорема применима также к η-редукции, в которой подтерм заменяется на . Это также относится к βη-редукции, объединению двух правил редукции.
Доказательство
Для β-редукции один метод доказательства исходит от Уильяма В. Тейта и Пера Мартин-Лёфа . [5] Скажите, что бинарное отношение удовлетворяет свойству алмаза, если:
Тогда свойство Черча – Россера - это утверждение, что удовлетворяет алмазному свойству. Мы вводим новое сокращение чье рефлексивное транзитивное замыкание и который удовлетворяет свойству алмаза. Таким образом, индукцией по числу шагов редукции следует, что удовлетворяет алмазному свойству.
Соотношение имеет правила формирования:
- Если а также тогда а также а также
Непосредственно можно доказать, что правило η-редукции является правилом Чёрча – Россера. Тогда можно доказать, что β-редукция и η-редукция коммутируют в том смысле, что: [6]
- Если а также тогда существует термин такой, что а также .
Отсюда можно заключить, что βη-редукция есть Чёрча – Россера. [7]
Нормализация
Правило редукции, удовлетворяющее свойству Черча – Россера, обладает тем свойством, что каждый член M может иметь не более одной отличной нормальной формы, а именно: если X и Y являются нормальными формами M, то по свойству Черча – Россера они оба сводятся к равный термин Z . Оба термина уже являются нормальными формами, поэтому. [4]
Если редукция является сильно нормализующей (нет бесконечных путей редукции), то слабая форма свойства Черча – Россера влечет полное свойство. Слабое свойство для отношения, это: [8]
- если а также тогда существует термин такой, что а также .
Варианты
Теорема Черча – Россера также верна для многих вариантов лямбда-исчисления, таких как лямбда-исчисление с простой типизацией , многих исчислений с расширенными системами типов и исчисления бета-значений Гордона Плоткина . Плоткин также использовал теорему Черча – Россера, чтобы доказать, что оценка функциональных программ (как для ленивого, так и для активного вычисления ) является функцией от программ к значениям ( подмножество лямбда-членов).
В более старых исследовательских работах система переписывания именуется Чёрч-Россер или имеет свойство Чёрча-Россера, когда она сливается .
Заметки
- ^ Алама (2017) .
- ^ Барендрегт (1984) , стр. 283.
- ^ Барендрегт (1984) , стр. 53–54.
- ↑ a b Barendregt (1984) , стр. 54.
- ^ Барендрегт (1984) , стр. 59-62.
- ^ Барендрегт (1984) , стр. 64–65.
- ^ Барендрегт (1984) , стр. 66.
- ^ Барендрегт (1984) , стр. 58.
Рекомендации
- Алама, Джесси (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. Опечатки .