커리–하워드 대응(Curry–Howard correspondence)

다음 함수를 봅시다. $\lambda f{:}A{\to}B.\;\lambda g{:}B{\to}C.\;\lambda x{:}A.\;g\,(f\,x)$. A를 B로 바꾸는 f와 B를 C로 바꾸는 g를 받아, A가 들어오면 f 다음 g를 거쳐 C를 내놓습니다. 단순 타입 람다 계산⁠(simply typed lambda calculus)⁠의 규칙으로 따지면 타입은 $(A \to B) \to (B \to C) \to (A \to C)$입니다. 이제 화살표를 '이면'으로 읽어 봅시다. 'A이면 B이고, B이면 C라면, A이면 C이다.' 논리 시간에 배우는 삼단논법(가언 삼단논법⁠, hypothetical syllogism⁠)입니다. 함수는 이 명제의 증명을 담고 있습니다. A의 증명 x가 주어지면 f로 B의 증명 $f\,x$를 얻고, g로 C의 증명 $g\,(f\,x)$를 얻습니다. 명제는 타입이고, 증명은 그 타입의 프로그램입니다.

이것은 비유가 아니라 규칙 하나하나의 일치입니다. 타입 규칙에서 항을 지우고 타입만 남기면 자연 연역(독일 논리학자 게르하르트 겐첸이 1934–35년에 내놓은, 가정을 세우고 내려놓으며 추론하는 증명 체계)의 규칙이 됩니다. Var는 '가정한 것은 쓸 수 있다', App은 'A → B와 A에서 B'(전건 긍정⁠, modus ponens⁠), Abs는 'A를 가정해 B를 얻으면, 가정을 내려놓고 A → B'(→ 도입)입니다. 아래 그림은 같은 유도를 두 가지로 읽게 해 줍니다.

증명할 명제: , 읽는 법:

대응은 '이면'에서 멈추지 않습니다. 논리의 연결사마다 타입을 만드는 방법이 하나씩 짝지어집니다.

$$\begin{array}{l|l|l|l} \text{논리} & \text{타입} & \text{증명을 만드는 법} & \text{증명을 쓰는 법} \\ \hline A \Rightarrow B & A \to B & \lambda x.\,M & M\,N \\ A \land B & A \times B & (a,\, b) & \mathsf{fst}\,p,\;\mathsf{snd}\,p \\ A \lor B & A + B & \mathsf{inl}\,a,\;\mathsf{inr}\,b & \text{경우 나누기} \\ \top & 1 & () & \text{쓸 것 없음} \\ \bot & 0 & \text{없음} & 0 \to C \\ \lnot A & A \to 0 & \lambda x.\,M & M\,a \\ \forall x{:}D.\;P(x) & \Pi_{x:D}\,P(x) & \lambda x.\,M & M\,d \\ \exists x{:}D.\;P(x) & \Sigma_{x:D}\,P(x) & (d,\, p) & \text{증인과 증명을 꺼냄} \end{array}$$

한 줄씩 읽으면 증명이 무엇인지에 대한 하나의 답이 됩니다. 'A 그리고 B'의 증명은 A의 증명과 B의 증명의 쌍입니다. 'A 또는 B'의 증명은 둘 중 하나의 증명에, 어느 쪽인지 알려 주는 꼬리표(inl 또는 inr)를 붙인 것입니다. 거짓 ⊥은 원소⁠(element)⁠가 하나도 없는 빈 타입⁠(empty type)⁠이라 증명이 없습니다. 대신 빈 타입에서 아무 타입 C로 가는 함수는 늘 하나 있어서, 거짓에서는 무엇이든 나온다는 원리가 됩니다. '아니다' ¬A는 따로 두지 않고 $A \to \bot$, 곧 'A의 증명이 오면 거짓을 만들어 내는 함수'로 정의합니다. 마지막 두 줄에서 명제 P(x)는 x에 따라 달라지는 타입이 되는데, 이런 타입이 의존 타입⁠(dependent type)⁠입니다. '모든 x에 대해 P(x)'의 증명은 x를 받아 P(x)의 증명을 돌려주는 함수이고, 'P(x)인 x가 있다'의 증명은 그런 x(증인)와 P(x)의 증명의 쌍입니다.

