Arithmetic & Logic in Lambda Calculus

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)의 특성만 잘 이해하면 이해하기는 쉬운 편이다.

댓글 달기

이메일 주소는 공개되지 않습니다.

이 사이트는 스팸을 줄이는 아키스밋을 사용합니다. 댓글이 어떻게 처리되는지 알아보십시오.