처치-로서 정리

1. 개요

처치-로서 정리는 람다 계산에서 항의 축약에 관한 정리로, 1936년 앨런조 처치와 J. 바클리 로서에 의해 증명되었다. 이 정리는 순수 무형 람다 계산에서 β-축약과 같은 특정 축약 규칙에 적용되며, 축약된 두 항이 공통 항으로 축약되어야 함을 의미한다. 처치-로서 정리는 다이아몬드 속성을 만족하는 관계를 이용하여 증명되며, 정규화를 통해 항이 최대 하나의 정규형을 갖도록 한다. 또한, 단순 타입 람다 계산과 같은 람다 계산의 변형에도 적용되며, 함수형 프로그래밍 평가의 특성을 증명하는 데 사용되기도 한다.

2. 역사

1936년, 앨런조 처치와 J. 바클리 로서는 β-축약에 대해 처치-로서 정리가 성립함을 증명하였다. 이 증명 방법은 "전개 유한성"으로 알려져 있다. 1965년 D. E. 슈로어는 순수 비형식 람다 계산에 대한 결과를 증명하였다.

3. 순수 무형 람다 계산 (Pure untyped lambda calculus)

순수 무형 람다 계산에서 처치-로서 정리가 적용되는 한 유형의 축약은 β-축약이며, 이는 $(\; \backslash lambda\; x\; .\; t)\; s$ 형태의 하위 항을 $t\; [\; x\; :=\; s]$로 치환하여 축약하는 것이다. β-축약을 $\backslash rightarrow\_\backslash beta$로, 그리고 그 반사적, 전이적 폐쇄를 $\backslash twoheadrightarrow\_\backslash beta$로 나타내면 처치-로서 정리는 다음과 같다:

:$\backslash forall\; M,\; N\_1,\; N\_2\; \backslash in\; \backslash Lambda:\; \backslash text\{if\}\backslash \; M\backslash twoheadrightarrow\_\backslash beta\; N\_1\; \backslash \; \backslash text\{and\}\backslash \; M\backslash twoheadrightarrow\_\backslash beta\; N\_2\; \backslash \; \backslash text\{then\}\backslash \; \backslash exists\; X\backslash in\; \backslash Lambda:\; N\_1\backslash twoheadrightarrow\_\backslash beta\; X\; \backslash \; \backslash text\{and\}\backslash \; N\_2\backslash twoheadrightarrow\_\backslash beta\; X$

이 속성의 결과는 $\backslash lambda\backslash beta$에서 같은 두 항은 공통 항으로 축약되어야 한다는 것이다.

:$\backslash forall\; M,\; N\backslash in\; \backslash Lambda:\; \backslash text\{if\}\backslash \; \backslash lambda\backslash beta\; \backslash vdash\; M=N\; \backslash \; \backslash text\{then\}\backslash \; \backslash exists\; X:\; M\; \backslash twoheadrightarrow\_\backslash beta\; X\; \backslash \; \backslash text\{and\}\backslash \; N\backslash twoheadrightarrow\_\backslash beta\; X$

이 정리는 $\backslash lambda\; x.Sx$ 하위 항을 $S$로 대체하는 η-축약에도 적용된다. 또한 두 축약 규칙의 합집합인 βη-축약에도 적용된다.

3.1. 증명

윌리엄 W. 테이트와 페르 마틴-뢰프는 β-축약을 위한 증명 방법을 제시했다. 이 방법은 다이아몬드 속성을 만족하는 관계를 통해 처치-로서 속성을 증명한다. η-축약 규칙은 직접 처치-로서 속성을 갖는 것으로 증명될 수 있다.

먼저, 이항 관계 $\backslash rightarrow$가 다음 다이아몬드 속성을 만족한다고 가정한다.