몇 가지를 직접 짜 봅시다. $A \land B \to B \land A$의 증명은 $\lambda p.\,(\mathsf{snd}\,p,\,\mathsf{fst}\,p)$로, 쌍의 순서를 바꾸는 함수입니다. $(A \land B \to C) \Leftrightarrow (A \to B \to C)$는 두 인자를 한꺼번에 받는 함수와 하나씩 받는 함수를 서로 바꾸는 변환이며, '커링⁠(currying)⁠'이라는 이름은 해스켈 커리에게서 왔습니다. $A \to \lnot\lnot A$는 $\lambda a.\,\lambda k.\,k\,a$입니다. 'A가 있는데 A를 반박하는 k가 오면, k에 a를 넣어 거짓을 만든다.' 거꾸로 $\lnot\lnot A \to A$(A는 아무 명제)에는 이 체계 안에서 아무리 애써도 프로그램이 나오지 않습니다. A를 반박할 수 없다는 사실만으로는 A의 증명을 만들어 낼 재료가 없기 때문입니다. '애써도 안 된다'를 엄밀하게 보이는 방법은 직관주의 논리⁠(intuitionistic logic)⁠의 크립키 모형입니다. 이것이 대응에서 나오는 논리가 고전 논리가 아니라 직관주의 논리인 이유입니다. 그러나 $\lnot\lnot(A \lor \lnot A)$는 프로그램이 있습니다. 그림에서 마지막 명제를 골라 보세요.

대응의 둘째 절반은 계산입니다. 증명 안에서 → 도입으로 A → B를 만들어 놓고 바로 다음 줄에서 → 제거로 A를 넣어 B를 꺼낸다면, 그것은 돌아가는 길입니다. 처음부터 A의 증명을 가정 자리에 끼워 넣으면 됩니다. 프로그램으로는 $(\lambda x.\,M)\,N$을 $M[x := N]$으로 바꾸는 β-축약⁠(β-reduction)⁠과 정확히 같습니다. 스웨덴 논리학자 다그 프라비츠는 1965년 자연 연역⁠(natural deduction)⁠의 증명에서 이런 돌아가는 길을 모두 없앨 수 있음을 보였는데(정규화), '이면'만 쓰는 부분에서 이것은 단순 타입 람다 계산의 정규화 정리⁠(normalization theorem)⁠와 같은 내용입니다. 여기서 무모순성⁠(consistency)⁠이 따라 나옵니다. 가정 없이 돌아가는 길도 없는 증명은 마지막 줄이 도입 규칙이어야 하는데, ⊥에는 도입 규칙이 없습니다. 그러니 ⊥의 닫힌 증명은 없습니다. 반대로 끝나지 않는 되부름 $\mathrm{fix} : (A \to A) \to A$를 넣으면 $\mathrm{fix}\,(\lambda x.\,x) : \bot$이 생겨 논리가 무너집니다. 이 체계에서는 모든 프로그램이 끝난다는 사실이 논리의 무모순성을 보증하고, 끝나지 않는 되부름을 허락하는 순간 그 보증이 사라집니다.

역사는 두 단계입니다. 미국 논리학자 해스켈 커리는 1934년 조합자⁠(combinator)⁠ 논리의 기본 함수 K와 S의 타입 $A \to B \to A$, $(A \to B \to C) \to (A \to B) \to A \to C$가 힐베르트식 명제 논리⁠(propositional logic)⁠의 두 공리⁠(axiom)⁠와 똑같고, 함수 적용이 전건 긍정과 같다는 것을 알아차렸습니다. 미국 논리학자 윌리엄 하워드는 1969년에 쓰고 돌려 읽다가 1980년에야 출판한 원고에서 이것을 자연 연역과 람다 계산⁠(lambda calculus)⁠으로 옮기고, '그리고'·'또는'·'모든'·'있다'까지 넓히며, 증명의 정규화가 항의 축약이라는 점을 적었습니다. 비슷한 시기 네덜란드의 N. G. 더 브라위언은 수학 증명을 기계로 검사하려고 만든 Automath(1967)에서 같은 생각을 따로 썼습니다. 1960년대 말부터 캐나다의 요아힘 람베크가 여기에 데카르트 닫힌 범주⁠(cartesian closed category)⁠를 셋째 기둥으로 더해, 커리–하워드–람베크 대응이라고도 부릅니다.

