4.6 베타 축약(β-reduction)의 정의와 계산 규칙

1. 베타 축약의 정의

베타 축약(Beta Reduction, β-reduction)은 람다 대수의 핵심적 계산 규칙이다. 함수(추상화)에 인자를 적용한 결과를 계산하는 것으로, 함수의 본체에서 매개변수를 실제 인자로 대입하는 과정이다.

1.1 형식적 정의

추상화 \lambda x. M에 인자 N을 적용한 결과는 M 내의 x의 모든 자유 출현을 N으로 대입한 것이다:

(\lambda x. M) \; N \rightarrow_\beta M[x := N]

여기서 (\lambda x. M) \; N을 베타 레덱스(Beta Redex, Reducible Expression)라 하고, M[x := N]을 축약형(Reduct, Contractum)이라 한다.

예시

(\lambda x. x) \; a \rightarrow_\beta a
(\lambda x. x \; x) \; a \rightarrow_\beta a \; a
(\lambda x. \lambda y. x) \; a \rightarrow_\beta \lambda y. a
(\lambda f. f \; a) \; (\lambda x. x) \rightarrow_\beta (\lambda x. x) \; a \rightarrow_\beta a

대입의 정밀한 규칙

베타 축약의 핵심 연산인 대입 M[x := N]은 변수 포획(Variable Capture)을 방지하면서 정확히 수행되어야 한다.

대입 규칙

x[x := N] = N
y[x := N] = y \quad (y \neq x)
(M_1 \; M_2)[x := N] = (M_1[x := N]) \; (M_2[x := N])
(\lambda x. M)[x := N] = \lambda x. M
(\lambda y. M)[x := N] = \lambda y. (M[x := N]) \quad \text{if } y \neq x \text{ and } y \notin FV(N)
(\lambda y. M)[x := N] = \lambda z. (M[y := z][x := N]) \quad \text{if } y \neq x \text{ and } y \in FV(N)

마지막 규칙에서 z는 M과 N 모두에서 자유롭지 않은 신선 변수(Fresh Variable)이다. 이 규칙은 알파 변환을 수행하여 변수 포획을 방지한다.

변수 포획의 구체적 예시

올바르지 않은 대입:
(\lambda y. x \; y)[x := y] \neq \lambda y. y \; y

여기서 대입할 N = y가 본체의 속박 변수 y와 동일하므로 변수 포획이 발생한다. 올바른 대입:

(\lambda y. x \; y)[x := y] = (\lambda z. x \; z)[x := y] = \lambda z. y \; z

먼저 알파 변환 \lambda y. x \; y \rightarrow_\alpha \lambda z. x \; z를 수행한 후 대입한다.

다단계 축약과 축약 열

다단계 베타 축약

\rightarrow_\beta^*는 \rightarrow_\beta의 반사적 추이적 폐포(Reflexive Transitive Closure)를 나타내며, 0번 이상의 베타 축약 단계를 나타낸다.

M \rightarrow_\beta^* N \quad \text{iff} \quad M = M_0 \rightarrow_\beta M_1 \rightarrow_\beta \cdots \rightarrow_\beta M_k = N

1.2 축약 전략(Reduction Strategy)

람다 항 내에 여러 베타 레덱스가 동시에 존재할 때, 어떤 레덱스를 먼저 축약할지를 결정하는 규칙을 축약 전략이라 한다. 주요 축약 전략:

정상 순서 축약(Normal Order Reduction): 가장 왼쪽·가장 바깥쪽(Leftmost Outermost)의 레덱스를 먼저 축약한다. 정상 순서 축약은 항이 정규형을 가지면 반드시 그 정규형에 도달하는 것이 보장된다(정규화 정리).

적용 순서 축약(Applicative Order Reduction): 가장 왼쪽·가장 안쪽(Leftmost Innermost)의 레덱스를 먼저 축약한다. 인자를 먼저 완전히 평가한 후 함수에 전달한다. 대부분의 명령형 프로그래밍 언어의 함수 호출 방식(Call by Value)에 대응한다.

느긋한 평가(Lazy Evaluation): 인자를 필요할 때까지 평가하지 않고, 실제로 사용되는 시점에 평가한다. Haskell의 기본 평가 전략이다.

2. 정규형(Normal Form)

2.1 정의

더 이상 베타 축약이 불가능한 람다 항, 즉 베타 레덱스를 포함하지 않는 항을 베타 정규형(Beta Normal Form, β-NF)이라 한다.

예시:

• x: 정규형 (변수이므로 축약 불가)
• \lambda x. x: 정규형 (레덱스 없음)
• x \; y: 정규형 (x가 추상화가 아니므로 레덱스 아님)
• (\lambda x. x) \; y: 정규형이 아님 (베타 레덱스 존재)

2.2 정규형의 부재

모든 람다 항이 정규형을 갖는 것은 아니다. 대표적 예:

\Omega = (\lambda x. x \; x) \; (\lambda x. x \; x)

\Omega에 베타 축약을 적용하면:

(\lambda x. x \; x) \; (\lambda x. x \; x) \rightarrow_\beta (\lambda x. x \; x) \; (\lambda x. x \; x) = \Omega

축약 결과가 원래 항과 동일하므로, \Omega는 무한히 자기 자신으로 축약된다. \Omega는 정규형을 갖지 않으며, 이는 “비종료 계산(Non-Terminating Computation)“의 람다 대수적 표현이다.

3. 처치-로서 정리(Church-Rosser Theorem)

3.1 정리의 진술

처치-로서 정리(합류성 정리, Confluence Theorem): 람다 항 M에서 두 개의 축약 경로 M \rightarrow_\beta^* N_1과 M \rightarrow_\beta^* N_2가 존재하면, 어떤 람다 항 P가 존재하여 N_1 \rightarrow_\beta^* P이고 N_2 \rightarrow_\beta^* P이다.

\text{If } M \rightarrow_\beta^* N_1 \text{ and } M \rightarrow_\beta^* N_2, \text{ then } \exists P: N_1 \rightarrow_\beta^* P \text{ and } N_2 \rightarrow_\beta^* P

의의

처치-로서 정리의 핵심적 귀결: 정규형이 존재하면 유일하다(알파 동치까지). 즉, 서로 다른 축약 경로를 통해 도달하는 정규형은 동일하다. 이는 람다 대수에서의 계산 결과가 축약 전략에 독립적임을 보장한다.

정규화 정리

정규화 정리: 항 M이 정규형을 가지면, 정상 순서 축약은 반드시 그 정규형에 도달한다.

이 정리는 정상 순서 축약이 “완전한(Complete)” 축약 전략임을 보장한다: 정규형이 존재하면 정상 순서로 반드시 찾을 수 있다. 다른 축약 전략(예: 적용 순서)은 정규형이 존재함에도 무한 축약에 빠질 수 있다.

베타 축약과 계산의 대응

베타 축약은 함수 호출의 추상적 모델이다. 프로그래밍 언어에서 함수 호출 시 매개변수에 실제 인자를 대입하는 과정은 베타 축약의 직접적 구현이다.

베타 축약은 람다 대수의 유일한 계산 메커니즘이며, 이 단일 규칙만으로 임의의 계산 가능 함수를 표현하고 계산할 수 있다.