4.11 처치 수(Church Numerals)를 통한 자연수 인코딩

1. 처치 인코딩의 원리

처치 인코딩(Church Encoding)은 순수 람다 대수(Pure Lambda Calculus)에서 기본 데이터 유형(자연수, 불 값, 쌍, 리스트 등)을 함수로 표현하는 기법이다. 처치(Alonzo Church)가 1930년대에 개발한 이 기법은 순수 함수만으로 데이터와 계산을 통합적으로 표현할 수 있음을 보여준다.

처치 인코딩의 핵심 아이디어는 데이터를 그 데이터에 대한 연산의 패턴으로 표현하는 것이다. 자연수 n은 “함수를 n번 적용하는 것“으로 표현된다.

2. 처치 수의 정의

자연수 n \geq 0에 대응하는 처치 수(Church Numeral) \overline{n}은 다음과 같이 정의된다:

\overline{n} = \lambda f. \lambda x. f^n(x) = \lambda f. \lambda x. \underbrace{f(f(\cdots(f}_{n \text{번}} \; x)\cdots))

구체적으로:

\overline{0} = \lambda f. \lambda x. x
\overline{1} = \lambda f. \lambda x. f \; x
\overline{2} = \lambda f. \lambda x. f \; (f \; x)
\overline{3} = \lambda f. \lambda x. f \; (f \; (f \; x))

처치 수 \overline{n}은 두 인자 fx를 받아, fxn번 반복 적용한 결과를 반환하는 고차 함수(Higher-Order Function)이다. \overline{0}f를 한 번도 적용하지 않고 x를 그대로 반환하며, 이는 f^0 = \text{id}(항등 함수)에 대응한다.

처치 수에 대한 산술 연산

후자 함수(Successor, SUCC)

\text{SUCC} = \lambda n. \lambda f. \lambda x. f \; (n \; f \; x)

n \; f \; xf^n(x)를 계산하고, 여기에 f를 한 번 더 적용하여 f^{n+1}(x)를 얻는다.

검증:
\text{SUCC} \; \overline{0} = \lambda f. \lambda x. f \; (\overline{0} \; f \; x) = \lambda f. \lambda x. f \; x = \overline{1} \; \checkmark
\text{SUCC} \; \overline{2} = \lambda f. \lambda x. f \; (\overline{2} \; f \; x) = \lambda f. \lambda x. f \; (f \; (f \; x)) = \overline{3} \; \checkmark

2.1 덧셈(Addition, ADD)

\text{ADD} = \lambda m. \lambda n. \lambda f. \lambda x. m \; f \; (n \; f \; x)

n \; f \; x = f^n(x)를 먼저 계산하고, 이 결과에 m \; f = f^m을 적용하여 f^{m+n}(x)를 얻는다.

또는 후자 함수를 m번 적용하는 방식:

\text{ADD} = \lambda m. \lambda n. m \; \text{SUCC} \; n

검증: \text{ADD} \; \overline{2} \; \overline{3} = \overline{2} \; \text{SUCC} \; \overline{3} = \text{SUCC} \; (\text{SUCC} \; \overline{3}) = \text{SUCC} \; \overline{4} = \overline{5} \; \checkmark

2.2 곱셈(Multiplication, MULT)

\text{MULT} = \lambda m. \lambda n. \lambda f. m \; (n \; f)

n \; f는 “fn번 적용하는 함수“이고, m \; (n \; f)는 이 함수를 m번 적용한다. 따라서 f가 총 m \times n번 적용된다.

또는:

\text{MULT} = \lambda m. \lambda n. m \; (\text{ADD} \; n) \; \overline{0}

2.3 거듭제곱(Exponentiation, EXP)

\text{EXP} = \lambda m. \lambda n. n \; m

검증: \text{EXP} \; \overline{2} \; \overline{3} = \overline{3} \; \overline{2}. \overline{3}은 “함수를 3번 적용“이고, \overline{2}는 “함수를 2번 적용하는 함수“이므로, \overline{3} \; \overline{2}는 “2번 적용을 3번 적용” = 2^3 = 8번 적용. 따라서 \overline{3} \; \overline{2} = \overline{8} \; \checkmark

선행자 함수(Predecessor, PRED)

선행자 함수는 처치 수에 대한 가장 복잡한 기본 연산이다. 직접적 정의:

\text{PRED} = \lambda n. \lambda f. \lambda x. n \; (\lambda g. \lambda h. h \; (g \; f)) \; (\lambda u. x) \; (\lambda u. u)

이 정의의 핵심 아이디어는 쌍(Pair)을 사용하여 이전 값을 추적하는 것이다. n번의 반복 과정에서 현재 값과 이전 값의 쌍을 유지하며, 최종적으로 이전 값(즉, n-1에 대응하는 처치 수)을 추출한다.

\text{PRED} \; \overline{0} = \overline{0} (0의 선행자는 0으로 정의), \text{PRED} \; \overline{n+1} = \overline{n}

2.4 뺄셈(Subtraction, SUB)

\text{SUB} = \lambda m. \lambda n. n \; \text{PRED} \; m

\text{PRED}n번 적용하여 m에서 n을 뺀다. m < n이면 결과는 \overline{0}이다(자연수 뺄셈의 바닥 기능).

처치 불(Church Boolean)과 조건 분기

불 값의 정의

\text{TRUE} = \lambda x. \lambda y. x
\text{FALSE} = \lambda x. \lambda y. y

처치 불은 두 인자 중 하나를 선택하는 함수이다. \text{TRUE}는 첫 번째를, \text{FALSE}는 두 번째를 선택한다.

조건 분기(IF-THEN-ELSE)

\text{IF} = \lambda b. \lambda t. \lambda e. b \; t \; e

\text{IF} \; \text{TRUE} \; M \; N = \text{TRUE} \; M \; N = M
\text{IF} \; \text{FALSE} \; M \; N = \text{FALSE} \; M \; N = N

2.5 영 판별(ISZERO)

\text{ISZERO} = \lambda n. n \; (\lambda x. \text{FALSE}) \; \text{TRUE}

\overline{0}f를 적용하지 않으므로 \text{TRUE}를 반환하고, \overline{n} (n > 0)은 (\lambda x. \text{FALSE})를 적어도 한 번 적용하므로 \text{FALSE}를 반환한다.

논리 연산

\text{AND} = \lambda p. \lambda q. p \; q \; \text{FALSE}
\text{OR} = \lambda p. \lambda q. p \; \text{TRUE} \; q
\text{NOT} = \lambda p. p \; \text{FALSE} \; \text{TRUE}

3. 처치 인코딩의 한계와 의의

3.1 효율성의 한계

처치 수에서의 산술 연산은 이론적으로 올바르지만 효율적이지 않다. 선행자 함수가 O(n) 시간을 요구하고, 뺄셈과 비교 연산도 마찬가지이다. 실용적 프로그래밍 언어에서는 처치 인코딩 대신 원시(Primitive) 데이터 유형을 사용한다.

3.2 이론적 의의

처치 인코딩의 핵심적 의의는 데이터가 함수로 환원 가능하다는 것을 증명하는 것이다. 순수 함수만으로 자연수, 불 값, 쌍, 리스트, 트리 등 모든 데이터 구조를 표현할 수 있으며, 이는 람다 대수의 계산적 보편성을 확립하는 근거이다.

또한, 처치 인코딩에서 데이터와 연산의 경계가 소멸한다는 관찰은 객체 지향 프로그래밍(Object-Oriented Programming)에서 데이터와 메서드가 결합되는 원리의 함수적 원형으로 해석될 수 있다.