보조정리 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을 만드세요.
댓글 0