4.12 람다 대수에서의 산술 연산 정의

1. 산술 연산의 람다 대수적 구현

순수 람다 대수에서 산술 연산은 처치 수(Church Numeral) 위에서 정의된다. 모든 산술 연산은 함수의 추상화(Abstraction)와 적용(Application)만으로 구현되며, 이는 산술이 순수 함수적 계산의 특수한 사례임을 보여준다.

2. 가산적 연산

2.1 덧셈의 정의와 정당성 증명

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

정당성 증명: $\text{ADD} \; \overline{a} \; \overline{b} =_\beta \overline{a+b}$ 를 증명한다.

$\text{ADD} \; \overline{a} \; \overline{b} = (\lambda m. \lambda n. \lambda f. \lambda x. m \; f \; (n \; f \; x)) \; \overline{a} \; \overline{b}$
$\rightarrow_\beta \lambda f. \lambda x. \overline{a} \; f \; (\overline{b} \; f \; x)$
$= \lambda f. \lambda x. \overline{a} \; f \; (f^b(x))$
$= \lambda f. \lambda x. f^a(f^b(x))$
$= \lambda f. \lambda x. f^{a+b}(x)$
$= \overline{a+b} \quad \blacksquare$

뺄셈의 정의

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

여기서 $\text{PRED}$ 는 선행자 함수이다. $\text{SUB} \; \overline{a} \; \overline{b}$ 는 $\text{PRED}$ 를 $\overline{a}$ 에 $b$ 번 적용하여 $\overline{\max(a-b, 0)}$ 를 산출한다.

3. 승법적 연산

3.1 곱셈의 정의와 정당성 증명

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

정당성 증명: $\text{MULT} \; \overline{a} \; \overline{b} =_\beta \overline{a \times b}$ 를 증명한다.

$\text{MULT} \; \overline{a} \; \overline{b} = \lambda f. \overline{a} \; (\overline{b} \; f)$

$\overline{b} \; f = \lambda x. f^b(x)$ 는 “ $f$ 를 $b$ 번 적용하는 함수“이다. 이를 $g$ 로 놓으면:

$\overline{a} \; g = \lambda x. g^a(x) = \lambda x. (f^b)^a(x) = \lambda x. f^{a \times b}(x)$

따라서:

$\text{MULT} \; \overline{a} \; \overline{b} = \lambda f. \lambda x. f^{a \times b}(x) = \overline{a \times b} \quad \blacksquare$

3.2 거듭제곱의 정의와 정당성 증명

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

정당성 증명: $\text{EXP} \; \overline{a} \; \overline{b} =_\beta \overline{a^b}$

$\text{EXP} \; \overline{a} \; \overline{b} = \overline{b} \; \overline{a}$

$\overline{b}$ 는 “함수를 $b$ 번 적용“이고, $\overline{a}$ 는 “함수를 $a$ 번 적용하는 함수“이다.

$\overline{b} \; \overline{a} = \overline{a}^b$ . $\overline{a}$ 를 한 번 적용하면 $f$ 가 $a$ 번 적용되고, 이를 $b$ 번 반복하면 $f$ 가 $a^b$ 번 적용된다. 따라서 $\overline{b} \; \overline{a} = \overline{a^b}$ . $\blacksquare$

4. 비교 연산

4.1 영 판별(ISZERO)

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

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

이하 비교(LEQ, Less than or Equal)

$\text{LEQ} = \lambda m. \lambda n. \text{ISZERO} \; (\text{SUB} \; m \; n)$

$m \leq n$ 이면 $\text{SUB} \; m \; n = \overline{0}$ 이므로 $\text{TRUE}$ 를 반환한다.

4.2 동치 비교(EQ, Equal)

$\text{EQ} = \lambda m. \lambda n. \text{AND} \; (\text{LEQ} \; m \; n) \; (\text{LEQ} \; n \; m)$

$m = n$ 이면 $m \leq n$ 이고 $n \leq m$ 이므로 $\text{TRUE}$ 를 반환한다.

미만 비교(LT, Less Than)

$\text{LT} = \lambda m. \lambda n. \text{NOT} \; (\text{LEQ} \; n \; m)$

5. 나눗셈과 나머지

5.1 나눗셈(DIV)

나눗셈은 재귀적으로 정의된다. $a \div b$ 는 $a$ 에서 $b$ 를 반복적으로 뺄 수 있는 횟수이다.

$G_{\text{div}} = \lambda f. \lambda a. \lambda b. \text{IF} \; (\text{LT} \; a \; b) \; \overline{0} \; (\text{SUCC} \; (f \; (\text{SUB} \; a \; b) \; b))$

$\text{DIV} = \mathbf{Y} \; G_{\text{div}}$

5.2 나머지(MOD)

$G_{\text{mod}} = \lambda f. \lambda a. \lambda b. \text{IF} \; (\text{LT} \; a \; b) \; a \; (f \; (\text{SUB} \; a \; b) \; b)$

$\text{MOD} = \mathbf{Y} \; G_{\text{mod}}$

6. 페아노 공리의 충족

처치 수에 대한 산술 연산이 페아노 공리(Peano Axioms)를 만족함을 확인할 수 있다:

$\overline{0}$ 은 자연수이다. ✓ ( $\overline{0} = \lambda f. \lambda x. x$ )
모든 자연수 $\overline{n}$ 에 대해 $\text{SUCC} \; \overline{n}$ 은 자연수이다. ✓
$\text{SUCC} \; \overline{n} \neq_\beta \overline{0}$ (모든 $n$ 에 대해). ✓
$\text{SUCC} \; \overline{m} =_\beta \text{SUCC} \; \overline{n}$ 이면 $\overline{m} =_\beta \overline{n}$ . ✓ (후자 함수의 단사성)
수학적 귀납법: Y 조합자에 의한 재귀로 구현 가능. ✓

이 충족은 처치 수가 자연수의 올바른 람다 대수적 인코딩임을 이론적으로 보장한다.

7. 산술 연산의 복잡도

연산	시간 복잡도 (축약 단계)
SUCC	$O(1)$
ADD	$O(a)$ 또는 $O(1)$ (정의에 따라)
MULT	$O(a)$
EXP	$O(b)$
PRED	$O(n)$
SUB	$O(b \cdot a)$ ( $\text{PRED}$ 를 $b$ 번 적용)
ISZERO	$O(1)$

선행자(PRED)의 $O(n)$ 복잡도는 처치 인코딩의 주된 비효율성이며, 이로 인해 뺄셈과 비교 연산의 복잡도가 높아진다.

8. 산술 연산 정의의 이론적 의의

람다 대수에서의 산술 연산 정의는 다음의 이론적 의의를 갖는다.

첫째, 산술의 함수적 환원: 모든 산술 연산이 함수의 추상화와 적용만으로 정의 가능하다는 것은, 산술이 순수 함수적 계산의 특수한 경우임을 증명한다.

둘째, 계산 가능성의 확인: 재귀적으로 정의 가능한 모든 산술 함수가 람다 대수로 표현 가능하다는 것은, 람다 정의 가능성(Lambda Definability)이 재귀적 함수(Recursive Function) 전체를 포착함을 보여주는 증거이다.

셋째, 함수형 프로그래밍의 기반: 처치 수 위의 산술 연산은 함수형 프로그래밍에서 재귀, 고차 함수, 패턴 매칭 등의 프로그래밍 기법이 산술적 계산을 구현하는 방식의 이론적 원형이다.