Tutorial Introduction to Lambda Calculus을 읽으면서 재미있었던 것은 Church integer/boolean들과 그에 상응하는 arithmetic/logic operator가 λ calculus만으로도 잘 정의될 수 있다는 점이었다. 예를 들어보자.
Church integer
λ calculus를 사용하여 자연수를 표현하는 방법 중에는 Church integer라는 방법이 있다.
- 0 := λsz.z
- 1 := λsz.s(z)
- 2 := λsz.s(s(z))
- 3 := λsz.s(s(s(z)))z
간단히 설명하면 자연수 n은 s를 n번 z argument에 적용한 함수인 것이다.
Addition
successor function을 사용하여 Addition을 구현할 수 있다. successor function은 다음과 같다.
- S := λwyx.y(wyx)
successor function에 argument를 적용하면,
S0 := λwyx.y(wyx) λsz.z := λyx.y(λsz.z yx) := λyx.yx := 1
0S := λsz.z λwyx.y(wyx) := λz.z := I (identity function)
S1 := λwyx.y(wyx) λsz.sz := λyx.y(λsz.sz yx) := λyx.yyx := 2
1S := λsz.sz λwyx.y(wyx) := λz.λwyx.y(wyx) z := λz.λyx.y(zyx) = λzyx.y(zyx) = S
S2 := λwyx.y(wyx) λsz.s(s(z)) := λyx.y(λsz.s(s(z)) yx) := λyx.y(y(y(x))) := 3
2S := λsz.s(s(z)) S := λz.S(S(z))
결국, Sn의 형태는 s를 치환하는 y를 하나 더 추가하게 되어 n+1의 결과를 낳게되고, nS의 형태는 Church integer의 특성상 S를 n번 수행하는 함수를 결과로 넘겨주게 된다. 따라서, 다음과 같은 형태도 가능함을 알 수 있다.
2S3 := λz.S(S(z)) 3 := S(S(3)) = S(4) = 5
증명해보지는 않았지만, 아마도 S는 commutative하고 transitive할 것 같다.
그럼 이런 건 어떻게 될까?
12 := λz.2(z) := λz.(λst.s(s(t)))z := λz.(λt.z(z(t))) := λzt.z(z(t)) := 2
22 := λz.2(2(z)) := λz.2(λt.z(z(t))) := λz.(λsu.s(s(u)) (λt.z(z(t))) ) := λz.(λu.(λt.z(z(t))) ((λt.z(z(t))) u) ) := λz.(λu.(λt.z(z(t))) z(z(u)) ) := λzu.z(z(z(z(u)))) = 4
결과는 곱셈 같지만, 다른 것들도 계산해보면, 일관성있는 결과는 나오지 않는 것 같다. 물론, Church integer에 대한 곱셈 연산도 따로 있다.
Churge Booleans
- T := λxy.x
- F := λxy.y
F는 0과 동일함을 눈여겨볼 수 있다.
Logic
기본적인 논리 연산들은 다음과 같이 정의된다.
- ∧ := λxy.xy(λuv.v) := λxy.xyF
- ∨ := λxy.x(λuv.u)y := λxy.xTy
- ¬ := λx.x(λuv.v)(λab.a) := λx.xFT
T는 두 argument 중 첫번째를 선택하고, F는 두번째를 선택하므로, 쉽게 다음을 계산할 수 있다.
∧TT := TTF := T
∧TF := TFF := F
∧FT := FTF := F
∧FF := FFF := F
∨TT := TTT := T
∨TF := TTF := T
∨FT := FTT := T
∨FF := FTF := F
¬T := TFT := F
¬F := FFT := T
Tutorial에서는 multiplication, conditional test, predecessor, equiality, recursion 등도 소개하고 있는데, λ calculus의 substitution과 기본적인 함수들(church integers/booleans, arithmetic/logic operator)의 특성만 잘 이해하면 이해하기는 쉬운 편이다.