Terminy Lambda-Calculus, które redukują się do siebie

W mojej ciągłej próbie nauki rachunku różniczkowego lambda, „Lambda-Calculus and Combinators an Introduction” Hindleya i Seldina wymienia następujący artykuł (autorstwa Bruce'a Lerchera), który dowodzi, że jedynym redukowalnym wyrażeniem jest to samo (konwersja modulo alfa) to: .$(\lambda x.xx)(\lambda x.xx)$

Chociaż wierzę w wynik, wcale nie podążam za argumentem.

Jest dość krótki (mniej niż jeden akapit). Wszelkie wyjaśnienia byłyby bardzo mile widziane.

Dzięki,

Charlie

Po pierwsze, zauważ, że wynik stwierdza, że ​​jedyny redex beta, w którym prawa strona jest równa (konwersja modulo alfa) do lewej strony to . Istnieją inne terminy, które ograniczają się do siebie, mając ten redex w kontekście.$(\lambda x. x x) (\lambda x. x x)$

Widzę, jak działa większość dowodu Lerchera, choć są punkty, w których nie mogę przejść bez nieznacznej modyfikacji dowodu. Załóżmy, że (użyć = alpha równoważności) i zgodnie z konwencją zmiennej przypuszczać, że x nie występują wolne w B .$(\lambda x. A) B = [B/x] A$$=$$x$$B$

Policz liczbę po lewej i prawej stronie. Zmniejszenie usuwa jedną z Redex, a także tych z B i dodaje tyle, ile jest w B czasach liczba wystąpień x w A . Innymi słowy, jeśli L ( M ) jest liczbą λ w M, a # x ( M ) jest liczbą wolnych wystąpień x w M, to 1 + L ( B ) = # x$\lambda$$B$$B$$x$$A$$L(M)$$\lambda$$M$$\#_x(M)$$x$$M$ . Jedynym rozwiązaniem tego równania diofantycznego jest # x ( A ) = 2 (i L ( B ) = 1, ale nie wykorzystamy tego faktu).$1 + L(B) = \#_x(A) \times L(B)$$\#_x(A) = 2$$L(B)=1$

Nie rozumiem argumentu Lerchera dla powyższego akapitu. Liczy liczbę atomów i atomowych; napiszmy to # ( M ) . Równanie to # ( B ) + 1 = # x ( A ) × ( # ( B ) - 1 ) , który ma dwa rozwiązania: # x ( A ) = 2 , # ( B ) = 3 i # x ( $\lambda$$\#(M)$$\#(B) + 1 = \#_x(A) \times (\#(B) - 1)$$\#_x(A)=2, \#(B)=3$ . Nie widzę oczywistego sposobu na wyeliminowanie drugiej możliwości.$\#_x(A)=3, \#(B)=2$

Zastosujmy teraz to samo rozumowanie do liczby podwładności równej po obu stronach. Redukcja usuwa jeden u góry i dodaje tyle, ile jest podstawionych wystąpień x w A , tj. 2. Stąd jeszcze jedno wystąpienie B musi zniknąć; ponieważ te w A pozostają (ponieważ B nie zawiera wolnego x ), dodatkowe wystąpienie B po lewej stronie musi wynosić λ x . .$B$$x$$A$$B$$A$$B$$x$$B$$\lambda x. A$

Nie rozumiem, w jaki sposób Lercher wywnioskuje, że nie ma B jako podterminu, ale w rzeczywistości nie ma to znaczenia dla dowodu.$A$$B$

$[(\lambda x. A)/x] A$$A = x$$A$$M N$$\lambda x.M N = [(\lambda x. M N)/x] M = [(\lambda x. M N)/x] N$$M$$M$$\lambda x.P$$M = x$$N = x$

$(\lambda x. A) B = [B/x] A$

$A = x$$(\lambda x. A) B = B$$B$$A$$A_1 A_2$$\lambda x. A = [B/x] A_1$$B = [B/x] A_2$

$A_1 = x$$A_1 = \lambda x. [B/x] A$$A_1 = \lambda x. (\lambda x. A_1 A_2) B$

$A_2 = x$$A_2$$x$$B$$A_2 = B$

$A = x x$$B B$$B = \lambda x. A$$\lambda x. x x$