Chapter 3. The Power of Lambda: If φ is numeric function, we have "φ is computable." ↔ "φ is λ-definable.".


> 먼저 참과 거짓을 정의해 봅시다.


1. 정의: if then else 구문.


1) true ≡ λx,y. x, false ≡ λx,y. y이라고 합시다.


2) 그러면 B가 true 또는 false일 때 B P Q가 if B then P else Q를 나타내는 것을 알 수 있습니다.


2. 정의: 순서있는 쌍(ordered pair).


1) 임의의 람다-항 M, N에 대하여 [M, N] ≡ λb. b M N이라고 합시다.


2) 그러면 항상 [M, N] true = M이고 [M, N] false = N입니다.


> 이제 람다-항들의 리스트를 구현해 봅시다. Cons, Head, Tail, Null, nil을 만들면 되겠네요.

다음과 같이 택할 수 있습니다. 밑을 보지 말고 여러분도 한 번 만들어 보세요.


Cons ≡ λx,y,z. z x y,

Head ≡ λx. x true,

Tail ≡ λx. x false,

Null ≡ λx. x (λy,z. false),

nil ≡ λx. true.


그러면 리스트 [M, N, ..., L]를 Cons M (Cons N (Cons ... (Cons L nil)))로 구현할 수 있겠죠?

두 리스트를 합치는 함수 Append를 만들면서 워밍업을 마무리합시다.

nil이 아닌 임의의 리스트 X와 임의의 리스트 Y에 대하여


Append nil Y = Y,

Append X Y = Cons (Head X) (Append (Tail X) Y)


이면 되므로, 고정점 결합자 Y ≡ λf. (λx. f (x x)) (λx. f (x x))을 이용하여, 다음과 같이 택할 수 있습니다.


Append ≡ Y (λf,x,y. (Null x) (y) (Cons (Head x) (f (Tail x) y))).


> 이제 처치 수(Church numeral) 대신 사용할 자연수의 새로운 표현을 정의해 봅시다.


3. 정의: 'n'.


1) 다음과 같이 정의합시다.


'0' ≡ I,

'n + 1' ≡ [false, 'n'], for all n ∈ N.


4. 보조정리: successor(다음 수), predecessor(이전 수), test for zero(0인지 확인).


1) 임의의 자연수 n에 대하여 다음을 만족하는 결합자 S+, P-, Zero가 존재합니다.


S+ 'n' = 'n + 1',

P- 'n + 1' = 'n',

Zero '0' = true,

Zero 'n + 1' = false.


증명) S+ ≡ λx. [false, x], P- ≡ λx. x true, Zero ≡ λx. x false를 택하면 됩니다.


5. 정의: λ-정의가능성(λ-definability).


1) 수치 함수(numeric function)은 p에 대한 사상 φ: N^p → N입니다.

이 경우 φ는 p개의 항(p-ary)을 취한다고 합니다.


2) p항의 수치 함수 φ는 다음을 만족하는 결합자 F가 존재할 때 λ-정의가능하다고 합니다.


F 'n_1' ... 'n_p' = 'φ(n_1, ..., n_p)', for all n_1, ..., n_p ∈ N.


이 경우 φ는 F에 의하여 λ-정의된다고 합니다.


> 계산가능성(computability): 부분 함수 f: N^p → N에 대하여 입력 x ∈ N^p를 받아

x가 f의 정의역의 원소라면 f(x)를 출력한 후 종료되고 그렇지 않으면 영원히 종료되지 않는 알고리듬이

존재할 때 그리고 오직 그럴 때에만 f가 계산가능하다고 합니다.


> 그런데 함수가 계산가능할 때 그리고 오직 그럴 때에만 recursive하다는 것이 밝혀졌습니다.

여기서 recursive는 우리가 아는 재귀와 약간 다릅니다. 조금 뒤에서 설명하겠습니다.

이제부터 λ-정의가능한 함수는 recursive함을 보이겠습니다.


6. 정의: 초기함수(initial function).


1) 초기함수들은 다음과 같이 정의된 3 개의 수치 함수 U[i]n, S+, Z입니다.


U[i]n(x_1, ..., x_n) = x_i, 1 ≤ i ≤ n;

S+(n) = n + 1;

Z(n) = 0.


> 자연수 n에 대한 명제 P(n)에 대하여


