연습문제: P, Q를 임의의 람다-항이라고 합시다. P와 Q는 양립불가능(incompatible)하고- P # Q로 표기합니다 -
λ에 P = Q를 공리로 추가함으로써 람다 대수를 확장하면 모든 람다-항 사이에 등호가 성립할 것입니다.
예를 들어, ∀M, N ∈ Λ에 대하여 λ+(P = Q)⊢ M = N을 얻습니다.
이런 경우 λ+(P = Q)를 모순된(incosistent)다고 합니다.
1) true ≡ K이고 false ≡ K*일 때, P, Q ∈ Λ에 대하여 다음 두 명제가 동치임을 보이세요.
P # Q.
λ+(P = Q)⊢ true = false.
풀이)
∀M, N ∈ Λ. M = N
⟺ ∀N. ∀M. true M N = false M N
⟺ ∀M. true M = false M
⟺ true = false.
∴(P # Q) ⟺ (∀M, N ∈ Λ. λ+(P = Q)⊢ M = N) ⟺ (λ+(P = Q)⊢ true = false).
2) I # K임을 보이세요.
풀이)
I = K ⇒ I K = K I ⇒ λx,y. I K x y = λx,y. K I x y ⇒ λx,y. x = λx,y. y ⇒ true = false.
λ+(I = K)⊢ true = false ⇒ I # K.
3) F I = x이고 F K = y인 람다항을 찾으세요.
풀이)
F I = M N x y이고 F K = N x y인 F가 있다면 M과 N을 각각 λa,b,c. b, λa,b. b로 놓으면 됩니다.
그러므로 F ≡ λf. f I (λa,b,c. b) (λa,b. b) x y이면 됩니다.
4) K # S임을 보이세요.
풀이)
Let F ≡ λf. f I (λa,b,c. b) (λa,b. b) x y.
S K K = λx. S K K x = λx. K x (K x) = λx. x = I.
K = S
⇒ λx,y. F (K K K) = λx,y. F (S K K)
⇒ λx,y. F K = λx,y. F I
⇒ λx,y. x = λx,y. y
⇒ true = false.
λ+(K = S)⊢ true = false ⇒ K # S.
> 풀 만하셨나요? 틀린 거 지적이나 질문 환영합니다.
이런거 배우려면 무슨책 봐야함?
이 책은 Introduction to Lambda Calculus에요
http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf
1번 풀이가 찜찜한데.... M, N이 보기에는 P, Q가 고정된 것처럼 보이는 거 같은데....