Chapter 4. Reduction: β-소거는 비대칭적입니다. (λx. x^2 + 1) 3은 10으로 축약될 수 있지만 그 반대는 아닙니다.


> 이 장에서 자주 쓰이는 증명법 중 하나는 수학적 귀납법을 일반화한 structural induction입니다.

기본 생성 규칙들과 재귀 생성 규칙들에 의해 발생되는 구조 S의 인스턴스 i에 대한 명제 P(i)에 대하여,

기본 생성 규칙에 생성되는 임의의 인스턴스 b에 대해 P(b)가 항상 참임을 보이고

임의의 p항의 재귀 생성 규칙 r과 임의의 인스턴스 i_1, ..., i_p에 대하여

P(i_1), ..., P(i_p)가 참임을 가정할 때 P(r(i_1, ..., i_p))도 참임을 보이면

S의 모든 인스턴스 i에 대하여 P(i)가 성립함을 알 수 있습니다.


1. 정의: 이항관계(binary relation)


    1) Λ에 대한 이항관계 R은 다음과 같을 때 연산과 "양립가능"하다고 합니다.


        (M R N) ⇒ ((Z M) R (Z N)) and ((M Z) R (N Z)) and ((λx. M) R (λx. N)).


    2) Λ에 대한 congruence 관계는 양립가능한 동치관계(equivalence relation)입니다.


    3) Λ에 대한 reduction 관계는 양립가능하고 reflexive하고 transitive한 관계입니다.


2. 정의: Λ에 대한 이항관계 →β, ⇒β, =β는 다음과 같이 귀납적으로 정의됩니다.

→β는 양립가능하고, ⇒β는 reduction 관계이고, =β는 congruence 관계입니다.


    i) M →β N: M이 한 단계만에 N으로 β-소거된다.


        1) (λx. M) N →β M[x := N];

        2) (M →β N) ⇒ ((Z M) →β (Z N)) and ((M Z) →β (N Z)) and ((λx. M) →β (λx. N)).


    ii) M ⇒β N: M이 N으로 β-소거된다.


        1) M ⇒β M;

        2) (M →β N) ⇒ (M ⇒β N);

        3) (M ⇒β N) and (N ⇒β L) ⇒ (M ⇒β L).


    ) M =β N: M은 N으로 β-변환될 수 있다.


        1) (M ⇒β N) ⇒ (M =β N);

        2) (M =β N) ⇒ (N =β M);

        3) (M =β N) and (N =β L) ⇒ (M =β L).


3. 예제: ω ≡ λx. x x, Ω ≡ ω ω이라 하면

    1) Ω →β Ω.

    2) K I Ω →β I.


> 직관적으로 M이 N과 β-화살표를 통해 연결되어 있을 때 그리고 그럴 때에만 M =β N입니다.


4. 예제: K I Ω =β I I. 왜냐하면 K I Ω →β (y. I) Ω →β I이고 I I →β I이기 때문입니다.


5. 명제: M =β N ⟺ λ⊢ M = N.


    증명) 구조에 대한 귀납법으로.


6. 정의: β-표준형(β-nf).


    1) β-redex는 (λx. M) N 꼴의 항이고 M[x := N]은 그것의 contractum입니다.


    2) 하위항으로 β-redex를 가지지 않는 람다-항을 β-표준형이라고 합니다.


    3) M =β N인 β-표준형 N이 존재한다면 M은 β-표준형을 가진다고 합니다.


7. 예제: (λx. x x) y는 β-표준형이 아니지만 y y를 β-표준형으로 가집니다.


8. 보조정리: 임의의 β-표준형 M에 대하여 (M ⇒β N) ⇒ (N ≡ M)입니다.


9. Church-Rosser 정리: M ⇒β N_1이고 M ⇒β N_2이면 L가 항상 존재하여 N_1 ⇒β L이고 N_2 ⇒β L입니다.


10. 따름정리: M =β N인 N이면 L이 존재하여 M ⇒β L이고 N ⇒β L입니다.


    증명) M =β N을 나타내는 β-화살표 경로가 주어지면 반복적으로 Church-Rosser 정리를 적용하여

    공통 reduct L을 얻을 수 있습니다. =β의 정의에 대하여 경우를 나누어 귀납적으로 증명합시다.

    Case1. M ⇒β N이어서 M =β N인 경우:

        L ≡ N인 N이 존재하므로 성립합니다.

    Case2. N =β M이어서 M =β N인 경우:

        가정에 의하여 N과 M의 공통 β-reduct L1이 존재하므로 L ≡ L1을 택합시다.

    Case3. M =β N'이고 N' =β N이어서 M =β N인 경우:

        가정에 의하여 M ⇒β L1이고 N' ⇒β L1인 L1과 N' ⇒β L2이고 N ⇒β L2인 L2가 존재합니다.

        이때 Church-Rosser 정리에 의하여 L1 ⇒β L이고 L2 ⇒β L인 L이 존재하여 M ⇒β L이고 N ⇒β L입니다.


