4.8 정규형(Normal Form)과 처치-로서 정리(Church-Rosser Theorem)

1. 정규형의 정의

1.1 베타 정규형(β-Normal Form)

람다 항 $M$ 이 베타 정규형(β-Normal Form, β-NF)에 있다 함은, $M$ 내에 베타 레덱스(Beta Redex)가 존재하지 않음을 의미한다. 베타 레덱스란 $(\lambda x. P) \; Q$ 형태의 부분항으로, 베타 축약이 적용 가능한 위치이다.

정규형의 예시:

$x$ , $y$ , $\lambda x. x$ , $x \; y$ , $\lambda x. x \; y \; z$ : 정규형
$(\lambda x. x) \; y$ : 정규형 아님 (레덱스 존재)

1.2 헤드 정규형(Head Normal Form, HNF)

람다 항 $M$ 이 헤드 정규형에 있다 함은, $M$ 이 다음 형태임을 의미한다:

$\lambda x_1. \lambda x_2. \cdots \lambda x_n. y \; M_1 \; M_2 \; \cdots \; M_k$

여기서 $y$ 는 변수이고, $n \geq 0$ , $k \geq 0$ 이다. 가장 바깥쪽의 헤드 위치에 레덱스가 없는 것이 핵심이며, $M_i$ 내부에는 레덱스가 존재할 수 있다.

약한 헤드 정규형(Weak Head Normal Form, WHNF)

약한 헤드 정규형은 다음 중 하나의 형태이다:

$\lambda x. M$ (추상화)
$x \; M_1 \; \cdots \; M_k$ ( $x$ 가 변수)

WHNF는 최외곽이 추상화이거나, 변수에 대한 적용인 경우이다. 대부분의 함수형 프로그래밍 언어에서 느긋한 평가(Lazy Evaluation)가 도달하는 형태이다.

정규형의 존재와 부재

정규형을 갖는 항

$(\lambda x. x) \; a \rightarrow_\beta a$

$(\lambda x. x) \; a$ 는 정규형 $a$ 를 갖는다.

$(\lambda x. \lambda y. x) \; a \; b \rightarrow_\beta (\lambda y. a) \; b \rightarrow_\beta a$

정규형: $a$ .

정규형을 갖지 않는 항

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

$\Omega$ 는 무한히 자기 자신으로 축약되며 정규형에 도달하지 않는다.

1.3 정규형을 갖지만 비종료 경로도 존재하는 항

$(\lambda x. \lambda y. y) \; \Omega$

이 항에서 두 가지 축약 전략이 가능하다:

외부 레덱스 우선: $(\lambda x. \lambda y. y) \; \Omega \rightarrow_\beta \lambda y. y$ (정규형 도달)
내부 레덱스( $\Omega$ ) 우선: $(\lambda x. \lambda y. y) \; \Omega \rightarrow (\lambda x. \lambda y. y) \; \Omega \rightarrow \cdots$ (비종료)

이 예시는 축약 전략의 선택이 정규형 도달 여부에 영향을 미칠 수 있음을 보여준다.

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

정리의 진술

처치-로서 정리 (합류성, Confluence):

만약 $M \rightarrow_\beta^* N_1$ 이고 $M \rightarrow_\beta^* N_2$ 이면, 어떤 항 $P$ 가 존재하여 $N_1 \rightarrow_\beta^* P$ 이고 $N_2 \rightarrow_\beta^* P$ 이다.

다이어그램으로 표현:

$\begin{array}{ccc} & M & \\ \swarrow & & \searrow \\ N_1 & & N_2 \\ \searrow & & \swarrow \\ & P & \end{array}$

증명의 역사

처치와 로서(J. Barkley Rosser)가 1936년 “Some Properties of Conversion“에서 이 정리를 최초로 증명하였다. 원래 증명은 복잡하였으나, 이후 타카하시(M. Takahashi, 1995)가 병렬 축약(Parallel Reduction)을 사용한 간결한 증명을 제시하였다.

핵심적 귀결

귀결 1: 정규형의 유일성

만약 $M \rightarrow_\beta^* N_1$ 과 $M \rightarrow_\beta^* N_2$ 에서 $N_1$ 과 $N_2$ 가 모두 정규형이면, $N_1 \equiv_\alpha N_2$ (알파 동치)이다.

증명: 처치-로서 정리에 의해 $N_1 \rightarrow_\beta^* P$ 와 $N_2 \rightarrow_\beta^* P$ 인 $P$ 가 존재한다. $N_1$ 과 $N_2$ 가 정규형이므로 더 이상 축약이 불가능하다. 따라서 $N_1 = P = N_2$ (알파 동치까지).

이 결과는 계산의 결과가 축약 전략에 독립적임을 보장한다.

귀결 2: 베타 동치의 판정

$M =_\beta N$ ( $M$ 과 $N$ 이 베타 동치)이고, 두 항이 정규형을 가지면, 각각의 정규형을 계산하여 비교함으로써 동치 여부를 판정할 수 있다.

정규화 정리(Normalization Theorem)

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

이 정리는 정상 순서 축약이 정규화에 대해 완전(Complete)한 전략임을 보장한다. 즉, 정규형이 존재하는 경우 정상 순서를 따르면 반드시 찾을 수 있다.

강정규화(Strong Normalization)와 약정규화(Weak Normalization)

강정규화

항 $M$ 이 강정규화(Strongly Normalizing)라 함은, $M$ 에서 시작하는 모든 축약 열이 유한함을 의미한다. 즉, 어떤 축약 전략을 사용하든 반드시 정규형에 도달한다.

순수 람다 대수(유형 없는 람다 대수)는 강정규화하지 않는다. $\Omega$ 와 같은 비종료 항이 존재하기 때문이다.

약정규화

항 $M$ 이 약정규화(Weakly Normalizing)라 함은, $M$ 에서 시작하는 적어도 하나의 축약 열이 정규형에 도달함을 의미한다. 이는 정규형으로 이끄는 경로가 존재하되, 다른 경로는 비종료일 수 있음을 의미한다.

단순 유형 람다 대수의 강정규화

유형이 부여된 단순 유형 람다 대수(Simply Typed Lambda Calculus)에서는 모든 유형 가능(Typeable)한 항이 강정규화한다. 이는 유형 시스템이 비종료 계산을 배제하는 효과를 가짐을 의미한다.

정규형과 처치-로서 정리의 계산 이론적 의의

정규형은 “계산의 최종 결과“의 형식적 정의이며, 처치-로서 정리는 “이 결과가 유일하다“는 보장이다. 이 두 결과는 람다 대수가 일관된(Consistent) 계산 체계임을 확정하며, 이 일관성이 람다 대수를 계산 가능성의 형식적 정의로 사용할 수 있는 기반이다.