> 이제 람다-토폴로지(?)에 대해 공부해봅시다.
20. 정의: 람다-항 M에 대하여 M의 소거 그래프 G[β](M)은 { X ∈ Λ | M ⇒β X }가 정점들의 집합이고 →β가 방향인 멀티 그래프입니다.
21. 예제: 그래프 G[β](I (I x))는 다음과 같이 표로 나타낼 수 있습니다.
from/to | I (I x) | I x | x | ||||||
I (I x) | 2 | ||||||||
I x | 1 | ||||||||
x |
> 한편 K I Ω를 생각해 봅시다. Ω →β Ω →β Ω →β ...이므로 eager한 소거 전략을 택하면 무한 루프에 빠집니다.
하지만 왼쪽 우선 소거 전략을 택하면 K I Ω ⇒β I입니다.
22. 표준화 정리: M이 표준형을 가진다면 가장 왼쪽의 redex를 축약하는 것을 반복함으로써 표준형에 도달할 수 있습니다.
증명은 Barendregt(1984)에 있다는데 못 찾겠습니다.
23. 예제: K Ω I를 왼쪽 우선 소거 전략을 택하여 소거해도 무한루프에 빠지므로 K Ω I는 표준형을 가지지 않음을 알 수 있습니다.
> 고정점 정리에 소거를 적용한 버전을 공부해 봅시다.
24. 정의: 튜링의 고정점 결합자 Θ는 A ≡ λx,y. y (x x y)에 대하여 Θ ≡ A A입니다.
25. 명제: 모든 람다-항 F에 대하여 Θ F ⇒β F (Θ F)을 얻습니다.
증명) Θ F ≡ A A F →β (λy. y (A A y)) F →β F (A A F) ≡ Θ F.
26. 예제: ∃G. ∀X. G X ⇒β X (X G).
증명) G ≡ Θ (λg,x. x (x g))
⇒ G ⇒β ((λg,x. x (x g)) G
⇒ G ⇒β λx. x (x G)
⇒ G X ⇒β X (X G).
27. 정리: 임의의 람다-항 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 ≡ (Cons (F_1 X_1 ... X_n) (Cons ... (Cons (F_n X_1 ... X_n) nil)))을 두고
X_i ≡ Head (c_i Tail X))일 때 X_i ⇒β F_i X_1 ... X_n임을 보이면 됩니다.
> 마치며: 오늘은 β-소거에 대하여 깊이있게 공부했습니다. 강의는 지루했지만 연습문제는 어렵고 재미있으니 풀어보세요.
연습문제에 대한 대략적인 풀이를 댓글로 달아주시면 감사하겠습니다. 1, 2, 3, 4, 5번은 풀었습니다.
그리고 질문이나 지적도 환영하니 댓글 많이 달아주세요. 다음주에 5장 ＜타입 할당＞에 대하여 정리해 올리겠습니다.
1) ∀M∈Λ. ∃N∈Λ. N in β-nf and N I ⇒β M을 보이세요.
2) 각각 다음과 같은 G[β](M)을 갖는 4개의 항 M을 생성하세요.
from/to | A | B | C | D | |||||
A | 1 | 1 | |||||||
B | 1 | 1 | |||||||
C | 1 | 1 | |||||||
D | 1 | 1 |
from/to | A | B | C | ||||||
A | 1 | 1 | |||||||
B | 1 | 1 | |||||||
C |
from/to | A | B | C | ||||||
A | 1 | 1 | |||||||
B | 1 | 1 | |||||||
C |
from/to | A | B | C | ||||||
A | 1 | ||||||||
B | 1 | 1 | |||||||
C | 1 |
3) 모든 람다-항 M, N에 대하여 다음을 만족하는 F는 존재하지 않는다는 것을 보이세요.
F (M N) = M.
4) A ≡ λa,x,z. z (a a x)이고 M ≡ A A x일 때 임의의 자연수 n에 대하여 G[β](M)이 n차원 큐브를 서브그래프로 가짐을 보이세요.
5) A. Visser:
1) 다음 그래프를 갖는 redex R이 유일함을 보이세요.
from/to | R | ||||||||
R | 1 |
2) G[β](M)로 다음 그래프를 갖는 람다-항 M은 존재하지 않음을 보이세요.
from/to | A | B | C | D | E | ||||
A | 1 | 1 | 1 | ||||||
B | 1 | ||||||||
C | 1 | ||||||||
D | 1 | ||||||||
E |
6) C. Bohm. M이 각각 다음과 같을 때 G[β](M)을 시험하세요.
1) H I H, H ≡ λx,y. x (λz. y z y) x.
2) L L I, L ≡ λx,y. x (y y) x.
3) Q I Q, Q ≡ λx,y. x y I x y.
7) J.W. Klop. λ-calculus를 두 상수 δ, ε을 추가해 확장시킵시다.
소거 규칙 δ M M →δ ε만 추가되면 이 확장된 체계는 Church-Rosser 특성을 가지지 않음을 보이세요.
8) A ≡ λa,x,z. z (a a x)일 때 A A x는 β-표준형을 가지지 않음을 보이세요.
9) M과 N이 다음과 같이 주어졌을 때, λ⊬ M = N을 보이세요.
1) M ≡ W W W, N ≡ ω3 ω3, W ≡ λx,y. x y y, ω3 ≡ λx. x x x.
2) M ≡ (λx. x x a), N ≡ (λx. x x b).
10) M이 다음과 같을 때 G[β](M)을 그리세요.
1) W W W, W ≡ λx,y. x y y.
2) ω ω, ω ≡ λx. x x.
3) ω3 ω3, ω3 ≡ λx. x x x.
5) (λx. I (x x)) (λx. I (x x)).
6) I I (I I I).
11) 항의 길이를 사용된 기호들의 개수 * 0.5[cm]이라고 정의합시다.
30[cm]보다 짧으면서 그것의 표준형은 10^10 ^10 광년보다 긴 람다-항을 적으세요.
글자 수 제한 걸리네요 ㅠㅠ
연습문제 9.2: M ≡ (λx. x x a)(λx. x x a), N ≡ (λx. x x b)(λx. x x b)입니다.
ㄴ 감사합니다