11. 따름정리: β-표준형을 가짐에 대하여


    1) M이 N을 β-표준형으로 가진다면 M ⇒β N입니다.


    증명) β-표준형 N에 대하여 M =β N이라고 가정합시다.

    그러면 따름정리 10에 의하여 M ⇒β L이고 N ⇒β L인 L이 존재합니다.

    하지만 보조정리 8에 의하여 N ≡ L이므로 M ⇒β N입니다.


    2) 모든 람다-항은 많아야 한 개의 β-표준형을 가집니다.


    증명) M이 N1, N2를 β-표준형으로 갖는다면 N1 =β M =β N2입니다.

    그러면 따름정리 10에 의하여 N1 ⇒β L이고 N2 ⇒β L입니다.

    하지만 보조정리 8에 의하여 N1 ≡ L ≡ N2입니다.


12. 어떤 결과들:


    1) λ-calculus는 일관성이 있습니다. 예를 들어 λ⊬ true = false입니다. 그렇지 않다면 명제 5에 의하여

    true =β false이어야 하는데 둘은 서로 다른 β-표준형이므로 따름정리 11에 의하여 불가능합니다.


    2) Ω는 β-표준형 가지지 않습니다. 그렇지 않다면 β-표준형 N이 존재하여 Ω ⇒β N인데

    Ω는 자기 자신으로만 소거되며 β-표준형이 아니기 때문에 불가능합니다.


> Church-Rosser 정리를 증명하기 위해 조각 보조정리(strip lemma)


        (M →β N1) and (M ⇒β N2) ⇒ (∃N3. (N1 ⇒β N3) and (N2 ⇒β N3)), for all M,N1,N2∈Λ


를 보입시다. 이 보조정리를 증명하기 위해 M →β N을 M 안의 redex R을 N1 안의 R의 contractum R'로

바꾸는 결과를 낳는 한 단계 소거라고 합시다. 소거 M ⇒β N2 중에 R에게 무슨 일이 생기는 지의

bookkeeping을 만든다면 N2 안의 R의 모든 잔여를 소거함으로서 N3를 찾을 수 있습니다.

이 필수적인 bookkeeping을 하기 위해서 Λ에서 확장된 집합 Λ과 소거 β를 도입합시다.


13. 정의 밑줄 긋기는 추적 동위원소(tracing isotope)로서 일합니다.


    1) Λ는 다음과 같이 귀납적으로 정의된 항들의 집합입니다.


        x ∈ V ⇒ x ∈ Λ,

        M, N ∈ Λ ⇒ (M N) ∈ Λ,

        M ∈ Λ, x ∈ V ⇒ (λx. M) ∈ Λ,

        M, N ∈ Λ, x ∈ V ⇒ ((λx. M) N) ∈ Λ.


    2) 밑줄 소거 관계 →β(한 단계)와 ⇒β는 축약 규칙


        (λx. M) N →β M[x := N],

        (λx. M) N →β M[x := N]


    으로 정의되기 시작합니다. 그러면 →β는 λ-추상화의 관점에서도 양립가능하기 위해 확장됩니다.

    추가로 ⇒β는 transitive하고 reflexive한 closure입니다.


    3) 모든 M ∈ Λ에 대하여 |M|은 M에서 모든 밑줄을 없앤 것입니다.


14. 정의: 사상 φ:Λ→Λ은 밑줄 쳐진 모든 redex들을 안쪽에서 바깥쪽으로 축약해 갑니다.


        φ(x) ≡ x,

        φ(M N) ≡ φ(M) φ(N),

        φ(λx. M) ≡ λx. φ(M),

        φ((λx. M) N) ≡ φ(M)[x := φ(N)].


15. 보조정리: M', N' ∈ Λ와 M, N ∈ Λ에 대하여 |M'| ≡ M이고 |N'| ≡ N이고 M ⇒β N이면 M ⇒β N입니다.


        증명) M →β N일 때 성립함을 보이면 transitivity에 의하여 증명됩니다.

        M →β N이면 N을 M 안의 redex 하나를 축약하여 얻고,

        N'를 M' 안의 대응하는 redex를 축약하여 얻을 수 있습니다.


