처치 부호화

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

처치 논리값

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

\mathbf{T} = \lambda a.\, \lambda b.\, a
\mathbf{F} = \lambda a.\, \lambda b.\, b

따라서 어떤 논리값 b가 있을 때 b\ then\ elseb가 참일 때 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}))))로 표현할 수 있다. 람다 대수에서 리스트를 표현하는 방법은 이 외에도 여러 가지 존재하나 여기서는 생략.

1) 여기서 \mathbf{\Omega}는 정규화가 되지 않는 아무 함수나 사용할 수 있으며, 빈 리스트를 참조하는 것이 정의되어 있지 않다는 의미로 쓰였다.

도쿠위키DokuWiki-custom(rev 9085d92e02)을 씁니다.
마지막 수정 2011-05-30 18:25 | 외부 편집기