고전 논리에는 계산이 없을까요? 1990년 티머시 그리핀은 '지금까지의 계산의 나머지'(연속, continuation)를 값으로 붙잡아 나중에 그 자리로 뛰어 돌아가게 하는 연산자⁠(operator)⁠ call/cc에 $((A \to B) \to A) \to A$라는 타입을 줄 수 있음을 보였습니다. 이것은 고전 논리에서만 성립하는 퍼스의 법칙입니다. 고전 논리의 증명도 계산을 담지만, 그 계산에는 되돌아가 다른 답을 내는 '점프'가 끼어듭니다. 고전 명제를 이중 부정으로 감싸 직관주의⁠(intuitionism)⁠ 명제로 옮기는 변환은 프로그램으로는 모든 함수가 '결과를 넘겨줄 곳'을 인자로 받게 고쳐 쓰는 연속 전달 방식⁠(continuation-passing style)⁠ 변환에 해당합니다.

오해 셋을 짚어 둡니다. 첫째, 모든 프로그램이 흥미로운 증명은 아닙니다. 정수⁠(integer)⁠를 받아 정수를 돌려주는 프로그램은 '정수가 있으면 정수가 있다'를 증명할 뿐입니다. 타입이 무엇을 말할 수 있는지가 증명의 내용을 정하고, 흥미로운 정리는 의존 타입처럼 표현력이 큰 체계에서 나옵니다. 둘째, 이것은 정리 하나가 아니라 체계 사이의 대응들의 묶음입니다. 단순 타입 람다 계산은 직관주의 명제 논리의 '이면' 조각에, 시스템 F⁠(System F)⁠는 2차 명제 논리에, 의존 타입 체계는 술어 논리⁠(predicate logic)⁠에, 지라르의 선형 논리(1987)는 자원을 정확히 한 번씩 쓰는 언어에 대응합니다. 셋째, 같은 명제에 서로 다른 증명이 있을 수 있고, 여기서는 그 차이가 프로그램의 차이로 보입니다. A가 기본 타입일 때 $A \to A \to A$의 증명은 더 줄일 곳이 없는 꼴로 따지면 $\lambda x.\,\lambda y.\,x$와 $\lambda x.\,\lambda y.\,y$ 둘이고, 둘은 다른 함수입니다.

이어지는 곳. 증명이 곧 구성이라는 생각의 철학적 뿌리와, 배중률⁠(law of excluded middle)⁠에 프로그램이 없다는 것을 엄밀하게 보이는 방법(크립키 모형⁠, Kripke model⁠)은 직관주의 논리에 있습니다. 표의 마지막 두 줄을 실제로 쓰려면 타입이 값에 의존해야 하며, 그것이 의존 타입과 수학적 귀납법⁠(mathematical induction)⁠을 되부름 프로그램으로 쓰는 방법입니다. 이 대응을 도구로 만든 것이 증명 보조기⁠(proof assistant)⁠이고, Coq(Rocq)와 Lean에서 증명을 검사하는 일은 타입 검사입니다. 합과 곱을 논리 대신 개수로 읽으면 대수적 자료형⁠(algebraic data type)⁠의 셈이 나옵니다. 곱과 함수 타입이 이루는 구조를 대상과 화살표만으로 적으면 데카르트 닫힌 범주가 되고, 부작용이 있는 계산을 타입으로 다루는 모나드⁠(monad)⁠도 같은 줄기에서 나왔습니다. 증명을 기계적으로 검사할 수 있게 된다고 해서 모든 참을 증명할 수 있게 되지는 않는다는 한계는 괴델의 불완전성 정리⁠(Gödel's incompleteness theorems)⁠가 말해 줍니다. 가정을 버리거나 복사하는 규칙을 뺀 선형 람다 항과 증명의 대응은 선형 논리⁠(linear logic)⁠에서, '재귀⁠(recursion)⁠로 정의한 프로그램'과 '귀납법으로 한 증명'이 같은 것이라는 관점은 시작 대수에서 이어집니다.