16. 보조정리: 사상 φ에 관하여


    1) M, N ∈ Λ이면 φ(M[x := N]) ≡ φ(M)[x := φ(N)]입니다.


    증명) 치환 보조정리


        x ≢ y and x ∉ FV(L) ⇒ M[x := N][y := L] ≡ M[y := L][x := N[y := L]]


    를 M ≡ (λy. P) Q인 경우에 적용하면서, M의 구조에 대하여 귀납법을 적용해 봅시다.

    Case1. M ≡ x인 경우:

       LHS ≡ φ(N)이고 RHS ≡ x[x := φ(N)] ≡ φ(N)이므로 성립합니다.

    Case2. M ≡ y인 경우 - 단, x ≢ y:

        LHS ≡ φ(y) ≡ y이고 RHS ≡ y[x := φ(N)] ≡ y이므로 성립합니다.

    Case3. M ≡ L L'인 경우:

        LHS

        ≡ φ(L[x := N] L'[x := N])

        ≡ φ(L[x := N]) φ(L'[x := N])

        ≡ φ(L)[x := φ(N)] φ(L')[x := φ(N)] /* 가정에 의하여 */

        ≡ (φ(L) φ(L'))[x := φ(N)]

        ≡ φ(L L')[x := φ(N)]

        ≡ RHS.

    Case4. M ≡ (λy. L)인 경우 - 단, x ≢ y:

        LHS

        ≡ φ(λy. L[x := N])

        ≡ λy. φ(L[x := N])

        ≡ λy. φ(L)[x := N] /* 가정에 의하여 */

        ≡ (λy. φ(L))[x := φ(N)]

        ≡ RHS.

    Case5. M ≡ (λy. P) Q인 경우 - 단, x ≢ y:

        LHS

        ≡ φ((λy. P[x := N]) Q[x := N])

        ≡ φ(P[x := N] [y := Q[x := N]])

        ≡ φ(P[y := Q][x := N]) /* 치환 보조정리에 의하여 */

        ≡ φ(P)[y := φ(Q)][x := φ(N)] /* 가정에 의하여 */

        ≡ φ((λy. P) Q)[x := φ(N)]

        ≡ RHS.


    2) M ⇒β N이면 φ(M) ⇒β φ(N)입니다.


    증명) 1)을 이용하여 M →β N일 때 φ(M) ⇒β φ(N)임을 보이면 transitivity에 의하여 증명됩니다.

    Case1. M ≡ (λx. P) Q이고 N ≡ P[x := Q]인 경우:

        φ(M)

        ≡ (λx. φ(P)) φ(Q)

        →β φ(P)[x := φ(Q)]

        ≡ φ(P[x := φ(Q)])

        ≡ φ(N).

    Case2. M ≡ (λx. P) Q이고 N ≡ P[x := Q]인 경우:

        φ(M)

        ≡ φ((λx. P) Q)

        ≡ φ(P)[x := φ(Q)]

        ≡ φ(P[x := φ(Q)]) /* 1)에 의하여 */

        ≡ φ(N).

    Case3. M ≡ Z L이고 N ≡ Z L'이고 L →β L'이어서 M →β N인 경우:

        φ(M)

        ≡ φ(Z) φ(L)

        ⇒β φ(Z) φ(L') /* 가정에 의하여 */

        ≡ φ(N).

    Case4. M ≡ L Z이고 N ≡ L' Z이고 L →β L'이어서 M →β N인 경우:

        φ(M)

        ≡ φ(L) φ(Z)

        ⇒β φ(L') φ(Z) /* 가정에 의하여 */

        ≡ φ(N).

    Case5. M ≡ λx. L이고 M ≡ λx. L'이고 L →β L'이어서 M →β N인 경우:

        φ(M)

        ≡ λx. φ(L)

        ⇒β λx. φ(L') /* 가정에 의하여 */

        ≡ φ(N).


17. 보조정리: |M| ⇒β φ(M), for all M ∈ Λ.


    증명) M이 생성되는 경우로 나누어 귀납적으로 증명합시다.


    Case1. M ≡ x인 경우:

        |x| ≡ x ≡ φ(x)이므로 성립합니다.

    Case2. M ≡ P Q인 경우:

        |P Q|

        ≡ |P| |Q|

        ⇒β φ(P) φ(Q) /* 가정에 의하여 */

        ≡ φ(P Q).

    Case3. M ≡ λx. N인 경우:

        |λx. N|

        ≡ λx. |N|

        ⇒β λx. φ(N) /* 가정에 의하여 */

        ≡ φ(λx. N).

    Case4. M ≡ (λx. P) Q인 경우:

        |(λx. P) Q|

        ≡ (λx. |P|) |Q|

        ⇒β (λx. φ(P)) φ(Q) /* 가정에 의하여 */

        →β φ(P)[x := φ(Q)]

        ≡ φ((λx. P) Q).


18. 조각 보조정리의 증명: 

    N1을 M 안의 redex R ≡ (λx. P) Q를 축약한 결과라고 합시다.

    M 안의 R을 R' ≡ (λx. P) Q로 치환한 결과를 M'라 합시다. 그러면 |M'| ≡ M이고 φ(M') ≡ N1입니다.

    이때 |N2'| ≡ N2인 N2'가 존재하므로 보조정리 15에 의하여 M ⇒β N2'이고

    보조정리 17에 의하여 |N2'| ⇒β φ(N2')입니다.

    그런데 보조정리 16에 의하여 N1 ⇒β φ(N2')이므로 N3를 φ(N2')로 두고 증명을 마치겠습니다.


19. Church-Rosser 정리의 증명: 

    M ⇒β N이면 M ≡ M1 →β M2 →β ... →β Mn ≡ N1이므로 각각에 대하여 계단 보조정리를 적용하면 됩니다.