Church encoding. Alonzo Church가 제안한, 자연수 같은 일반적인 개념들을 람다 대수로 부호화하는 방법. 람다 대수에서 모든 것은 함수이기 때문에 이 개념들 또한 적절한 고차 함수로 표현되어야 하는데, 다행히도(?) 이 부호화 방법은 어려운 것이 아니다. 단지 귀찮을 뿐.
논리값을 람다 대수에서 표현하려면 크게 두 가지를 인식해야 한다. 하나는 우리는 단지 두 개의 값, true와 false만 필요하다는 거고, 다른 하나는 이 두 값이 (함수이므로) 같은 인자를 받아들여서 서로 다른 결과를 낼 수 있도록 해야 한다는 것이다. 이를 만족하는 한 가지 방법은 다음과 같다:
\mathbf{T} = \lambda a.\, \lambda b.\, a
\mathbf{F} = \lambda a.\, \lambda b.\, b
따라서 어떤 논리값 b가 있을 때 b\ then\ else는 b가 참일 때 then을, 거짓일 때 else를 돌려 주게 된다. 타입 있는 람다 대수에서 이는 \tau\to\tau\to\tau 타입에 대응된다. 여기에 대한 연산은 다음과 같이 정의할 수 있다:
\mathbf{if} = \lambda x.\, \lambda a.\, \lambda b.\, x\ a\ b
\mathbf{and} = \lambda x.\, \lambda y.\, x\ y\ x
\mathbf{or} = \lambda x.\, \lambda y.\, x\ x\ y
\mathbf{not} = \lambda x.\left( \lambda a.\, \lambda b.\, x\ b\ a \right)
\mathbf{xor} = \lambda x.\, \lambda y.\left( \lambda a.\, \lambda b.\, x\ (y\ b\ a)\ (y\ a\ b) \right)
자연수를 람다 대수에서 표현하기 위한 기본적인 아이디어는, 자연수 n에 대응되는 함수는 다른 함수를 받아서 그 함수를 n회 반복 실행해야 한다는 것이다. 따라서 다음과 같은 대응이 성립해야 한다:
\mathbf{0} = \lambda f.\, \lambda x.\, x
\mathbf{1} = \lambda f.\, \lambda x.\, f\ x
\mathbf{2} = \lambda f.\, \lambda x.\, f\ (f\ x)
\mathbf{3} = \lambda f.\, \lambda x.\, f\ (f\ (f\ x))
등등…
타입 있는 람다 대수에서 모든 처치 숫자는 (\tau\to\tau)\to(\tau\to\tau) 타입을 가진다. 처치 숫자에 대한 연산은 다음과 같이 표현할 수 있으며, 이렇게 얻은 함수는 위의 대응과 β-축약으로 동치이다.
\mathbf{succ} = \lambda n.\left( \lambda f.\, \lambda x.\, f\ (n\ f\ x) \right)
\mathbf{plus} = \lambda m.\, \lambda n.\left( \lambda f.\, \lambda x.\, m\ f\ (n\ f\ x) \right) = \lambda m.\, m\ \mathbf{succ}
\mathbf{times} = \lambda m.\, \lambda n.\left( \lambda f.\, \lambda x.\, m\ (n\ f)\ x \right)
\mathbf{iszero} = \lambda n.\, n\ (\lambda x.\, \mathbf{F})\ \mathbf{T}
마지막 iszero는 0에 대응되는 처치 숫자가 주어진 함수를 전혀 실행하지 않는다는 점을 이용한 것으로 꼭 처치 논리값을 쓸 필요는 없다.
뺄셈은 좀 더 어려운데, 일단 뺄셈을 하기 전에 pred 함수, 즉 0이 아닌 숫자를 그보다 하나 작은 숫자로 대응시키고 0이면 0을 반환하는 함수를 구현하여 사용한다:
\mathbf{pred} = \lambda n.\left( \lambda f.\, \lambda x.\, n\ (\lambda g.\, \lambda h.\, h\ (g\ f))\ (\lambda u.\, x)\ (\lambda u.\, u) \right)
\mathbf{minus} = \lambda m.\, \lambda n.\, (n\ \mathbf{pred})\ m
\mathbf{le} = \lambda m.\, \lambda n.\, \mathbf{iszero}\ (\mathbf{minus}\ m\ n)
\mathbf{eq} = \lambda m.\, \lambda n.\, \mathbf{and}\ (\mathbf{le}\ m\ n)\ (\mathbf{le}\ n\ m)
순서쌍을 구현하기 위해서는 두 개의 원소를 가지고 있을 경우만 구현하면 된다. 여기에 대한 간단한 구현은:
\mathbf{pair} = \lambda x.\, \lambda y.\left( \lambda s.\, s\ x\ y \right)
\mathbf{first} = \lambda p.\, p\ (\lambda x.\, \lambda y.\, x)
\mathbf{second} = \lambda p.\, p\ (\lambda x.\, \lambda y.\, y)
이 구현에서 s는 각 원소를 받아서 어느 쪽을 반환할지 결정하는 선택(selector)의 역할을 한다. 따라서 타입 있는 람다 대수에서 각 쌍의 타입은 (\tau\to\tau\to\tau)\to\tau가 된다. 이 방법을 사용하면 여러 개의 원소를 가진 순서쌍 뿐만 아니라, 그 길이가 미리 알려져 있지 않은 리스트도 다음과 같이 구현할 수 있다:
\mathbf{empty} = \mathbf{pair}\ \mathbf{T}\ \mathbf{\Omega}1)
\mathbf{isempty} = \mathbf{first}
\mathbf{cons} = \lambda h.\, \lambda t.\, \mathbf{pair}\ \mathbf{F}\ (\mathbf{pair}\ h\ t)
\mathbf{head} = \lambda l.\, \mathbf{first}\ (\mathbf{second}\ l)
\mathbf{tail} = \lambda l.\, \mathbf{second}\ (\mathbf{second}\ l)
따라서 4와 5를 가진 리스트는 \mathbf{pair}\ \mathbf{F}\ (\mathbf{pair}\ \mathbf{4}\ (\mathbf{pair}\ \mathbf{F}\ (\mathbf{pair}\ \mathbf{5}\ (\mathbf{pair}\ \mathbf{T}\ \mathbf{\Omega}))))로 표현할 수 있다. 람다 대수에서 리스트를 표현하는 방법은 이 외에도 여러 가지 존재하나 여기서는 생략.