====== 처치 부호화 ======

Church encoding. [[Alonzo Church]]가 제안한, [[자연수]] 같은 일반적인 개념들을 [[람다대수]]로 부호화하는 방법. 람다 대수에서 모든 것은 함수이기 때문에 이 개념들 또한 적절한 고차 함수로 표현되어야 하는데, 다행히도(?) 이 부호화 방법은 어려운 것이 아니다. 단지 귀찮을 뿐.

===== 처치 논리값 =====

[[논리값]]을 람다 대수에서 표현하려면 크게 두 가지를 인식해야 한다. 하나는 우리는 단지 두 개의 값, true와 false만 필요하다는 거고, 다른 하나는 이 두 값이 (함수이므로) 같은 인자를 받아들여서 서로 다른 결과를 낼 수 있도록 해야 한다는 것이다. 이를 만족하는 한 가지 방법은 다음과 같다:

<.indent>
$$\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$$ 타입에 대응된다. 여기에 대한 연산은 다음과 같이 정의할 수 있다:

<.indent>
$$\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$$회 반복 실행해야 한다는 것이다. 따라서 다음과 같은 대응이 성립해야 한다:

<.indent>
$$\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)$$ 타입을 가진다. 처치 숫자에 대한 연산은 다음과 같이 표현할 수 있으며, 이렇게 얻은 함수는 위의 대응과 β-축약으로 동치이다.

<.indent>
$$\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을 반환하는 함수를 구현하여 사용한다:

<.indent>
$$\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)$$
</>

===== 처치 순서쌍 =====

[[순서쌍]]을 구현하기 위해서는 두 개의 원소를 가지고 있을 경우만 구현하면 된다. 여기에 대한 간단한 구현은:

<.indent>
$$\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$$가 된다. 이 방법을 사용하면 여러 개의 원소를 가진 순서쌍 뿐만 아니라, 그 길이가 미리 알려져 있지 않은 [[리스트]]도 다음과 같이 구현할 수 있다:

<.indent>
$$\mathbf{empty} = \mathbf{pair}\ \mathbf{T}\ \mathbf{\Omega}$$((여기서 $$\mathbf{\Omega}$$는 정규화가 되지 않는 아무 함수나 사용할 수 있으며, 빈 리스트를 참조하는 것이 정의되어 있지 않다는 의미로 쓰였다.))\\
$$\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}))))$$로 표현할 수 있다. 람다 대수에서 리스트를 표현하는 방법은 이 외에도 여러 가지 존재하나 여기서는 생략.

{{tag>전산학}}