보조정리 10의 증명)

χ, ψ_1, ..., ψ_m가 각각 G, H_1, ..., H_m으로 λ-정의됐다고 합시다. 그러면

        φ(n) = χ(ψ_1(n), ..., ψ_m(n))

은 F에 의하여 λ-정의되고

        F ≡ λx. G (H_1 x) ... (H_m x).

보조정리 11의 증명)

φ가 다음과 같이 정의된다고 합시다.

        Φ(0, n) = χ(n), φ(k + 1, n) = ψ(φ(k, n), k, n),

여기서 χ, ψ는 각각 G, H로 λ-정의됐습니다. Append를 구했던 것처럼 φ를 정의하는 F를 만듭시다.

        F ≡ Y (λf,x,y. (Zero x) (G y) (H (f (P- x) y) (P- x) y)).

보조정리 12의 증명)

φ가 다음과 같이 정의된다고 합시다.

        φ(n) = μm. [χ(n, m) = 0],

여기서 χ는 G로 λ-정의됐습니다. 고정점 정리에 의하여 다음과 같은 람다-항 H가 존재함을 알 수 있습니다.

        H x y = (Zero (G x y)) (y) (H x (S+ y))).

이때 F ≡ λx. H x '0'라 정의하면 F가 φ를 λ-정의함을 알 수 있습니다.

정리 13의 증명)

보조정리 9-12에 의하여.

정리 14의 증명)

        S[c]+ ≡ λn,f,x. f (n f x),

        P[c]- ≡ λn,f,x. n (λg,h. h (g f)) (λi. x) I,

        Zero_c ≡ λn. n (K false) true

이라 정의합시다. 그러면 이 항들은 각각 다음 수, 이전 수, 0인지 확인을 나타냅니다.

위의 내용에 의하여 모든 recursive한 함수는 c_n으로 λ-정의될 수 있습니다.

> P[c]- ≡ λn,f,x. n (λg,h. h (g f)) (λi. x) I가 무슨 원리로 이전 수를 반환하는지 궁금하지 않나요? 확인해봅시다.

(임의의 자연수 n에 대하여)

{

    (∀F,X∈Λ. c_(n+1) F X = F (c_n F X)) ⇒ c_(n+1) = λf,x. f (c_n f x).

    (임의의 람다-항 succ, zero에 대하여) /* succ는 다음 수, zero는 0을 의미합니다. */

    {

        M_n :≡ c_n (λg,h. h (g succ)) (λi. zero).

        n > 0 ⇒ M_n = (λf,x. f (c_(n-1) f x)) (λg,h. h (g succ)) (λi. zero) = (λg,h. h (g succ)) M_(n-1).

        n = 0 ⇒ M_n = (λf,x. x) (λg,h. h (g succ)) (λi. zero) = (λi. zero).

        n = 1 ⇒ M_n = (λg,h. h (g succ)) (λi. zero) = λh. h zero = λh. h (c_(n-1) succ zero).

        n ≥ 1 ⇒ (M_n = λh. h (c_(n-1) succ zero) ⇒ M_(n+1) = (λg,h. h (g succ)) M_n = λh. h (c_n succ zero)).

        P[c]- c_n succ zero = M_n I = if n = 0 then zero else c_(n-1) succ zero.

    }

    P[c]- c_n = if n = 0 then c_0 else c_(n-1).

}

명제 15의 증명)

다음을 만족하는 변환자(translator) T, T^-1을 만들 수 있기 때문에 명제 15가 성립합니다.

        T ≡ λn. n S+ '0',

        T^-1 = (Zero x) (c_0) (S[c]+ (T^-1 (P- x))).

연습문제 1)

임의의 자연수 n에 대하여 Fac 'n' = 'n!'인 람다-항 Fac을 만드세요.

연습문제 2)

다음 연립방정식 해 G, H가 존재함을 보이세요.

        G x y = H y (K x),

        H x = G (x x) (S (H (x x))).

연습문제 3)

람다-항 And, Or, Not을 만드세요.