:$\backslash forall\; M,\; N\_1,\; N\_2\; \backslash in\; \backslash Lambda:\; \backslash text\{if\}\backslash \; M\backslash rightarrow\; N\_1\; \backslash \; \backslash text\{and\}\backslash \; M\backslash rightarrow\; N\_2\; \backslash \; \backslash text\{then\}\backslash \; \backslash exists\; X\backslash in\; \backslash Lambda:\; N\_1\backslash rightarrow\; X\; \backslash \; \backslash text\{and\}\backslash \; N\_2\backslash rightarrow\; X$

그러면 처치-로서 속성은 $\backslash twoheadrightarrow\_\backslash beta$가 다이아몬드 속성을 만족한다는 명제이다. 이를 증명하기 위해 반사적 추이적 폐쇄가 $\backslash twoheadrightarrow\_\backslash beta$이고 다이아몬드 속성을 만족하는 새로운 축약 $\backslash rightarrow\_\{\backslash |\}$를 도입한다. 축약 단계 수에 대한 귀납법을 통해 $\backslash twoheadrightarrow\_\backslash beta$가 다이아몬드 속성을 만족한다는 결론을 얻는다.

관계 $\backslash rightarrow\_\{\backslash |\}$는 다음 규칙을 따른다.

* $M\; \backslash rightarrow\_\{\backslash |\}\; M$
* 만약 $M\; \backslash rightarrow\_\{\backslash |\}\; M\text{'}$이고 $N\; \backslash rightarrow\_\{\backslash |\}\; N\text{'}$이면, $\backslash lambda\; x.M\; \backslash rightarrow\_\{\backslash |\}\; \backslash lambda\; x.M\text{'}$이고 $MN\; \backslash rightarrow\_\{\backslash |\}\; M\text{'}N\text{'}$이며 $(\backslash lambda\; x.\; M)N\; \backslash rightarrow\_\{\backslash |\}\; M\text{'}[x:=N\text{'}]$이다.

또한, β-축약과 η-축약은 서로 교환 가능하다. 즉, 만약 $M\; \backslash rightarrow\_\backslash beta\; N\_1$이고 $M\; \backslash rightarrow\_\backslash eta\; N\_2$이면, $N\_1\; \backslash rightarrow\_\backslash eta\; X$이고 $N\_2\backslash rightarrow\_\backslash beta\; X$를 만족하는 항 $X$가 존재한다.

따라서 βη-축약은 처치-로서 속성을 갖는다고 결론 내릴 수 있다.

4. 정규화 (Normalisation)

처치-로서 성질을 만족하는 축약 규칙은 모든 항 M이 최대 하나의 서로 다른 정규형을 가질 수 있다는 성질을 갖는다. 만약 X와 Y가 M의 정규형이라면, 처치-로서 성질에 의해 둘 다 동일한 항 Z로 축약된다. 두 항 모두 이미 정규형이므로 $X=Z=Y$이다.

축약이 강하게 정규화되면(무한한 축약 경로는 없음) 처치-로서 성질의 약한 형태가 전체 성질을 함축한다(뉴먼의 보조정리 참조). 관계 $\backslash rightarrow$에 대한 약한 성질은 다음과 같다.

:$\backslash forall\; M,\; N\_1,\; N\_2\backslash in\; \backslash Lambda:$ 만약 $M\backslash rightarrow\; N\_1$이고 $M\backslash rightarrow\; N\_2$라면, $N\_1\backslash twoheadrightarrow\; X$이고 $N\_2\; \backslash twoheadrightarrow\; X$를 만족하는 항 $X$가 존재한다.

5. 변형 (Variants)

처치-로서 정리는 단순 타입 람다 계산, 고급 타입 시스템을 갖춘 계산법, 그리고 고든 플롯킨의 베타-값 계산법과 같은 람다 계산법의 많은 변형에도 적용된다. 고든 플롯킨은 처치-로서 정리를 사용하여 함수형 프로그래밍의 평가가 ( 느긋한 계산법과 조급한 계산법 모두에 대해) 프로그램에서 값으로의 함수(람다 항의 부분 집합)임을 증명했다.

과거 연구 논문에서는, 재작성 시스템이 합류할 때 처치-로서라고 하거나 처치-로서 속성을 갖는다고 말한다.

6. 같이 보기

합류