1) redex 앞에 변수를 놓읍시다.

주어진 M에 대하여 i ∉ FV(M)일 때 M 안의 모든 redex R ≡ (λx. P) Q를 i ((λx. P) Q)로 바꾼 다음

i를 λ-추상화에 바운딩시킨 것을 N으로 두면 됩니다.


2) 각각을 다음과 같이 두면 됩니다.


    (λx. I I I x) (λx. I I I x) Ω;

    (λx. y) ((λx. I x) (λx. I x));

    (λx,y. x) x Ω;

    (λx,y. y (x x)) ω y.


3) Church-Rosser 정리를 이용합시다.

F ((true a) b) = true a이고 F ((false b) a) = false b이므로 λx. a = F a = λx. x인데

λx. a와 λx. x는 서로 다른 β-표준형이므로 모순이 생김을 알 수 있습니다.


4) 점- 0차원 큐브 -을 서브그래프로 가지는 것은 자명하므로 임의의 자연수 k에 대하여

k차원 큐브를 서브그래프로 가질 때 k + 1차원을 서브그래프로 가짐을 보이면 됩니다.

가장 왼쪽 redex를 축약하는 것을 n번 반복한 결과를 M_n이라 하면 다음과 같은 식을 얻습니다.


    M_0 ≡ A A x_0,

    M_(i + 1) ≡ (λx_i,z_i. z_i M_i) x_(i + 1), for 0 ≤ i ＜ n.


M_k가 k차원 큐브를 서브그래프로 가진다고 가정하면

M_k ⇒β X_1인 임의의 X_1과 M_k ⇒β X_2인 임의의 X_2에 대하여 4개의 항


    A ≡ (λx_k,z_k. z_k X_1) x_(k + 1),

    B ≡ (λx_k,z_k. z_k X_2) x_(k + 1),

    C ≡ λz_k. z_k X_1[x_k := x_(k + 1)],

    D ≡ λz_k. z_k X_2[x_k := x_(k + 1)]


은 서로 다른 항들이고 M_(k + 1)을 축약하여 얻을 수 있으므로

M_(k + 1)가 k + 1차원 큐브를 서브그래프로 가짐을 알 수 있습니다.


5-1) 임의의 β-표준형 P,Q에 대하여 두 명제


    (λx. P) Q ≡ P[x := Q],

    Q ≡ λx. P and P ≡ x x


가 서로 동치임을 보이면 됩니다.

(Q ≡ λx. P and P ≡ x x) ⇒ ((λx. P) Q ≡ P[x := Q])는 자명하니 그 역만 보입시다.

람다-항을 생성하는 문법을 상기해 보면 ∃z∈V. ∃M∈Λ. P ≡ λz. M은 거짓임을 알 수 있습니다.

그런데 P는 β-표준형이므로 P의 가장 왼쪽은 변수- 괄호는 지워도 됩니다 -입니다. 그 변수를 z라고 하면


    (λx. P) ≡ z[x := Q] or (λx. P) Q ≡ z[x := Q]


인데 후자는 모순되므로 z ≡ x이고 Q ≡ λx. P이어야 합니다.

Q는 β-표준형이므로 P ≡ x Z인 람다-항 Z가 존재함을 알 수 있습니다.

그러므로 P[x := Q] ≡ Q Q이기 때문에 Z[x := Q] ≡ Q이어야 합니다.

이때 x ∈ FV(Z)가 참인 경우와 거짓인 경우로 나눕시다.

Case1. 참인 경우:

    Z ≡ x이지 않으면 Z[x := Q]가 Q보다 길기 때문에 Z ≡ x입니다.

Case2. 거짓인 경우:

   Z ≡ Z[x := Q] ≡ Q이므로 (λx. x Q) Q ≡ Q Q이어야 하는데 이는 모순입니다.

따라서 Z ≡ x이므로 P ≡ x x이고 Q ≡ λx. x x입니다.


5-2) 길이가 3 이상인 β-경로가 존재함을 보이면 됩니다.

M은 3 개의 redex를 가지고 있으므로 다음을 만족하는 N이 존재합니다.


    M ≡ N[r1 := (λx1. P1) Q1][r2 := (λx2. P2) Q2][r3 := (λx3. P3) Q3].


그러므로 다음과 같은 소거가 존재합니다.

N[r1 := (λx1. P1) Q1][r2 := (λx2. P2) Q2][r3 := (λx3. P3) Q3]

→β N[r1 := (λx1. P1) Q1][r2 := (λx2. P2) Q2][r3 := P3[x3 := Q3]]

→β N[r1 := (λx1. P1) Q1][r2 := P2[x2 := Q2]][r3 := P3[x3 := Q3]]

→β N[r1 := P1[x1 := Q1]][r2 := P2[x2 := Q2]][r3 := P3[x3 := Q3]].

따라서 길이가 3 이상인 경로가 존재하지 않는 G[β](M)은 모순입니다.