처치-로서 정리

처치-로서 정리(Church–Rosser theorem)는 두 개의 특별한 재작성이 동일한 람다 대수항으로부터 시작한다면, 해당 항으로부터 재작성을 거듭하면 결국 어느 하나의 항 표현에 도달한다는 사실을 주장한다. 이는 우측의 그림으로 도식화되어 있다. a 항이 b와 c로 재작성 가능하다면 d(이는 근본적으로 b랑 c와 동일하다)는 b와 c로 재작성 가능하다.

추상 재작성 시스템 상에서의 람다 대수 상에서 처치-로서 정리는 합류성 정리이다. 정리를 거듭해보면 람다 대수의 한 항은 최소한 하나의 표준 형식을 가지게 되어 있다. 이는 해당 표준 형식의 특정 형태라는 걸 증명함으로써 가능하다. 이 정리는 알론조 처치와 존 버클리 로서에 의해 1936년 증명되었다.

처치-로서 정리는 또한 람다 대수의 많은 변형을 가져오는데 단순한 타입 기반 람다 대수(simply-typed lambda calculus), 고급 타입 시스템의 기초가 되는 수많은 정리, 그리고 고든 프로킨(Gordon Plotkin)의 베타-값 대수와 같은 것이 있다. 프로킨은 처치-로서 정리를 필요한 대로의 계산(lazy evaluation)이나 성급한 계산(eager evaluation)과 같은 함수형 프로그래밍 기법의 계산 방식이 람다 대수를 통해 가능함을 증명하는데 사용했다.

참고 자료

• Alonzo Church and J. Barkley Rosser. "Some properties of conversion". Transactions of the American Mathematical Society, vol. 39, No. 3. (May 1936), pp. 472–482.