정의
커리-하워드 대응(Curry–Howard correspondence)은 수리논리학과 프로그래밍 언어 이론에서 핵심적인 개념으로, 증명과 프로그램 사이의 구조적 유사성을 형식적으로 나타내는 원리이다. 이 대응 관계는 특정한 논리 체계의 증명이 함수형 프로그래밍 언어의 프로그램으로, 논리 명제가 타입으로 해석될 수 있음을 보여준다. 이를 흔히 "증명은 프로그램이며, 증명은 그 프로그램의 타입 검사이다(proofs as programs, propositions as types)"라고 요약한다.
개요
커리-하워드 대응은 직관주의 명제 논리(intuitionistic propositional logic)와 단순 타입 람다 계산(simple type lambda calculus) 사이의 일대일 대응을 기반으로 한다. 이에 따르면, 어떤 명제를 증명하는 과정은 해당 명제를 타입으로 갖는 프로그램(람다 항)을 구성하는 것과 동등하다. 예를 들어, 논리적 함축 $ A \to B $는 함수 타입 $ A \Rightarrow B $에 대응하며, 이 타입의 값을 만드는 람다 항은 $ A $에서 $ B $로의 추론을 구현한다. 이 대응은 이후 직관주의 술어 논리, 직교형 이론, 형 이론(type theory) 등으로 확장되어, 군형 이론(ML 타입 이론), 코퀴르(coq), 애그다(Agda) 등의 정형 검증 시스템 개발에 큰 영향을 미쳤다.
어원/유래
이 대응 관계는 로버트 무어 커리(Robert Moorman Curry)가 1930년대에 수식된 컴비네이터 논리에서의 직관주의 논리와 함수 간의 관계에 대한 관찰에서 기원한다. 이후 1969년에 윌리엄 알빈 하워드(William Alvin Howard)가 람다 계산과 직관주의 명제 논리의 증명을 명시적으로 대응시킨 논문을 발표하면서, 이 관계는 체계적인 형태를 갖추게 되었다. 따라서 "커리-하워드 대응" 또는 "커리-하워드 동형사상(Curry–Howard isomorphism)"으로 불리게 되었다. 일부 문헌에서는 마틴-Löf의 직관주의 유형 이론에 대한 기여를 반영하여 "커리-하워드-마틴뢰프 대응"이라고 부르기도 한다.
특징
- 직관주의 논리와의 연결: 고전 논리가 아닌 직관주의 논리는 배중률이나 귀류법을 제한하는 대신, 증명 절차를 명시적으로 구성함으로써 프로그램으로의 해석을 가능하게 한다.
- 타입과 명제의 동치성: 명제가 타입에, 증명이 그 타입을 갖는 항(term)에 대응한다. 예를 들어, $ A \land B $는 곱 타입(product type), $ A \lor B $는 합 타입(sum type)으로 해석된다.
- 계산과 정규화: 증명의 절삭 제거(cut elimination)는 프로그램의 베타 축소(beta reduction)와 대응하며, 이는 정규 형태(normal form)에서 증명의 완전성과 프로그램의 종료를 의미한다.
- 확장 가능성: 단순 타입 외에도 의존 타입(dependent types), 다형성, 귀납 타입 등으로 확장되어 현대의 증명 검증기와 프로그래밍 언어에 활용된다.
관련 항목
- 직관주의 논리(Intuitionistic logic)
- 람다 계산(Lambda calculus)
- 형 이론(Type theory)
- 군형 이론(Martin-Löf type theory)
- 정형 검증(Formal verification)
- 코퀴르(Coq), 애그다(Agda) 등의 증명 보조기(proof assistant)