Термины лямбда-исчисления, которые сводят к себе

13

В моем продолжающемся стремлении изучить лямбда-исчисление Хамдли и Селдин «Лямбда-исчисление и комбинаторы введение» упоминают следующую статью (Брюса Лерчера), которая доказывает, что единственное приводимое выражение, которое является одним и тем же (преобразование по модулю альфа) к себе является: (λx.xx)(λx.xx) .

Хотя я верю результату, я совсем не слежу за аргументом.

Это довольно короткий (менее одного абзаца). Любые объяснения будут приветствоваться.

Благодарность,

Чарли

Чарльз Рейх
источник

Ответы:

16

Во-первых, обратите внимание, что результат гласит, что единственный бета-пересчет, где правая часть равна (по модулю альфа-преобразованию) левой части, равен . Есть другие термины, которые сводятся к себе, имея этот переопределение в контексте.(λx.xx)(λx.xx)

Я могу видеть, как работает большинство доказательств Лерчера, хотя есть моменты, где я не могу пройти, не слегка изменив доказательство. Предположим, что (я использую = для альфа-эквивалентности), и согласно соглашению с переменными предположим, что x не встречается свободно в B(λx.A)B=[B/x]A=xB .

Подсчитайте количество в левой и правой части. Уменьшение удаляет один из Redex, а также тех , B , и добавляет столько , сколько есть в B раз число вхождений х в А . Другими словами, если L ( M ) - это число λ в M, а # x ( M ) - количество свободных вхождений x в M, то 1 + L ( B ) = # x (λBBxAL(M)λM#x(M)xM . Единственное решение этого диофантова уравнения - # x ( A ) = 2 L ( B ) = 1, но мы не будем использовать этот факт).1+L(B)=#x(A)×L(B)#x(A)=2L(B)=1

Я не понимаю аргументацию Леркера для параграфа выше. Он считает количество и атомных членов; давайте напишем это # ( M ) . Уравнение имеет вид # ( B ) + 1 = # x ( A ) × ( # ( B ) - 1 ) , который имеет два решения: # x ( A ) = 2 , # ( B ) = 3 и # x ( Aλ#(M)#(B)+1=#x(A)×(#(B)1)#x(A)=2,#(B)=3 . Я не вижу очевидного способа устранения второй возможности.#x(A)=3,#(B)=2

Теперь применим те же рассуждения к числу подтермов, равных с обеих сторон. Сокращение удаляет единицу около вершины и добавляет столько, сколько есть замещенных вхождений x в A , то есть 2. Следовательно, еще одно вхождение B должно исчезнуть; поскольку те, что в A, остаются (поскольку B не содержит свободного x ), дополнительное вхождение B в левой части должно быть λ x . .BxABABxBλx.A

Я не понимаю, как Лерчер делает вывод, что не имеет B в качестве подтерма, но на самом деле это не имеет отношения к доказательству.AB

Из исходной гипотезы является приложением. Этого не может быть, если A = x , поэтому само A является приложением M N с λ x . M N = [ ( λ x . M N ) / x ] M = [ ( λ x . M N ) / x ] N[(λx.A)/x]AA=xAMNλx.MN=[(λx.MN)/x]M=[(λx.MN)/x]N . Поскольку не может быть субтермом, MMM не может иметь форму , поэтому М = х . Аналогично, N = x .λx.PM=xN=x


Я предпочитаю доказательства без подсчета аргументов. Предположим, что (λx.A)B=[B/x]A .

If A=x then we have (λx.A)B=B, which is not possible since B cannot be a subterm of itself. Thus, since the right-hand side of the hypothesis is equal to an application, A must be an application A1A2, and λx.A=[B/x]A1 and B=[B/x]A2.

A1=xA1=λx.[B/x]AA1=λx.(λx.A1A2)B, which is not possible since $A_1 cannot be a subterm of itself.

From the latter equality, either A2=x or A2 has no free x (otherwise B would be a subterm of itself). In the latter case, A2=B.

We have shown that A=xx. The right-hand side of the initial hypothesis is thus BB, and B=λx.A = λx.xx.

Gilles 'SO- stop being evil'
источник