μn. P(n) = x ↔ (∀i. 1 ≤ i ≤ x ⇒ ￢P(i)) and P(x)


이라 정의합시다.


> 벡터를 표현하기 어려운 관계로 n이나 x를 보면 벡터라고 생각해 주세요.


7. 정의: 수치 함수들의 분류(class)의 3 가지 연산- 합성(composition), 원시 재귀(primitive recursion),

최소화(minimalization) -에 대하여 닫혀있음은 다음과 같이 정의됩니다.


1) 다음과 같이 정의되는 모든 φ에 대하여 φ ∈ A를 얻을 때 A는 합성에 대하여 닫혀있다고 합니다.


φ(n) = χ(ψ_1(n), ..., ψ_m(n)), with χ, ψ_1, ..., ψ_m ∈ A.


2) 다음과 같이 정의되는 모든 φ에 대하여 φ ∈ A를 얻을 때 A는 원시 재귀에 대하여 닫혀있다고 합니다.


φ(0, n) = χ(n), φ(k + 1, n) = ψ(φ(k, n), k, n), with χ, ψ ∈ A.


3) 다음과 같이 정의되는 모든 φ에 대하여 φ ∈ A를 얻을 때 A는 최소화에 대하여 닫혀있다고 합니다.


φ(n, m) = μm. [χ(n, m) = 0], with χ ∈ A such that ∀n. ∃m. χ(n, m) = 0.


8. 정의: recursive한 함수들의 분류 R.


1) R은 모든 초기함수들을 포함하고 합성, 원시 재귀, 최소화에 닫혀있는 수치 함수들의 가장 작은 분류입니다.


2) 그러므로 R을 귀납적으로 정의할 수 있습니다.


> The proof that all recursive functions are λ-definable is in fact by corresponding induction argument - Kleene(1936).


9. 보조정리: 초기함수들은 λ-정의가능합니다.


증명) U[i]n ≡ λx_1,...,x_n. x_i, S+ ≡ λx. [false, x], Z ≡ λx. '0'을 택하면 됩니다.


10. 보조정리: λ-정의가능한 함수들은 합성에 대하여 닫혀있습니다.


11. 보조정리: λ-정의가능한 함수들은 원시 재귀에 대하여 닫혀있습니다.


12. 보조정리: λ-정의가능한 함수들은 최소화에 대하여 닫혀있습니다.


13. 정리: 모든 recursive한 함수는 λ-정의가능합니다.


> 역 또한 성립합니다. 그러므로 수치 함수 φ에 대하여 φ가 recursive일 때 그리고 오직 그럴 때에만 λ-정의가능합니다.

게다가 부분 함수에 대해서도 λ-정의가능성의 개념이 존재합니다. 만약 ψ가 부분 함수라면 다음을 얻습니다.


ψ is partial recursive ↔ ψ is λ-definable.


14. 정리: 모든 recursive한 함수는 처치 수 c_n에 대하여 λ-정의될 수 있습니다.


15. 명제: 람다항 T, T^-1이 존재하여 임의의 자연수 n에 대하여 T c_n = 'n'이고 T^-1 'n' = c_n입니다.


16. 따름정리: 정리 14의 다른 증명 - F가 φ을 'n'으로 λ-정의할 때

변환자 T와 T^-1을 이용하면 φ는 F_c에 의하여 c_n으로 λ-정의할 수 있습니다.


> 마지막으로 연립방정식을 풀 때 쓰는 기술을 배우겠습니다.


17. 다중 고정점 정리(multiple fixed-point theorem): F_1, ..., F_n이 람다-항일 때

다음을 만족하는 X_1, ..., X_n이 항상 존재합니다.


X_1 = F_1 X_1 ... X_n,

.

.

.

X_n = F_n X_1 ... X_n.


증명) X ≡ [F_1 X_1 ... X_n, ..., F_n X_1 ... X_n]이라 정의합시다.

그러면 X_i = Head (c_i Tail X)일 때 기존의 고정점 정리에 의하여 X를 구할 수 있습니다.

따라서 모든 X_i를 적어도 하나씩 구할 수 있습니다.


> 마치며: 원래 22일 오후 3시 반에 올렸는데 지워졌네요 ㅠㅠ 다음 주에 4장 reduction으로 돌아오겠습니다.

삭제된 글에 있던 증명과 연습문제는 자고난 다음에 올릴게요.