증명은 프로그램이다

러셀의 역설⁠(Russell's paradox)⁠을 막으려고 만든 '타입⁠(type)⁠'은 반세기 뒤 프로그램의 잘못을 미리 잡는 장치가 되었습니다. 그 사이 두 논리학자가 서로 다른 시기에, 명제를 타입으로, 증명을 프로그램으로 읽으면 두 체계가 규칙 하나하나까지 맞아떨어진다는 것을 알아챘습니다. 오늘날 수학자들은 그 사실을 이용해 컴퓨터에게 증명을 검사받습니다.

이 글의 처럼 점선이 그어진 숫자는 좌우로 끌 수 있고(키보드 ←/→도 됩니다), 색이 칠해진 같은 말은 눌러서 바꿀 수 있습니다. 글상자에는 프로그램을 직접 쓸 수 있고, 그 아래 나무에서 줄 하나에 마우스를 올리면 그 줄에 쓰인 규칙이 무슨 뜻인지 나옵니다. 그림 속 칸과 화살표에도 마우스를 올려 보세요. 휴대폰에서는 마우스를 올리는 대신 누르면 됩니다.

2005년 무렵, 영국 케임브리지의 마이크로소프트 연구소에서 일하던 컴퓨터 과학자 조르주 공티에는 프랑스 INRIA의 뱅자맹 베르네르와 함께 한 가지 작업을 마쳤다고 알렸습니다. 이웃한 나라끼리 색이 겹치지 않게 지도를 칠하는 데는 네 가지 색이면 충분하다는 4색 정리⁠(four color theorem)⁠의 증명 전체를, 컴퓨터가 한 줄도 빠짐없이 검사할 수 있는 꼴로 옮긴 것입니다. 1976년 케네스 아펠과 볼프강 하켄이 처음 내놓은 증명은 컴퓨터로 수많은 경우를 확인하는 계산에 기대고 있어서, 사람이 끝까지 따라가 검산하기 어렵다는 불만을 오래 들었습니다. 1979년 철학자 토머스 티모치코는 이 증명이 컴퓨터라는 실험 장치를 믿는 경험적 요소를 수학에 들여왔다고까지 주장했습니다(그 논쟁은 「일곱 다리의 도시」에서 4색 문제의 긴 역사와 함께 볼 수 있습니다). 1990년대에 로버트슨, 샌더스, 시모어, 토머스가 이 증명을 다듬었지만, 그 판도 컴퓨터 계산에 기대기는 마찬가지였습니다. 공티에가 옮긴 것은 이 다듬은 판이고, 그가 쓴 도구는 증명 보조기⁠(proof assistant)⁠ Coq였습니다. 증명 보조기는 사람이 적은 증명의 모든 단계가 규칙에 맞는지를 컴퓨터가 한 줄씩 검사하는 프로그램입니다.

그런데 Coq에게 증명은 글이 아닙니다. 프로그램입니다. 그리고 증명이 옳은지 검사하는 일은 그 프로그램의 타입이 맞는지 검사하는 일입니다. 타입은 프로그램이 무엇을 받아 무엇을 내놓는지를 적은 꼬리표입니다. 작은 예로 무슨 뜻인지 봅시다. "A 그리고 B이면, B 그리고 A이다"라는 명제가 있습니다. 한편 두 값의 쌍을 받아 순서를 바꿔 돌려주는 프로그램이 있습니다. (3, "사과")를 넣으면 ("사과", 3)이 나오는 프로그램입니다. 이 프로그램의 타입을 적으면 A × B → B × A입니다. 'A 값과 B 값의 쌍을 받아, B 값과 A 값의 쌍을 내놓는다'로 읽습니다. 이 타입에서 쌍(×)을 '그리고'로, 화살표(→)를 '이면'으로 바꿔 읽으면 앞의 명제가 되고, 프로그램은 그 명제의 증명으로 읽힙니다. 이것이 이 글의 이야기입니다.

질문을 정확히 적으면 이렇습니다. 증명을 쓰는 일과 프로그램을 쓰는 일이 정말 같은 일일 수 있을까? 같다면 정확히 무엇이 같은가? 답을 찾아가는 길에서 러셀의 역설, 무한을 믿지 않은 네덜란드의 수학자, 함수⁠(function)⁠만으로 이루어진 계산 체계, 한 논리학자의 복사본 원고, '자연스럽다'는 말을 정의하려던 두 수학자, 그리고 오늘날 스마트폰 앱을 만드는 프로그래밍 언어들을 만납니다. 그러면서 무엇이 증명된 정리이고 무엇이 철학적 입장인지를 구별하겠습니다. 커리–하워드 대응⁠(Curry–Howard correspondence)⁠은 정확히 정의된 두 체계 사이의 대응으로서 증명된 사실입니다. "수학은 곧 계산이다" 같은 말은 그 사실을 어디까지 밀고 갈지를 두고 취하는 입장입니다.

1 · 1902년 케임브리지층을 나눈 세계: 러셀의 타입

이 절의 물음은 이것입니다. 러셀의 역설은 "자기 자신을 원소⁠(element)⁠로 갖는가"라는 질문에서 나왔습니다. 그런 질문을 아예 할 수 없게 막으면 역설을 피할 수 있을까?

이야기는 한 통의 편지에서 시작합니다. 1902년 6월 케임브리지의 버트런드 러셀은 예나의 고틀로프 프레게에게, 산술을 논리만으로 세우려던 그의 체계에 모순이 있다고 알렸습니다. "자기 자신을 원소로 갖지 않는 집합⁠(set)⁠들의 집합"을 생각하면, 그 집합이 자기 자신의 원소인지 아닌지 어느 쪽으로 답해도 반대가 되어 버립니다(러셀의 역설). 이 편지의 사정과 모순을 손으로 만져 보는 그림은 「기계가 풀 수 없는 문제」 2절에 있습니다. 여기서는 그 뒤에 러셀이 내놓은 처방을 따라갑니다.

러셀은 1903년 『수학의 원리』의 부록에서 처방의 윤곽을 그렸고, 1908년 논문 「타입 이론⁠(type theory)⁠에 기초⁠(basics)⁠한 수리 논리」에서 그것을 체계로 만들었습니다. 생각은 이렇습니다. 세상의 것들을 층으로 나눕니다. 개별 대상(사람, 수)은 0층, 대상들의 집합은 1층, 1층 집합들의 집합은 2층입니다. 그리고 "$x$는 $y$의 원소이다"라는 문장은 $y$가 $x$보다 꼭 한 층 위에 있을 때만 쓸 수 있게 합니다. 그러면 "$x$는 $x$의 원소이다"는 참도 거짓도 아닌, 문법에 맞지 않는 문장이 됩니다. "자기 자신을 원소로 갖지 않는 집합들의 집합"은 처음부터 말할 수 없는 것이 되고, 역설은 생기지 않습니다. 층 하나하나를 러셀은 '타입'이라고 불렀습니다.

이 처방이 오늘날의 타입 이론의 씨앗입니다. 핵심은 '틀린 말'과 '뜻이 없는 말'을 가르는 데 있습니다. 프로그래밍 언어로 옮기면 쉽게 느낄 수 있습니다. "사과"의 길이 + 1은 뜻이 있는 식이고 값은 3입니다. 5의 길이는 틀린 값을 내는 식이 아니라 뜻이 없는 식입니다. 수에는 '길이'가 없으니까요. 타입을 검사하는 언어는 이런 식을 실행하기도 전에 거부합니다. 모든 잘못을 막지는 못합니다. 0으로 나누는 일은 보통의 타입으로는 막을 수 없습니다. 하지만 한 무리의 잘못을 문법 오류로 바꾸어, 실행해 보지 않고도 찾게 해 줍니다.

정리하면, 타입은 '거짓인 문장'이 아니라 '말이 안 되는 문장'을 미리 걸러 내는 문법입니다.

러셀의 체계는 실제로는 훨씬 복잡했습니다. 1906년 무렵 푸앵카레는 역설들의 공통 원인으로 '악순환', 곧 어떤 것을 그것이 속한 전체를 통해 정의하는 일을 지목했습니다. 러셀은 이 악순환을 막으려고 층을 다시 잘게 쪼갠 분지 타입⁠(ramified type)⁠을 썼습니다. 같은 층 안에서도 '어떤 전체를 언급하며 정의했는가'에 따라 다시 층을 매긴 것입니다. 그러자 보통의 수학까지 너무 많이 막혀서, '환원 공리⁠(axiom of reducibility)⁠'라는 억지스러운 공리⁠(axiom)⁠를 덧붙여야 했습니다. 잘게 쪼갠 층을 결국 다시 합쳐 주는 공리입니다. 1910년부터 1913년까지 화이트헤드와 함께 낸 『수학 원리』 세 권이 이 체계 위에 서 있습니다.

1920년대에 폴란드의 레온 흐비스테크와 케임브리지의 프랭크 램지는 러셀의 역설 같은 집합의 역설을 막는 데는 단순한 층만으로 충분하다고 지적했습니다. 분지 타입이 겨냥한 나머지 역설, 곧 거짓말쟁이 역설⁠(liar paradox)⁠처럼 '말'과 '뜻'이 얽힌 역설은 논리가 아니라 언어의 문제로 따로 다루자는 것이었습니다. 이것이 뒤에 처치가 다시 다듬는 '단순 타입'입니다. 수학자들은 대부분 다른 길, 곧 1908년 체르멜로가 시작한 공리적 집합론⁠(axiomatic set theory)⁠을 택했습니다. 타입은 한동안 논리학자들의 관심사로 남았습니다.

『수학 원리』는 팔릴 책이 아니었습니다. 케임브리지 대학 출판부가 내다본 손실 600파운드 가운데 출판부가 300파운드를 떠맡고, 왕립학회가 200파운드를 보탰으며, 남은 100파운드는 화이트헤드와 러셀이 50파운드씩 냈습니다. "1 + 1 = 2"의 증명이 2권에 가서야 끝나는 이 책을 끝까지 읽은 사람은 드물었지만, 그 체계는 한 세대 뒤 결정적인 과녁이 되었습니다. 1931년 빈의 쿠르트 괴델이 발표한 불완전성 논문의 제목은 「『수학 원리』 및 관련 체계의 형식적으로 결정 불가능한 명제에 대하여 I」입니다. 러셀이 역설을 막으려고 쌓은 체계에도 참이지만 그 안에서 증명할 수 없는 문장이 있다는 것입니다. 체계가 자연수⁠(natural number)⁠의 산술을 담을 만큼 강하고 모순이 없는 한 그렇습니다. 그 문장을 만드는 방법은 「기계가 풀 수 없는 문제」 3절에 있습니다.

2 · 1907년 암스테르담증명은 만드는 법이다: 브라우어르와 BHK

이 절의 물음은 이것입니다. "무엇이 있다"를 증명했다면, 그것이 무엇인지도 알아야 할까? 이 물음에 "그렇다"고 답하면, 증명이란 무엇인가를 새로 정의하게 됩니다. 그 정의가 4절에서 프로그램과 만납니다.

러셀이 층을 나누던 무렵, 암스테르담의 L. E. J. 브라우어르는 전혀 다른 곳을 문제 삼았습니다. 1907년 박사 논문과 이듬해의 논문 「논리 원리의 불확실성」에서 그는, 수학은 사람의 마음이 한 걸음씩 해내는 구성이고 논리는 그 구성을 뒤따라 정리한 것일 뿐이라고 주장했습니다. 그렇다면 유한한 대상에서 얻은 논리 법칙을 무한한 대상에 그대로 쓸 수는 없습니다. 특히 '$A$이거나 $A$가 아니다'라는 배중률⁠(law of excluded middle)⁠을 의심했습니다. 이 입장을 직관주의⁠(intuitionism)⁠라고 부르고, 그 논리를 직관주의 논리⁠(intuitionistic logic)⁠라고 부릅니다.

무엇이 걸려 있는지 예로 봅시다. "무리수⁠(irrational number)⁠ $a, b$ 가운데 $a^b$가 유리수⁠(rational number)⁠가 되는 것이 있다"를 증명해 봅니다(무리수는 $\sqrt2$처럼 분수로 적을 수 없는 수입니다). $\sqrt2$는 무리수입니다. 이제 $\sqrt2^{\sqrt2}$를 생각합니다. 이 수는 유리수이거나 무리수이고, 두 경우를 나눠 봅니다.

이 수가 유리수라면 $a = b = \sqrt2$로 끝입니다. 무리수라면 $a = \sqrt2^{\sqrt2}$, $b = \sqrt2$로 둡니다. 거듭제곱을 다시 거듭제곱하면 지수끼리 곱해지므로($(x^y)^z = x^{yz}$) $a^b = \sqrt2^{\sqrt2 \cdot \sqrt2} = \sqrt2^{2} = 2$이니 역시 끝입니다. 어느 경우든 참이니 증명이 끝났습니다. 그런데 이 증명을 다 읽고도 우리는 어느 쌍이 답인지 모릅니다. $\sqrt2^{\sqrt2}$가 유리수인지 아닌지를 몰라도 되게 짜인 증명이기 때문입니다. (답은 1934년에야 겔폰트–슈나이더 정리⁠(Gelfond–Schneider theorem)⁠로 알려졌습니다. $\sqrt2^{\sqrt2}$는 무리수이고, 더 나아가 초월수⁠(transcendental number)⁠입니다.)

직관주의자라면 쌍을 실제로 내놓으라고 할 것입니다. 그런 증명도 있습니다. $\log_2 9$('로그 2의 9')는 2를 몇 제곱해야 9가 되는지를 나타내는 수, 곧 $2^{\log_2 9} = 9$인 수입니다(약 3.17). $a = \sqrt2$(곧 $2^{1/2}$), $b = \log_2 9$로 두면 $a^b = 2^{\frac12 \log_2 9} = 9^{1/2} = 3$입니다(가운데 등호는 $(2^{\log_2 9})^{1/2}$로 묶어 읽으면 보입니다).

$\log_2 9$가 무리수라는 것은 쉽게 확인됩니다. $\log_2 9 = p/q$라면 $2^p = 9^q$인데, 왼쪽은 짝수이고 오른쪽은 홀수입니다($p, q$는 양의 정수⁠(integer)⁠). 이 증명은 '있다'고 말하면서 그것이 무엇인지까지 건넵니다. 직관주의에서 증명이란 바로 이런 것, 곧 무언가를 만들어 건네는 방법입니다. 흔히 직관주의를 '첫째 증명이 틀렸다'는 주장으로 오해하지만, 직관주의자도 첫째 증명의 논리가 고전 논리에서 옳다는 것은 인정합니다. 다만 그것을 '있다'의 증명으로 받아들이지 않을 뿐입니다.

이 생각을 정확한 말로 옮긴 사람들이 있습니다. 규칙을 형식 체계⁠(formal system)⁠로 적는 일은 브라우어르 자신이 탐탁지 않아 한 일이라, 계기는 밖에서 왔습니다. 1927년 네덜란드 수학회가 직관주의 이론을 형식화하라는 현상 과제를 내걸었고, 이듬해 상을 받은 사람이 브라우어르의 제자 아런트 헤이팅이었습니다. 헤이팅은 그 글을 다듬어 1930년 직관주의 논리의 규칙을 형식 체계로 발표했습니다.

1932년 모스크바의 안드레이 콜모고로프는 헤이팅의 논리를 '과제의 논리'로 읽었습니다. "A를 증명하라"를 "A라는 과제를 풀어라"로 읽자는 것입니다. 두 사람(헤이팅과 콜모고로프)의 설명은 뒤에 브라우어르까지 세 사람의 이름을 따서 BHK 해석⁠(BHK interpretation)⁠이라 불리게 됩니다.

BHK 해석은 '그리고', '또는', '이면', '아니다' 같은 논리 낱말마다, 그 낱말이 든 명제의 증명이 어떤 물건이어야 하는지를 정합니다. 아래 목록의 기호는 처음 나올 때 괄호 안에 읽는 법을 적었습니다. $A$, $B$는 아무 명제나 들어갈 수 있는 빈칸입니다.

• $A \land B$(A 그리고 B)의 증명은 $A$의 증명과 $B$의 증명의 쌍입니다.
• $A \lor B$(A 또는 B)의 증명은 어느 쪽인지 알려 주는 꼬리표와 그쪽의 증명입니다.
• $A \to B$(A이면 B)의 증명은 $A$의 증명을 받아 $B$의 증명으로 바꾸는 방법입니다.
• $\bot$('바닥'이라 읽고, 모순을 뜻합니다)에는 증명이 없습니다. '$A$가 아니다'($\lnot A$, '낫 A')는 $A \to \bot$, 곧 $A$의 증명을 받으면 모순을 만들어 내는 방법입니다. "$A$의 증명이 나오면 모순이니, $A$의 증명은 있을 수 없다"는 뜻입니다.
• $P(x)$는 $x$에 관한 주장 하나, 예를 들어 "$x + 0 = x$"나 "$x$는 짝수이다"입니다. "모든 $x$에 대해 $P(x)$"의 증명은 $x$를 받아 $P(x)$의 증명을 내는 방법이고, "$P(x)$인 $x$가 있다"의 증명은 그런 $x$ 하나와 그것이 $P$를 만족한다는 증명의 쌍입니다. "짝수인 수가 있다"의 증명이라면 (4, "4 = 2 × 2")처럼 수와 확인의 쌍입니다.

한 줄씩 예를 들면 이렇습니다. "A 그리고 B이면 B 그리고 A"($A \land B \to B \land A$)의 증명은 셋째 줄에 따라 '방법'이어야 합니다. $A \land B$의 증명, 곧 쌍 (A의 증명, B의 증명)을 받아서 순서를 바꾼 쌍 (B의 증명, A의 증명)을 돌려주는 방법입니다. 머리말의 '순서를 바꾸는 프로그램'과 똑같습니다.

이 표에서 보면 배중률이 왜 문제인지 분명해집니다. $A \lor \lnot A$의 증명은 꼬리표를 달아야 하니, $A$가 성립하는지 아닌지를 실제로 판정해야 합니다. 모든 명제 $A$에 대해 그렇게 해 주는 방법은 우리에게 없고, 적어도 기계적인 방법은 있을 수 없다는 것이 증명되어 있습니다. 예를 들어 "이 프로그램은 언젠가 멈춘다"를 모든 프로그램에 대해 판정하는 알고리즘⁠(algorithm)⁠은 없다는 것이 튜링의 정리입니다(정지 문제⁠(halting problem)⁠). 다만 조심할 점이 있습니다. 직관주의자는 배중률이 틀렸다고 말하지 않습니다. 그것을 일반 원리로 쓰지 않을 뿐입니다. 실제로 "배중률이 틀렸다"($\lnot(A \lor \lnot A)$)는 직관주의 논리에서 반박됩니다. 곧 "배중률이 틀렸다"를 가정하면 모순이 나온다는 것을 배중률 없이 증명할 수 있습니다. 4절에서 직접 해 봅니다.

정리하면, BHK 해석에서 증명은 참이라는 판정이 아니라 만들어 건네는 물건입니다. '그리고'의 증명은 쌍, '이면'의 증명은 바꾸는 방법입니다.

이 표를 손에 들면, BHK보다 앞선 콜모고로프의 결과 하나를 읽을 수 있습니다. 1925년 콜모고로프는 스물두 살에 쓴 논문 「배중률에 관하여」에서 이미 두 논리 사이에 다리를 놓았습니다. 고전 논리에서 증명되는 식을 가져와, 그 식을 이루는 작은 식 하나하나(부분식) 앞에 '아니다'를 두 번 붙이면, 직관주의 논리에서도 증명되는 식이 된다는 것입니다(이중 부정 변환⁠, double-negation translation⁠). 'A'를 'A가 아니라는 것은 아니다'($\lnot\lnot A$)로 바꾸는 셈입니다.

'아니다'를 두 번 붙이면 왜 증명하기 쉬워질까요? $\lnot\lnot A$는 표에 따라 "$A$를 반박하는 방법을 받으면 모순을 만들어 내는 방법"입니다. $A$가 성립한다는 증거를 직접 내놓으라는 요구보다, "$A$를 반박하려는 시도는 모두 무너진다"를 보이라는 요구가 약합니다. 1929년 발레리 글리벤코는 '그리고, 또는, 이면, 아니다'만 쓰는 식(명제 논리⁠(propositional logic)⁠의 식)에서는 식 전체 앞에 한 번만 붙여도 된다는 것을 보였습니다. 배중률을 버려도 고전 수학이 통째로 사라지지는 않고, 이중 부정의 옷을 입고 남는다는 뜻입니다. 4절에서 $\lnot\lnot(A \lor \lnot A)$('A 또는 A가 아니다, 가 아니라는 것은 아니다')가 증명되는 것이 그 가장 작은 예입니다.

BHK 해석에는 빈 곳이 하나 있었습니다. '방법'이 무엇인지를 정하지 않은 것입니다. 받은 증명을 다른 증명으로 바꾸는 방법이란 결국 무엇일까요? 이 물음은 브라우어르와 힐베르트가 수학의 기초를 두고 벌인 논쟁(수학 기초론 논쟁⁠, debate on the foundations of mathematics⁠) 한가운데 있었고, 그 다툼은 「무한에도 크기가 있다」 7절에 있습니다. 답은 뜻밖에도 논리학이 아니라 계산의 이론에서 왔습니다.

브라우어르가 수학자로 이름을 얻은 것은 직관주의가 아니라 1909년부터 1913년 무렵까지의 위상수학⁠(topology)⁠ 연구 덕이었습니다. 오늘날 그의 이름이 붙은 고정점 정리⁠(fixed-point theorem)⁠, 곧 원판을 연속적으로 자기 자신 안으로 옮기면 제자리에 머무는 점이 반드시 있다는 정리가 그 가운데 하나입니다. 그런데 그 증명은 고정점⁠(fixed point)⁠이 있다고만 말할 뿐 어디 있는지는 알려 주지 않는 증명이었습니다. 위상수학자로 자리를 굳혀 1912년 암스테르담 대학의 교수가 된 뒤, 그는 1918년 무렵부터 배중률 없이 수학을 다시 세우는 일로 돌아갔고, 이런 종류의 증명을 스스로 받아들이지 않게 되었습니다. 그의 타협 없는 태도는 학계의 충돌로도 번졌습니다. 1928년 힐베르트가 그를 『수학 연보』의 편집진에서 빼자, 같은 편집진에 있던 아인슈타인은 이 다툼을 '개구리와 쥐의 전쟁'이라 부르며 거리를 두었습니다.

브라우어르의 직관주의는 철학에 뿌리를 두고 있었습니다. 칸트는 수학이 경험에 앞선 직관, 곧 공간과 시간의 직관 위에 서 있다고 보았습니다. 19세기에 비유클리드 기하⁠(non-Euclidean geometry)⁠가 나오자 공간에 관한 칸트의 생각은 지키기 어렵다는 평이 많았는데, 브라우어르는 1912년 암스테르담 대학의 취임 강연 「직관주의와 형식주의⁠(formalism)⁠」에서 공간의 직관은 버리고 시간의 직관을 더 굳게 붙들면 된다고 답했습니다. 한 순간이 둘로 갈라져 앞의 것이 뒤의 것에 자리를 내주면서도 기억에 남는 경험, 그것을 되풀이하는 데서 수가 나온다는 것입니다. 반대편의 힐베르트는 1927년 함부르크 강연에서, 수학자에게서 배중률을 빼앗는 것은 천문학자에게서 망원경을, 권투 선수에게서 주먹을 빼앗는 것과 같다고 맞섰습니다. 논쟁은 반세기 뒤 다른 모양으로 되살아났습니다. 1970년대 옥스퍼드의 철학자 마이클 더밋은 마음의 직관이 아니라 언어에서 출발했습니다. 문장의 뜻은 그 문장을 어떻게 쓰는지로 정해지고, 수학 문장을 이해한다는 것은 그 증명을 알아볼 줄 안다는 것이니, '참'을 '증명할 수 있음'으로 읽어야 하고 그러면 알맞은 논리는 직관주의 논리라는 것입니다. 이 주장에는 고전 논리를 지키는 쪽의 반론이 이어졌고, 논쟁은 아직 끝나지 않았습니다.

러셀의 편지에서 범주론⁠(category theory)⁠의 첫 논문까지. 무대가 케임브리지, 예나, 암스테르담, 모스크바에서 프린스턴과 미국 동부·중서부의 대학 도시로 옮겨 가는 것을 보세요. 철학 줄(보라)에는 직관주의가, 수학 줄(파랑)에는 타입과 람다 계산⁠(lambda calculus)⁠이 있습니다. 괴팅겐에서 프린스턴으로 간 노란 선은 쇤핑켈의 논문이 커리에게 닿은 길, 프라하로 간 분홍 선은 겐첸의 마지막 길입니다.

3 · 1936년 프린스턴처치의 λ, 그리고 타입이 붙은 λ

이 절의 물음은 이것입니다. 2절의 BHK 해석은 증명을 '방법'이라 했지만, 방법이 무엇인지는 정하지 않았습니다. 함수를 만들고 적용하는 규칙만으로 '방법'을 정확히 적을 수 있을까? 그리고 그 규칙에서도 러셀의 역설 같은 괴물이 나올까?

1930년대 초 프린스턴의 알론조 처치는 함수만으로 논리 전체를 세우려 했습니다. 1932–33년에 발표한 체계에서 가장 기본적인 것은 함수를 만드는 일과 함수를 적용하는 일 두 가지였습니다. "$x$를 받아 $x + 1$을 돌려주는 함수"를 $\lambda x.\, x + 1$로 적고, 이 함수를 2에 적용한 $(\lambda x.\, x + 1)\, 2$는 몸통의 $x$ 자리에 2를 넣어 $2 + 1 = 3$이 됩니다. 이렇게 넣어서 푸는 한 걸음을 β 축약⁠(beta reduction)⁠이라고 부릅니다. 이것이 람다 계산입니다. 함수가 함수를 받고 함수를 돌려줄 수 있어서, 수와 덧셈까지도 함수로 만들 수 있습니다.

1935년 처치의 학생 스티븐 클리니와 바클리 로서는 처치의 논리 체계 전체에 모순이 있음을 보였습니다. 살아남은 것은 논리 부분을 떼어 낸 순수한 계산 규칙, 곧 람다 계산이었습니다. 처치는 1936년 이것으로 '기계적으로 계산할 수 있다'는 말을 정의하고, 힐베르트의 결정 문제⁠(decision problem)⁠, 곧 어떤 명제가 증명되는지를 기계적으로 가려내는 방법이 있느냐는 물음에 처음으로 부정의 답을 냈습니다. 같은 해 케임브리지의 튜링은 전혀 다른 모양의 정의, 곧 튜링 기계⁠(Turing machine)⁠로 같은 답에 이르렀고, 두 정의가 같은 함수들을 계산한다는 것이 곧 증명되었습니다. 반면 이 정의들이 '기계적으로 계산할 수 있다'는 직관을 빠짐없이 담는다는 주장은 증명할 수 있는 정리가 아니라 논제로 남았습니다(처치–튜링 논제⁠, Church–Turing thesis⁠). 그 이야기는 「기계가 풀 수 없는 문제」 4절에 있습니다.

그런데 람다 계산에는 러셀을 괴롭힌 것과 같은 모양의 괴물이 삽니다. 함수가 자기 자신에게 적용될 수 있기 때문입니다. 람다 계산에서는 적용을 괄호 없이 나란히 써서 나타냅니다. $f\,a$는 "$f$를 $a$에 적용한다", 흔히 쓰는 $f(a)$와 같은 뜻입니다. 그러면 $x\,x$는 "$x$를 $x$ 자신에게 적용한다"입니다. $\omega = \lambda x.\, x\,x$('오메가')는 "받은 것을 자기 자신에게 적용하라"는 함수입니다. 이것을 자기 자신에게 적용하면, 몸통 $x\,x$의 두 $x$ 자리에 모두 $\omega$가 들어갑니다.

한 걸음 풀었더니 제자리입니다. 계산이 끝나지 않습니다. $x\,x$는 "$x$는 $x$의 원소이다"와 닮은꼴입니다. 둘 다 자기 참조⁠(self-reference)⁠이고, 논리에서는 모순을, 계산에서는 끝없는 되풀이를 낳을 수 있습니다.

처치는 1940년 논문 「단순 타입 이론의 한 정식화」에서 람다 계산의 모든 변수에 타입을 붙였습니다. 기본 타입 $A, B, \ldots$가 있고, $A$를 받아 $B$를 돌려주는 함수의 타입은 $A \to B$입니다. $f : A \to B$는 'f는 A를 받아 B를 내는 함수'라고 읽습니다. 쌍점(:) 왼쪽은 프로그램, 오른쪽은 그 타입입니다. 예를 들어 $\lambda x.\, x + 1$은 수를 받아 수를 내니 타입이 '수 → 수'이고, 2에는 적용할 수 있지만 "사과"에는 적용할 수 없습니다. 이것이 단순 타입 람다 계산⁠(simply typed lambda calculus)⁠입니다.

타입을 정하는 규칙은 셋뿐입니다. 이 셋이 뒤에서 논리의 추론 규칙과 짝을 이루니, 하나씩 적어 둡니다.

• 변수: $x : A$라고 정해 두었으면, 그 자리의 $x$는 타입이 $A$입니다.
• 함수 만들기(λ): $x : A$라고 두고 몸통 $M$의 타입을 구했더니 $B$였다면, $\lambda x{:}A.\, M$의 타입은 $A \to B$입니다. ($\lambda x{:}A$는 "타입이 $A$인 $x$를 받는다"로 읽습니다.)
• 적용: $f : A \to B$이고 $a : A$이면 $f\,a : B$입니다. 인수의 타입이 $A$가 아니면 타입 오류입니다.

한 예를 손으로 따라가 봅시다. $\lambda f{:}A \to B.\, \lambda x{:}A.\, f\,x$는 "함수 $f$와 값 $x$를 받아 $f$를 $x$에 적용하라"는 프로그램입니다. 안쪽부터 봅니다. 변수 규칙으로 $f : A \to B$, $x : A$입니다. 적용 규칙으로 $f\,x : B$입니다. λ 규칙으로 $\lambda x{:}A.\, f\,x : A \to B$입니다. 한 번 더 λ 규칙을 쓰면 전체의 타입은 $(A \to B) \to (A \to B)$입니다.

화살표가 여럿일 때는 약속이 하나 있습니다. 괄호가 없으면 오른쪽부터 묶습니다. 그래서 $A \to B \to C$는 $A \to (B \to C)$, 곧 "$A$를 받아 '$B$를 받아 $C$를 내는 함수'를 내놓는다"이고, 사실상 $A$와 $B$를 차례로 받아 $C$를 내는 함수입니다. 위의 타입도 $(A \to B) \to A \to B$로 적습니다. 왼쪽 괄호는 뺄 수 없습니다. $(A \to B) \to C$는 "함수를 받는 함수"라서 $A \to B \to C$와 다른 타입입니다.

아래 글상자가 그 규칙으로 타입을 검사하는 작은 기계입니다. 견본 프로그램은 이 칸을 눌러 바꿀 수 있습니다: . 글상자에 직접 써도 됩니다. 나무는 아래에서 위로 읽습니다. 맨 아래 줄이 프로그램 전체와 그 타입이고, 가로줄 위에는 그것을 만드는 데 쓴 부분들이 놓입니다. 맨 위의 잎⁠(leaf)⁠은 변수입니다. 가로줄 오른쪽의 작은 글씨가 그 줄에서 쓴 규칙입니다. 지금 나무를 보고 있습니다.

처음 보이는 견본이 방금 손으로 따라간 프로그램입니다. 맨 위의 두 잎(변수 $f$와 $x$), 그 아래 '적용' 줄, 다시 그 아래 λ 줄 두 개를 찾아보세요. 기계가 적는 타입에는 위의 약속대로 필요한 괄호만 남습니다.

견본 가운데 λx:A. x x를 골라 보세요. 기계는 $x$의 타입이 $A$라서 함수가 아니니 인수를 줄 수 없다고 거부합니다. 타입을 적지 않고 \x. x x라고만 써도 소용없습니다. $x$가 자기 자신을 받으려면 $x$의 타입이 "$x$의 타입 → 무엇"이어야 하는데, 이 언어의 타입 가운데 그런 것은 없습니다. 자기 자신을 한 부분으로 품는 타입은 유한한 식으로 쓸 수 없기 때문입니다. $x$의 타입을 T라 하면 T = T → 무엇이어야 하고, 오른쪽의 T를 다시 풀면 (T → 무엇) → 무엇, 이렇게 끝없이 길어집니다. (그런 '재귀⁠(recursion)⁠ 타입'을 따로 허락하는 언어도 있지만, 그러면 바로 아래에서 볼 '계산은 반드시 끝난다'는 성질을 잃습니다.) 러셀이 층을 나누어 막은 것을 처치는 타입으로 막았습니다.

견본 λf:A→B. λx:B. f x는 조금 다른 이유로 거부됩니다. $A$를 받는 함수에 $B$를 넣었기 때문입니다. 일상의 프로그래밍 언어가 잡아 주는 타입 오류가 바로 이것입니다.

타입을 붙인 대가로 얻은 것이 있습니다. 단순 타입 람다 계산에서 타입이 맞는 프로그램의 계산은 반드시 끝납니다. 이것을 정규화 정리⁠(normalization theorem)⁠라고 합니다. 더 풀 것이 없는 꼴, 곧 정규형⁠(normal form)⁠에 반드시 닿는다는 뜻입니다. 위의 $\omega\,\omega$처럼 영원히 도는 계산은 타입이 붙는 순간 쓸 수 없게 됩니다. 튜링은 이 사실의 한 형태를 증명한 짧은 원고를 남겼고, 이 원고는 1980년에야 로빈 갠디의 글을 통해 알려졌습니다.

잃은 것도 있습니다. 모든 계산이 끝나는 언어는, 끝나는 계산조차 모두 표현하지는 못합니다. 이것은 1891년 칸토어가 실수⁠(real number)⁠를 셀 수 없다는 것을 보일 때 쓴 대각선 논법⁠(diagonal argument)⁠의 결과입니다(「무한에도 크기가 있다」 4절에서 직접 해 볼 수 있습니다).

논증은 이렇습니다. 그런 언어의 프로그램들을 기계적으로 차례로 늘어놓을 수 있고 실행할 수도 있다고 합시다(실제 언어는 모두 그렇습니다). 이제 "$n$번째 프로그램에 $n$을 넣은 값에 1을 더하라"는 함수를 생각합니다. 목록의 프로그램은 모두 끝나니, 이 함수는 프로그램을 찾아 실행해 보는 튜링 기계로 언제나 끝나게 계산할 수 있습니다. 그런데 $n$번째 프로그램과는 $n$에서 값이 다르니(1만큼 크니), 목록 어디에도 없습니다. 끝나는 계산인데 그 언어로는 쓸 수 없는 것입니다.

그래서 실제 프로그래밍 언어는 끝나지 않을 수도 있는 되풀이(재귀)를 허락합니다. 그 순간 타입의 약속 하나가 깨집니다. 영원히 자기를 부르는 프로그램은 어떤 타입이든 가진 척할 수 있습니다. 이 점이 4절의 증명 이야기에서 결정적으로 중요해집니다. 정리하면, 타입은 계산이 반드시 끝나게 해 주는 대신 쓸 수 있는 계산을 줄입니다.

처치는 기초론 논쟁의 두 진영을 직접 거쳐 온 사람이었습니다. 1927년 프린스턴에서 오즈월드 베블런의 지도로 체르멜로의 선택공리(비어 있지 않은 집합이 아무리 많이 있어도 각 집합에서 원소를 하나씩 동시에 고를 수 있다는 공리)를 대신할 가정들에 관한 논문으로 박사 학위를 받은 뒤, 국가 연구 회의의 연구원으로 한 해는 하버드에서, 한 해는 힐베르트의 괴팅겐과 브라우어르의 암스테르담에서 보냈습니다. 1929년 프린스턴으로 돌아온 그는 1936년 『기호 논리학 저널』의 창간을 이끌고 40년 넘게 그 서평란을 맡았는데, 이 서평란이 한 이름을 낳았습니다. 1937년 튜링의 논문을 소개한 서평에서 처치가 튜링의 기계를 처음으로 '튜링 기계'라고 부른 것입니다. 튜링은 그 무렵 처치의 박사 과정 학생으로 프린스턴에 와 있었고, 1938년 학위를 받았습니다. λ라는 기호가 어디서 왔는지는 설명이 엇갈립니다. 널리 전하는 이야기는 이렇습니다. 처치가 『수학 원리』에서 함수를 만드는 데 쓴 $\hat{x}$(x 위의 꺾쇠)를 빌리려 했는데, 식자공이 꺾쇠를 x 앞으로 옮겨 적는 과정에서 λ가 되었다는 것입니다. 하지만 처치 자신이 뒤에 특별한 까닭 없이 고른 글자라고 말했다는 증언도 있습니다.

4 · 1934–1969명제는 타입, 증명은 프로그램: 커리와 하워드

이 절의 물음은 이것입니다. 3절의 타입 붙은 프로그램과 2절의 '만들어 건네는' 증명은 정말 같은 것일까? 같다면 규칙 하나하나까지 맞아떨어질까? 먼저 두 사람이 이것을 알아챈 과정을 보고, 그다음 직접 프로그램을 써서 증명해 봅니다.

펜실베이니아 주립대학의 해스켈 커리는 처치와 거의 같은 시기에, 변수조차 없이 함수 몇 개를 조합하는 체계인 조합 논리⁠(combinatory logic)⁠를 연구하고 있었습니다. 가장 기본적인 조합자⁠(combinator)⁠는 둘이었습니다. $\mathsf K$는 두 인수를 받아 첫째를 돌려주고, $\mathsf S$는 세 인수 $x, y, z$를 받아 $x\,z\,(y\,z)$를 돌려줍니다. 뒤의 식은 "$x$에 $z$를 넣어 얻은 함수에, $y$에 $z$를 넣어 얻은 값을 다시 넣는다"로 읽습니다. 곧 $z$를 두 곳에 나눠 주는 조합자입니다. 예를 들어 K에 3과 5를 차례로 넣으면 3이 나옵니다. 1934년 커리는 이 둘에 붙는 타입을 적다가 이상한 것을 보았습니다.

왼쪽 식은 'K는 A 값을 받으면, B 값을 받아 A 값을 내는 함수를 내놓는다'로 읽습니다. 3과 5의 예에서 A와 B가 모두 수이면 K : 수 → (수 → 수)입니다. 이제 화살표를 '이면'으로 읽어 보세요. "A이면, (B이면 A)"입니다. A가 참이면 B가 무엇이든 A는 참이라는 뜻이니 논리 법칙으로도 옳습니다.

오른쪽 식도 같은 방법으로 읽으면 "(A이면 (B이면 C))이면, ((A이면 B)이면 (A이면 C))"입니다. 풀어 말하면 이렇습니다. A가 주어지면 'B이면 C'가 성립하고, A가 주어지면 B도 성립한다고 합시다. 그러면 A가 주어졌을 때 B가 성립하고, 그 B로 C를 얻습니다. 곧 A이면 C입니다. 가정 $A$(값 $z$)를 두 곳에 나눠 쓴다는 점이 S가 하는 일과 똑같습니다.

이 두 식은 명제 논리 교과서에 나오는 함의 논리의 두 공리와 글자 하나 다르지 않습니다. 명제 논리는 '그리고, 또는, 이면, 아니다'로 명제를 짜 맞추는 논리이고, 공리는 증명 없이 받아들이는 출발점입니다. 교과서의 흔한 체계는 이 두 공리에서 시작해 한 가지 추론 규칙만으로, '이면'만 쓰는 직관주의 논리(2절)의 법칙을 모두 끌어냅니다. 그 규칙이 바로 다음에 볼 전건 긍정입니다. 게다가 함수 $f : A \to B$를 $a : A$에 적용해 $B$를 얻는 일은, "$A$이면 $B$"와 "$A$"에서 "$B$"를 끌어내는 추론 규칙(전건 긍정⁠, modus ponens⁠)과 모양이 같습니다. '비가 오면 땅이 젖는다'와 '비가 온다'에서 '땅이 젖는다'를 끌어내는 규칙입니다. 커리는 이 관찰을 1958년 로베르 페이스와 함께 쓴 책 『조합 논리』에서 더 분명히 적었습니다.

이 관찰을 논리 전체로 넓힌 사람은 윌리엄 하워드입니다. 1969년 그는 「구성이라는 개념에 대한 '식은 곧 타입' 관점」(The formulae-as-types notion of construction)이라는 원고를 써서 복사본으로 돌렸습니다. 원고가 보인 것은 이것입니다. 1934년 게르하르트 겐첸이 만든 자연 연역⁠(natural deduction)⁠은 사람이 실제로 추론하는 방식을 본뜬 증명 체계인데, 그 규칙 하나하나가 타입 붙은 람다 계산의 규칙 하나하나와 짝을 이룹니다. 자연 연역에서는 "A라고 가정하자"로 시작해 규칙을 한 줄씩 쓰고, 결론을 얻으면 가정을 거두어 "A이면 …"을 얻습니다. 이 대응을 오늘날 커리–하워드 대응이라고 부릅니다(원고가 돌려 읽힌 사정은 이 절 끝에 적었습니다). 2절의 BHK 표를 다시 보면 거의 그대로입니다.

머리말의 예로 표를 한 줄씩 짚어 봅시다. 명제 "A 그리고 B이면 B 그리고 A"의 증명은 프로그램 λp:A×B. (snd p, fst p)입니다. λp:A×B.는 '쌍 p를 받는다', 곧 "A 그리고 B라고 가정하자"입니다. snd p는 쌍의 둘째 것, 곧 가정에서 B를 꺼내는 추론이고, fst p는 A를 꺼내는 추론입니다. ( , )로 둘을 묶는 것은 "B이고 A이니 B 그리고 A"라는 추론입니다. 프로그램의 부분 하나하나가 증명의 한 줄 한 줄입니다.

이 짝이 우연이 아닌 까닭은 규칙을 나란히 놓으면 보입니다. 자연 연역의 규칙은 논리 낱말마다 두 종류씩 있습니다. 도입 규칙은 그 낱말이 든 명제를 증명하는 법이고, 제거 규칙은 그런 명제를 이미 가졌을 때 써먹는 법입니다. 아래 증명 나무에서 I는 도입(Introduction), E는 제거(Elimination)의 머리글자입니다.

• 이면: →I는 "$A$를 가정해 $B$를 얻었으면, 가정을 거두고 $A \to B$"이고, 프로그램으로는 λ로 함수를 만드는 일입니다. →E는 "$A \to B$와 $A$에서 $B$"(전건 긍정)이고, 프로그램으로는 적용입니다.
• 그리고: ∧I는 "$A$와 $B$에서 $A \land B$"이고 쌍 (a, b)를 만드는 일입니다. ∧E₁, ∧E₂는 "$A \land B$에서 $A$", "$A \land B$에서 $B$"이고 fst, snd입니다.
• 또는: ∨I₁, ∨I₂는 "$A$에서 $A \lor B$", "$B$에서 $A \lor B$"이고 꼬리표 inl(왼쪽), inr(오른쪽)을 붙이는 일입니다. ∨E는 "$A \lor B$가 있고, $A$를 가정해도 $C$, $B$를 가정해도 $C$가 나오면 $C$"(경우 나누기)이고 case입니다.
• 모순: ⊥E는 "$\bot$에서는 무엇이든 따라 나온다"이고 absurd입니다. 원소가 없는 타입의 값은 실제로 올 수 없으니, 그런 값을 받았다고 치면 무엇을 돌려준다고 해도 거짓말이 되지 않습니다.

3절의 타입 규칙 셋을 다시 보세요. 변수 규칙은 "앞에서 세운 가정을 가져다 쓴다", λ 규칙은 →I, 적용 규칙은 →E입니다. 타입 규칙을 적는 일과 추론 규칙을 적는 일이 같은 일이었던 것입니다.

표의 마지막 줄이 이 대응을 말장난 이상으로 만듭니다. 자연 연역의 증명에는 군더더기가 있을 수 있습니다. "$A$를 가정하면 $A$이다. 그러니 $A \to A$. 그런데 $A$가 성립하니 $A$"처럼 →를 도입했다가(→I) 곧바로 제거하는(→E) 돌아가기입니다. 이미 가진 $A$를 한 바퀴 돌려 다시 얻었을 뿐입니다. 1965년 다그 프라비츠는 모든 증명에서 이런 돌아가기를 없앨 수 있음을 증명했습니다. 이 증명을 프로그램으로 적으면 $(\lambda x.\, x)\, a$이고, 돌아가기를 없애는 일은 이것을 $a$로 계산하는 β 축약과 정확히 같습니다. 정리하면, 증명을 단순하게 만드는 일이 곧 프로그램을 실행하는 일입니다.

이제 직접 증명해 봅시다. 목표 명제 를 고르고, 그 타입을 가진 프로그램을 칸에 써 보세요. 기계는 프로그램의 타입을 구한 뒤 목표와 비교합니다. 맞으면 그 프로그램이 곧 증명이고, 아래 나무는 겐첸의 자연 연역 증명입니다. 나무를 볼 수 있습니다. 두 나무의 모양이 똑같다는 것을 확인해 보세요. 막히면 답 보기, 처음부터 다시 하려면 지우기.

증명으로 본 나무에서 잎 $[A]^x$는 "$A$라고 가정하자"이고, 위첨자 $x$는 그 가정의 이름입니다. $\to$I 규칙의 줄 옆에 같은 위첨자가 붙어 있으면, 그 줄에서 그 이름의 가정이 거두어진다는 표시입니다. "$A$를 가정했더니 $B$가 나왔으니, 가정 없이 $A \to B$"라는 뜻입니다. 프로그램으로 보면 잎은 변수이고, 가정을 거두는 줄은 그 변수를 받는 $\lambda$입니다. 가정에 이름을 붙이는 일과 변수에 이름을 붙이는 일이 같은 일이었던 것입니다.

여기서 정확히 무엇이 증명된 것인지 짚어 둡시다. 요점은 셋입니다. 명제의 증명이 있으면 그 타입의 프로그램이 있고 거꾸로도 그렇습니다. 증명 하나에 프로그램 하나가 짝지어집니다. 증명을 다듬는 걸음과 프로그램을 계산하는 걸음이 서로 짝지어집니다. 정확히 적으면 정리는 이렇습니다.

명제 논리식 $A$가 직관주의 명제 논리의 자연 연역으로 증명되는 것과, 타입이 $A$인 닫힌 항(바깥의 변수를 쓰지 않는 프로그램)이 단순 타입 람다 계산(쌍, 합, 빈 타입⁠(empty type)⁠을 더한 것)에 있는 것은 동치이고, 증명과 항은 일대일로 대응하며, 증명의 군더더기를 없애는 걸음과 항을 계산하는 걸음이 서로 대응합니다. (∨가 들어가면, 경우 나누기로 얻은 결과에 곧바로 제거 규칙을 쓸 때 그 규칙을 두 갈래 안으로 옮겨 넣는 걸음까지 양쪽에 함께 넣어야 이 대응이 맞습니다.) '동치'는 한쪽이 성립하면 다른 쪽도 성립하고 거꾸로도 그렇다는 뜻이고, '일대일로 대응한다'는 빠짐도 겹침도 없이 하나씩 짝지어진다는 뜻입니다. 이것은 두 체계를 정확히 정한 뒤에 증명된 수학적 사실입니다. 반면 "모든 증명은 프로그램이다"는 슬로건입니다. 고전 논리, 집합론⁠(set theory)⁠, 선택공리⁠(axiom of choice)⁠까지 포함한 보통의 수학이 어떤 프로그램에 대응하는지는 체계마다 따로 따져야 하는 문제입니다.

3절 끝의 이야기가 여기서 돌아옵니다. 끝나지 않는 재귀를 허락하는 언어에서는 $\mathrm{loop} = \mathrm{loop}$처럼 영원히 자기를 부르는 정의가 아무 타입이나 가질 수 있습니다. 까닭은 이렇습니다. "loop의 타입은 $\bot$이다"라고 선언하면, 타입 검사기는 정의의 오른쪽 $\mathrm{loop}$의 타입을 보는데, 그것은 방금 선언한 대로 $\bot$이니 검사를 통과합니다. 실행하면 값을 내놓지 않고 영원히 돌 뿐이라, 선언이 거짓이라는 것이 드러날 일도 없습니다. 그래서 그런 언어의 타입 검사는 $\bot$의 '증명'도 통과시키고, 논리로서는 무너집니다. 모순이 증명되면 ⊥E로 무엇이든 증명되기 때문입니다. 증명 보조기들이 재귀 함수⁠(recursive function)⁠가 반드시 끝나는지를 따로 검사하는 까닭입니다. 또 하나. 일상의 프로그램 대부분은 시시한 명제의 증명입니다. 정수를 받아 정수를 돌려주는 함수는 "정수가 있으면 정수가 있다"를 증명할 뿐입니다. 이 대응이 수학에 쓸모 있으려면 타입이 훨씬 많은 것을 말할 수 있어야 합니다. 그 이야기는 9절에서 합니다.

조합자를 처음 생각한 사람은 커리가 아니었습니다. 1920년 12월 7일 괴팅겐 수학회에서 러시아 출신의 모지스 쇤핑켈이 변수 없이 몇 개의 기본 함수만으로 논리식을 적는 방법을 발표했습니다. 이 강연은 1924년 하인리히 베만의 손으로 정리되어 논문 「수리 논리의 구성 요소에 관하여」로 나왔습니다. 여러 인수의 함수를 한 인수씩 받는 함수로 바꾸는 기법도 이 논문에 이미 있었습니다. 커리는 1927년 말 프린스턴의 도서관에서 이 논문을 찾아냈고, 자기가 혼자 가던 길을 누군가 먼저 지나갔다는 것을 알았습니다. 그는 이듬해 괴팅겐으로 건너가 힐베르트와 파울 베르나이스 곁에서 연구를 이어 1930년 학위를 받았습니다. 쇤핑켈은 모스크바로 돌아간 뒤 연구를 거의 발표하지 못했고, 1942년 그곳에서 가난 속에 세상을 떠난 것으로 전합니다.

하워드의 원고가 걸어온 길도 순탄하지 않았습니다. 하워드의 회고에 따르면 핵심 착상은 1966년 무렵 조합자로 먼저 떠올랐고, 1969년 손으로 쓴 노트로 정리되었습니다. 노트는 출판되지 않은 채 복사본으로 논리학자들 사이에 돌았고, 9절의 마르틴뢰프와 7절의 지라르처럼 이 대응 위에서 새 체계를 짓는 사람들이 그것을 읽었습니다. 원고는 11년 동안 복사본으로 읽히다가, 1980년 커리의 여든 살을 기념하는 논문집에 실렸습니다.

자연 연역을 만든 겐첸의 목표는 힐베르트의 계획, 곧 수학이 모순을 낳지 않는다는 것을 유한한 방법으로 증명하는 일이었습니다. 그는 괴팅겐에서 베르나이스에게 배웠습니다. 1933년 나치 정권이 유대계인 베르나이스를 대학에서 쫓아낸 뒤, 겐첸은 헤르만 바일의 이름으로 박사 논문을 냈고, 그 논문이 1934–35년 「논리적 추론에 관한 연구」로 출판되었습니다. 여기서 그는 자연 연역과 함께 시퀀트 계산⁠(sequent calculus)⁠이라는 또 하나의 체계를 만들고, 증명에서 돌아가기를 모두 없앨 수 있다는 정리(절단 제거⁠, cut elimination⁠)를 증명했습니다. 프라비츠의 1965년 결과는 이것을 자연 연역에서 직접 보인 것입니다. 1936년 겐첸은 자연수의 산술에 모순이 없다는 것을 증명했지만, 괴델의 정리가 말하는 대로 산술 자체보다 강한 원리($\varepsilon_0$까지의 초한 귀납법⁠(transfinite induction)⁠)를 써야 했습니다. 나치 돌격대원이었던 그는 1943년부터 프라하의 독일 대학에서 가르치다가 1945년 5월 프라하 봉기 때 붙잡혔고, 같은 해 8월 4일 수용소에서 굶주림으로 세상을 떠났습니다. 서른다섯 살이었습니다.

5 · 1945년'자연스럽다'를 정의하기: 범주론

이 절의 물음은 이것입니다. 수학자들이 늘 쓰는 '자연스럽다'는 말을 정확히 정의할 수 있을까? 그 정의는 뜻밖에도 프로그램의 성질 하나, 곧 '원소를 들여다보지 않고 일한다'는 성질과 같은 것으로 드러납니다.

같은 무렵 전혀 다른 곳에서 세 번째 줄기가 자라고 있었습니다. 1941년 미시간 대학에 강연하러 간 하버드의 손더스 매클레인은, 바르샤바에서 공부하고 2년 전 미국으로 건너온 위상수학자 새뮤얼 에일렌베르크를 만났습니다. 매클레인이 강연한 대수의 계산이 에일렌베르크가 연구하던 위상수학의 계산과 똑같은 모양이었습니다. 두 사람은 공동 연구를 시작했습니다. 전쟁이 그 뒤를 가로질렀습니다. 매클레인은 1943년부터 1945년까지 하버드를 떠나 뉴욕 컬럼비아 대학의 응용수학 그룹을 이끌며 사격 통제 장치에 필요한 미분방정식⁠(differential equation)⁠을 풀었고, 공동 연구는 그 틈틈이 이어졌습니다. 그 과정에서 수학자들이 늘 쓰지만 아무도 정의한 적 없는 말 하나를 정의해야 했습니다. '자연스럽다'는 말입니다.

무엇이 문제였는지 선형대수⁠(linear algebra)⁠의 예로 봅시다. 여기서는 평면의 화살표들처럼 더하고 늘일 수 있는 것들의 모임을 벡터⁠(vector)⁠ 공간이라 하고, 이런 공간 $V$의 벡터를 수 하나로 바꾸는 규칙 가운데 덧셈과 늘이기를 지키는 것을 선형 사상⁠(linear map)⁠이라 합니다. 평면이라면 (x, y)를 2x + 3y로 보내는 규칙이 그런 예입니다. 이런 규칙들을 모은 공간이 $V^*$(쌍대 공간⁠, dual space⁠)입니다.

유한 차원 벡터 공간⁠(vector space)⁠ $V$와 $V^*$는 차원이 같으니 서로 같은 꼴(동형⁠, isomorphism⁠)입니다. 하지만 둘을 짝짓는 방법은 기저, 곧 좌표축을 하나 고른 뒤에야 정해지고, 기저를 바꾸면 짝도 바뀝니다. 평면에서 보통의 좌표축을 쓰면 벡터 (a, b)를 규칙 "(x, y) ↦ ax + by"와 짝지을 수 있지만, 좌표축을 기울이면 같은 벡터가 다른 규칙과 짝지어집니다. 한편 $V^*$도 벡터 공간이니 그 쌍대 공간을 또 만들 수 있습니다. 이것을 $V^{**}$('V 쌍대의 쌍대')라 적습니다. $V^{**}$의 원소는 $V^*$의 규칙 하나하나를 받아 수 하나를 내는, 덧셈과 늘이기를 지키는 규칙입니다. $V$와 $V^{**}$는 기저 없이 짝지을 수 있습니다. 벡터 $v$에 "선형 사상 $\varphi$('파이')를 받아 $\varphi(v)$를 내는 것"을 대응시키면 됩니다. 예를 들어 $v = (1, 2)$는 "규칙을 받으면 그 규칙에 (1, 2)를 넣어 본다"는 것과 짝지어지고, 규칙 (x, y) ↦ 2x + 3y를 받으면 2 + 6 = 8을 냅니다. 좌표축을 한 번도 쓰지 않은 짝짓기입니다. 수학자들은 앞의 것을 임의적, 뒤의 것을 자연스럽다고 불렀습니다.

에일렌베르크와 매클레인은 1942년의 짧은 논문에 이어 1945년 「자연 동치의 일반 이론」에서 이 차이를 정의로 만들었습니다. 그러려고 세 가지를 정의했습니다.

• 범주⁠(category)⁠: 대상들과, 대상 사이의 화살표들. 화살표 $f : A \to B$와 $g : B \to C$는 이어 붙여 $g \circ f : A \to C$('f 다음 g')가 되고, 이어 붙이기는 결합 법칙을 따르며, 대상마다 아무것도 하지 않는 항등 화살표⁠(identity arrow)⁠가 있습니다. 집합과 함수, 군과 준동형⁠(homomorphism)⁠ 사상, 위상 공간⁠(topological space)⁠과 연속 함수가 모두 범주입니다. 타입과 프로그램도, 계산해서 같아지는 프로그램을 하나로 치면 범주를 이룹니다.
• 함자⁠(functor)⁠: 범주에서 범주로 가는 대응(함자). 대상을 대상으로, 화살표를 화살표로 보내되 이어 붙이기와 항등을 지킵니다. 프로그래밍의 예: 타입 $A$를 'A의 목록' $\mathrm{List}\,A$로 보내고, 함수 $f$를 "목록의 원소마다 $f$를 적용하는" $\mathrm{map}\,f$로 보내는 것. $\mathrm{map}\,(g \circ f) = \mathrm{map}\,g \circ \mathrm{map}\,f$입니다. 예를 들어 map (두 배)는 [1, 2, 3]을 [2, 4, 6]으로 보냅니다. 등식은 원소마다 f와 g를 잇달아 한 번에 하는 것과, 목록 전체에 f를 한 다음 g를 하는 것이 같다는 뜻입니다.
• 자연 변환(자연 변환⁠, natural transformation⁠): 함자 $F$에서 함자 $G$로 가는, 대상마다 하나씩인 화살표들 $\eta_A : F A \to G A$('에타 A')의 모음. 여기서 $F A$는 함자 $F$가 대상 $A$를 보낸 곳, 목록의 예라면 'A의 목록'입니다. 목록의 예라면 "어떤 타입의 목록이든 뒤집는다"처럼, 타입마다 하나씩 있는 목록 재배열 방법입니다. 단 모든 화살표 $f : A \to B$에 대해 아래 네모가 닫혀야 합니다.

식을 말로 읽으면, "먼저 $\eta$로 바꾸고 그다음 $f$를 적용한 것"(왼쪽)과 "먼저 $f$를 적용하고 그다음 $\eta$로 바꾼 것"(오른쪽)이 같다는 뜻입니다. "네모가 닫힌다"는 말은 두 길로 가도 같은 곳에 닿는다는 뜻입니다. 손으로 먼저 해 봅시다. 목록 [3, −1, 2]에 '부호 바꾸기'를 먼저 하면 [−3, 1, −2], 이것을 뒤집으면 [−2, 1, −3]입니다. 거꾸로 먼저 뒤집으면 [2, −1, 3], 부호를 바꾸면 [−2, 1, −3]입니다. 같습니다. 그런데 '뒤집기' 대신 '정렬'을 쓰면 한쪽 길은 [−3, −2, 1], 다른 쪽 길은 [1, −2, −3]이 되어 어긋납니다.

그림에서 직접 해 봅시다. $F = G = \mathrm{List}$이고, $\eta$는 목록을 재배열하는 방법 , 원소에 적용할 함수는 , 처음 목록은 입니다. 위쪽 길은 먼저 원소마다 함수를 적용하고 그다음 재배열합니다. 아래쪽 길은 먼저 재배열하고 그다음 함수를 적용합니다. 세 선택지를 바꿔 가며 두 길이 오른쪽 아래에서 만나는지 보세요.

뒤집기, 앞의 둘만 남기기, 두 번 이어 쓰기는 어떤 함수, 어떤 목록에서도 네모가 닫힙니다. 정렬과 양수만 남기기는 어떤 함수에서는 닫히고 어떤 함수에서는 깨집니다. 정렬은 두 배 하기와는 잘 맞지만, 부호를 바꾸면 크기 순서가 뒤집히니 깨집니다. 차이는 이것입니다. 앞의 셋은 원소가 무엇인지 보지 않고 자리만 옮깁니다. 뒤의 둘은 원소를 들여다보고(크기를 비교하고, 양수인지 묻고) 결정합니다. 정리하면, 자연성이 금지하는 것이 바로 이것입니다. 자연 변환은 모든 타입에 대해 같은 방식으로, 원소의 정체를 보지 않고 일해야 합니다.

벡터 공간으로 돌아가면, 기저를 고르는 일은 벡터 공간 하나하나를 들여다보는 선택이라서 자연스럽지 않습니다. 게다가 $V \mapsto V^*$는 선형 사상 $f : V \to W$를 거꾸로 $W^* \to V^*$로 보내는 함자입니다. $W$ 위의 규칙 $\varphi$가 있으면 '먼저 $f$로 옮긴 뒤 $\varphi$를 쓰는 것'($\varphi \circ f$)이 $V$ 위의 규칙이 되니, 규칙은 $W$ 쪽에서 $V$ 쪽으로, 곧 거꾸로 옮겨집니다. 그래서 $V$와 $V^*$ 사이에는 위의 네모를 세울 수조차 없습니다. 반면 $V \mapsto V^{**}$는 방향을 두 번 뒤집어 제자리로 오니 네모를 세울 수 있고, 앞에서 본 짝짓기가 그 네모를 닫습니다. 에일렌베르크와 매클레인의 1945년 논문이 바로 이 예로 시작합니다.

매클레인은 뒤에 교과서 『일하는 수학자를 위한 범주론』(1971)에서 이렇게 적었습니다. 범주는 함자를 정의하려고, 함자는 자연 변환을 정의하려고 정의한 것이라고. 처음에는 대수적 위상수학의 계산을 정리하는 언어였던 범주론은 1950–60년대에 알렉산더 그로텐디크의 대수기하학을 거치며 수학의 여러 분야를 잇는 공용어가 되었습니다. 전환점으로 흔히 두 편의 논문을 꼽습니다. 하나는 그로텐디크가 1957년 일본의 『도호쿠 수학 저널』에 실은 호몰로지 대수(도형에 뚫린 구멍 같은 성질을 대수로 계산하는 도구) 논문으로, 따로따로 계산되던 여러 호몰로지 이론을 '아벨 범주⁠(abelian category)⁠'라는 한 틀에 담았습니다. 다른 하나는 1958년 대니얼 칸의 「수반 함자⁠(adjoint functor)⁠」로, 뒤에서 볼 수반을 처음 정의했습니다(「화살표만으로 본 수학」 5–6절). 이 글의 이야기에서 중요한 것은 두 가지입니다.

첫째는 요네다 보조정리⁠(Yoneda lemma)⁠입니다. 매클레인의 회고에 따르면 1954년 파리에서, 도쿄에서 온 젊은 수학자 요네다 노부오가 그에게 이 사실을 들려주었고, 이름은 매클레인이 붙였습니다. 파리 북역의 카페에서 시작한 대화는 요네다가 탈 기차가 떠날 때까지 기차 안에서 이어졌다고 합니다. 뜻을 말로 옮기면 이렇습니다. 대상 $A$는, 모든 대상 $X$에서 $A$로 가는 화살표들이 무엇이고 그것들이 이어 붙이기에 따라 어떻게 바뀌는지를 알면 (같은 꼴을 빼고는) 완전히 정해집니다. 안을 열어 보지 않고 바깥과의 관계만으로 대상을 안다는 것입니다.

프로그래밍으로 옮기면 한 가지 뜻밖의 사실이 됩니다. "어떤 타입 $R$이든, $A \to R$ 함수를 주면 $R$을 돌려주겠다"는 타입 $\forall R.\,(A \to R) \to R$('모든 R에 대해, A에서 R로 가는 함수를 받아 R을 낸다')의 값은, 따지고 보면 $A$의 값 하나와 같습니다. 그 값이 할 수 있는 일은 가지고 있는 $A$ 하나를 받은 함수에 넣는 것뿐이기 때문입니다(7절의 매개변수성⁠(parametricity)⁠이 이것을 보장합니다). 예를 들어 수 5를 들고 있는 값은 "함수 g를 주면 g(5)를 돌려주겠다"는 값과 같은 정보를 담습니다.

둘째는 이 생각을 정의의 방법으로 쓰는 보편 성질⁠(universal property)⁠입니다. 집합이라면 두 집합의 곱 $A \times B$는 순서쌍 (a, b)들의 집합이고, $\mathsf{fst}$는 앞의 것을, $\mathsf{snd}$는 뒤의 것을 꺼내는 함수입니다. 보편 성질은 이 곱을 "안에 무엇이 들었는가"로 정의하지 않고, "$A \times B$에는 두 화살표 $\mathsf{fst} : A \times B \to A$, $\mathsf{snd} : A \times B \to B$가 있고, 어떤 $X$에서든 $X \to A$와 $X \to B$의 쌍을 주면, 뒤에 $\mathsf{fst}$와 $\mathsf{snd}$를 붙였을 때 그 둘이 되는 $X \to A \times B$가 정확히 하나 있다"로 정의합니다. 예를 들어 $X$, $A$, $B$가 모두 수의 집합이고 두 화살표가 x ↦ x + 1과 x ↦ 2x라면, 그 하나뿐인 화살표는 x ↦ (x + 1, 2x)입니다. 뒤에 $\mathsf{fst}$를 붙이면 x + 1이, $\mathsf{snd}$를 붙이면 2x가 나오고, 쌍의 앞과 뒤가 이렇게 정해져 있으니 다른 선택은 없습니다. 4절에서 쓴 규칙을 떠올려 보세요. 쌍 $(a, b)$를 만드는 규칙과 $\mathsf{fst}$, $\mathsf{snd}$로 꺼내는 규칙이 이 성질의 '있다' 쪽을 말합니다. '정확히 하나' 쪽은 쌍을 풀었다가 다시 묶으면 제자리라는 규칙($(\mathsf{fst}\,p, \mathsf{snd}\,p) = p$)이 맡습니다. 논리의 '그리고', 프로그램의 쌍, 범주의 곱이 한 가지였던 것입니다.

요네다의 뒷날은 이 글의 두 줄기가 한 사람 안에서 만난 예입니다. 도쿄 대학에서 호몰로지 대수로 학위를 받은 그는 점차 계산기 과학으로 옮겨 가, 1972년부터 도쿄 대학에서 정보 과학의 기초론을 가르쳤습니다. 그리고 일본 대표로 IFIP 작업반 2.1, 곧 프로그래밍 언어 ALGOL 60을 관리하고 ALGOL 68을 정의한 국제 모임에 참여했습니다. ALGOL 60의 문법을 적은 표기법(BNF)이 2,000여 년 전 파니니의 문법 규칙과 같은 일을 한다는 이야기는 「말을 세는 기계」 1절에 있습니다.

6 · 1968–1972세 얼굴이 하나로: 람베크와 로베어

이 절의 물음은 이것입니다. 4절의 논리–프로그램 대응에 5절의 범주를 셋째 얼굴로 더할 수 있을까? 그러려면 범주에 무엇이 있어야 할까? 그리고 타입의 '곱'과 '지수'라는 이름은 왜 붙었을까?

몬트리올 맥길 대학의 요아힘 람베크가 이 이야기에 이른 길은 뜻밖에 언어학을 거쳤습니다. 1958년 논문 「문장 구조의 수학」에서 그는 낱말마다 타입을 주었습니다. 이름은 $n$, 문장은 $s$입니다. 자동사 "잔다"의 타입은 $n \backslash s$이고, "왼쪽에 이름(n)이 오면 문장(s)이 된다"는 뜻입니다.

그러면 "철수가 잔다"가 문장이라는 것을 계산으로 확인할 수 있습니다. "철수가"는 n, "잔다"는 n\s이니, 둘을 나란히 놓았을 때의 추론은 $n \cdot (n \backslash s) \to s$입니다. 가운데 점(·)은 "왼쪽 낱말 다음에 오른쪽 낱말", 화살표는 "그러면 이것이 된다"로 읽습니다. 3 × (5 ÷ 3) = 5에서 3이 약분되듯, 앞의 n과 n\s 안의 n이 지워지고 s가 남습니다. 이 규칙은 "n을 받아 s를 내는 함수에 n을 넣으면 s"라는 함수 적용과 모양이 같습니다. 다른 점은 하나입니다. 보통의 논리에서는 가정의 순서를 바꿔도 되지만('A 그리고 B'와 'B 그리고 A'는 같은 가정입니다), 문장에서는 "잔다 철수가"가 문장이 아니듯 순서가 중요해서, 순서를 바꾸는 규칙이 없습니다. 문법을 규칙으로 보는 이런 생각이 촘스키의 위계와 어떻게 이어지는지는 「말을 세는 기계」 6절에 있습니다.

람베크는 1968년부터 1972년까지 「연역 체계와 범주」라는 제목의 논문 세 편에서 마지막 조각을 맞추었습니다. 논리의 증명, 타입 붙은 람다 계산의 프로그램, 그리고 데카르트 닫힌 범주⁠(cartesian closed category)⁠라는 특별한 범주의 화살표가 서로 정확히 대응한다는 것입니다. 이 범주가 무엇인지, 5절의 집합과 함수의 범주에서 먼저 봅시다. 논리의 '그리고', '참', '이면'을 범주로 옮기려면 그 구실을 하는 대상이 셋 있어야 합니다.

• '그리고' ↔ 곱 $A \times B$: 5절 끝에서 보편 성질로 정의한 그 곱입니다. 집합에서는 순서쌍 (a, b)들의 집합입니다.
• '참' ↔ 끝 대상⁠(terminal object)⁠ $1$: 집합에서는 원소가 하나뿐인 집합, 예를 들어 {★}입니다. 어느 집합 X에서든 {★}로 가는 함수는 "모든 원소를 ★로 보낸다" 하나뿐입니다. '어느 대상에서든 화살표가 정확히 하나 들어온다'는 이 성질이 끝 대상의 정의입니다. 논리로는 "무엇에서든 참은 따라 나온다"입니다. 끝 대상을 '아무것도 없는 곱'이라고도 부릅니다. 수에서 아무것도 곱하지 않은 곱을 1로 치듯, 어떤 집합 A와 {★}의 곱 A × {★}은 A와 원소가 하나씩 짝지어져서 곱해도 달라지는 것이 없기 때문입니다.
• '이면' ↔ 지수 대상⁠(exponential object)⁠ $B^A$: 집합에서는 A에서 B로 가는 함수 전체의 집합입니다. 일반적인 범주에서 'A에서 B로 가는 화살표들'은 범주 바깥에서 모아 놓은 목록일 뿐이라, 그 목록 구실을 하는 대상이 범주 안에 따로 있어야 합니다. 그 대상이 B^A이고, 어떤 대상이 이 구실을 하는지는 아래 조건으로 정합니다.

데카르트 닫힌 범주는 이 셋이 모두 있는 범주입니다. 지수 대상의 조건을 적기 위해 기호 둘을 씁니다. $\operatorname{Hom}(X, Y)$('홈 X, Y')는 X에서 Y로 가는 화살표들의 모음이고, ≅는 두 모음이 빠짐도 겹침도 없이 짝지어진다는 뜻입니다(X를 바꿔도 같은 방식으로, 곧 5절의 뜻에서 자연스럽게 짝지어져야 합니다).

식을 말로 읽으면 "X × A에서 B로 가는 화살표와, X에서 B^A로 가는 화살표가 하나씩 짝지어진다"입니다. 집합으로 읽으면 왼쪽은 두 인수를 한꺼번에 받는 함수, 오른쪽은 인수를 하나 받아 "나머지 하나를 받는 함수"를 돌려주는 함수입니다. 예를 들어 두 수를 받아 더하는 함수 (x, a) ↦ x + a는, x를 받아 "a를 받아 x + a를 내는 함수"를 돌려주는 함수와 짝지어집니다. 이 둘째 함수에 3을 넣으면 '3 더하기' 함수가 나옵니다. 둘이 일대일로 대응한다는 것이 커링이고, 논리로는 "$X$ 그리고 $A$이면 $B$"와 "$X$이면, $A$이면 $B$"가 같다는 것입니다.

이 대응은 곱하기 $- \times A$와 지수 $(-)^A$ 사이의 수반 관계의 한 예이기도 합니다. 가로줄(−)은 대상이 들어갈 빈칸입니다. 앞의 것은 대상 X를 X × A로, 뒤의 것은 대상 B를 B^A로 보냅니다. 두 대응 사이에 "앞의 것을 거친 대상에서 나가는 화살표"와 "뒤의 것을 거친 대상으로 들어가는 화살표"가 위의 식처럼 자연스럽게 짝지어질 때, 두 대응을 수반이라고 부릅니다.

이제 타입과 프로그램으로 범주를 만들어 봅시다. 대상은 타입입니다. 타입 A에서 B로 가는 화살표는 변수 x : A 하나만 쓰는, 타입이 B인 프로그램입니다. 예를 들어 p ↦ fst p는 A × B에서 A로 가는 화살표이고, 논리로 읽으면 "A 그리고 B를 가정하고 A를 증명한 것"입니다. 두 화살표를 이어 붙이는 일은 대입입니다. x ↦ M 다음 y ↦ N은 N 안의 y 자리에 M을 넣은 프로그램이고, 증명으로는 앞 증명의 결론을 뒤 증명의 가정 자리에 끼워 넣는 일입니다. 항등 화살표는 x ↦ x입니다. 약속이 하나 필요합니다. 계산해서 같아지는 두 프로그램은 같은 화살표로 칩니다. 예를 들어 (λy. y) x와 x는 같은 화살표입니다.

람베크와 필립 스콧이 1986년 책에서 정리한 결과는 정확히 이렇습니다. 곱과 원소 하나짜리 타입이 있는 단순 타입 람다 계산의 항들을, β 축약과 η 규칙(함수나 쌍을 풀었다 다시 묶으면 제자리라는 규칙. 예를 들어 λx. f x는 f와 같고, (fst p, snd p)는 p와 같습니다)으로 같아지는 것끼리 묶으면, 기본 타입들에서 '자유롭게' 만든 데카르트 닫힌 범주가 됩니다. 여기서 '자유롭게'란 데카르트 닫힌 범주의 법칙이 강제하는 것 말고는 어떤 등식도 더하지 않았다는 뜻입니다. 그래서 이 대응을 커리–하워드–람베크 대응이라고도 부릅니다. 정리하면, 증명 하나는 프로그램 하나이고, 그것은 곧 데카르트 닫힌 범주의 화살표 하나입니다.

왜 하필 '곱'과 '지수'라는 이름일까요? 원소가 유한한 집합들의 범주에서 세어 보면 알 수 있습니다. 집합 $A$의 원소가 개, $B$의 원소가 개일 때, 타입 의 원소를 모두 늘어놓아 봅시다.

그림 아래 식의 $|A|$는 'A의 원소의 개수'라고 읽습니다. 쌍은 곱만큼, 꼬리표 붙은 합은 합만큼 있습니다. 함수는 입력마다 출력을 하나씩 고르는 일이라, 출력 가짓수를 입력 개수만큼 곱한 거듭제곱만큼 있습니다. A의 원소가 2개, B의 원소가 3개이면, a를 넣었을 때의 출력을 3가지 중에서, b를 넣었을 때의 출력을 다시 3가지 중에서 고르니 3 × 3 = 9가지입니다. 그래서 함수 타입을 $B^A$로 적습니다. 이런 뜻에서 곱과 합으로 짜 맞춘 타입을 대수적 자료형⁠(algebraic data type)⁠이라고 부르고, 학교에서 배운 지수 법칙이 타입의 법칙이 됩니다. 각 법칙의 양변은 원소의 수가 같을 뿐 아니라 자연스럽게 짝지어지는 타입이고, 논리로 읽으면 서로 동치인 명제입니다. 그래서 아래의 등호(=)는 '같은 개수'보다 강한 '빠짐없이 짝지어진다'(≅)의 뜻으로 읽습니다. 타입의 식에서 $0$은 원소가 없는 타입(⊥), $1$은 원소가 하나인 타입(⊤)입니다.

• $C^{A \times B} = (C^B)^A$: 쌍을 받는 함수는 인수를 하나씩 받는 함수와 같습니다(커링). 논리로는 $(A \land B \to C) \leftrightarrow (A \to (B \to C))$. $|A| = 2$, $|B| = 3$, $|C| = 2$이면 양쪽 모두 $2^6 = (2^3)^2 = 64$입니다.
• $C^{A + B} = C^A \times C^B$: 합을 받는 함수는 두 경우를 처리하는 함수의 쌍입니다(case). 논리로는 $(A \lor B \to C) \leftrightarrow (A \to C) \land (B \to C)$. 같은 크기(2, 3, 2)로 세면 왼쪽은 2⁵ = 32, 오른쪽은 2² × 2³ = 4 × 8 = 32입니다.
• $(B \times C)^A = B^A \times C^A$: 쌍을 내는 함수는 함수의 쌍입니다. 논리로는 $(A \to B \land C) \leftrightarrow (A \to B) \land (A \to C)$. 같은 크기로 세면 왼쪽은 6² = 36, 오른쪽은 3² × 2² = 9 × 4 = 36입니다.
• $A^0 = 1$: 빈 집합에서 나가는 함수는 정확히 하나입니다(정할 것이 없으니까요). 논리로는 $\bot \to A$가 늘 참이라는 것, 곧 "모순에서는 무엇이든 따라 나온다"입니다.

원소가 있으면 참, 없으면 거짓이라고 읽으면 세기가 곧 진리표입니다. $A$를 3개, $B$를 0개로 두고 $A \to B$를 보세요. 원소가 3개인 집합에서 빈 집합으로 가는 함수는 없으니, "참이면 거짓"은 거짓입니다. 다만 집합의 세계는 고전 논리의 세계라는 점을 기억해야 합니다. 타입 $A + (A \to 0)$은 논리로 읽으면 "A 또는 A가 아니다", 곧 배중률입니다. 모든 집합은 비었거나 비지 않았으니 이 타입에는 늘 원소가 있습니다. A가 비었으면 A에서 빈 집합으로 가는 함수가 하나 있고($A^0 = 1$과 같은 까닭입니다), 비지 않았으면 A의 원소가 있습니다. 하지만 그 원소를 실제로 집으려면 $A$가 비었는지를 먼저 알아야 합니다. 4절의 프로그램이 해내지 못한 바로 그 일입니다.

요컨대 곱과 합과 함수로 짜 맞춘 타입은 원소의 개수에서도, 논리에서도, 범주에서도 같은 법칙을 따릅니다.

그 무렵, 1963년 컬럼비아 대학에서 에일렌베르크의 지도로 박사 학위를 받은 윌리엄 로베어는 범주론으로 논리 자체를 다시 쓰고 있었습니다. 1969년의 두 논문에서 그는 두 가지를 보였습니다. 하나는 '모든'과 '어떤'이 수반 함자라는 것입니다. 예를 들어 Q가 x에 관한 말이 아닐 때, "Q이면, 모든 x에 대해 P(x)"와 "모든 x에 대해, Q이면 P(x)"는 같은 말입니다. 이 익숙한 법칙이 위의 커링 짝짓기와 같은 모양의 짝짓기라는 뜻입니다. 다른 하나는 칸토어의 정리와 괴델, 타르스키의 결과에 쓰인 대각선 논법이 모두 하나의 고정점 정리에서 나온다는 것입니다. 함수 f의 고정점은 f(y) = y인 y, 곧 f를 적용해도 움직이지 않는 점입니다. 여기서는 둘째 것을 따라갑니다.

먼저 칸토어의 대각선 논법⁠(Cantor's diagonal argument)⁠을 작은 표로 해 봅시다. A = {1, 2, 3}이고, A의 원소 a마다 A에서 {참, 거짓}으로 가는 함수 e(a)를 하나씩 정해 줍니다. e(a)는 1, 2, 3에 참이나 거짓을 하나씩 매기는 것이니, 표의 한 줄로 적을 수 있습니다. e(a)(b)는 'a번째 줄의 b번째 칸'입니다.

굵은 글씨의 대각선, 곧 e(1)(1), e(2)(2), e(3)(3)을 읽으면 참, 거짓, 거짓입니다. 이것을 모두 뒤집은 줄이 맨 아래의 g = (거짓, 참, 참)입니다. g는 e(1)과 첫째 칸에서, e(2)와 둘째 칸에서, e(3)과 셋째 칸에서 다르니, 표의 어느 줄과도 같지 않습니다. 표를 어떻게 채워도 마찬가지입니다. 대각선 칸을 뒤집어 만든 줄은 a번째 줄과 a번째 칸에서 반드시 다르기 때문입니다. 원소가 셋이면 가능한 줄 2³ = 8개를 세 줄로 덮을 수 없다는 것은 세어 봐도 알지만, 이 논법은 세지 않으므로 A가 무한해도 그대로 통합니다.

로베어는 이 논법에서 {참, 거짓}과 '뒤집기'를 빈칸으로 바꾸었습니다. {참, 거짓} 자리에 아무 대상 Y를, 뒤집기 자리에 Y에서 Y로 가는 아무 화살표 f를 넣습니다. 정리의 내용은 이렇습니다. $e : A \to Y^A$는 $A$의 원소 $a$마다 $A$에서 $Y$로 가는 함수 $e(a)$를 하나씩 정해 주는 대응입니다. 데카르트 닫힌 범주에서 $e : A \to Y^A$가 $Y^A$의 모든 원소를 덮는다면, 곧 $Y^A$의 원소가 모두 어떤 $a$에 대한 $e(a)$로 나타난다면, $Y$에서 $Y$로 가는 모든 화살표 $f$에 고정점($f(y) = y$인 $y$)이 있습니다. 일반적인 데카르트 닫힌 범주에는 '원소'가 따로 없으니, 끝 대상 1에서 오는 화살표를 원소로 읽습니다. 집합에서 {★}에서 A로 가는 함수 하나는 ★가 가는 곳 하나, 곧 A의 원소 하나와 같기 때문입니다. 증명은 한 줄입니다.

줄을 풀어 읽으면 이렇습니다. 먼저 대각선을 읽고 f를 씌운 함수 $g(a) = f\bigl(e(a)(a)\bigr)$를 만듭니다($a$번째 함수에 $a$ 자신을 넣은 값에 f를 적용). $g$도 $Y^A$의 원소이니 어떤 $a_0$에 대해 $e(a_0)$이고, 그 $a_0$을 자기 자신에 넣으면 $e(a_0)(a_0) = g(a_0) = f\bigl(e(a_0)(a_0)\bigr)$이니, $y = e(a_0)(a_0)$가 고정점입니다. 표로 말하면, g가 표의 $a_0$번째 줄로 나타난다면 그 줄의 대각선 칸 y는 f를 씌워도 그대로여야 한다는 것입니다.

이제 거꾸로 읽습니다. "모두 덮으면 고정점이 있다"는 "고정점이 없는 f가 하나라도 있으면 모두 덮을 수는 없다"와 같은 말입니다. $Y$를 {참, 거짓}으로, $f$를 '아니다'로 두면, '아니다'에는 고정점이 없으니(참을 뒤집으면 거짓, 거짓을 뒤집으면 참) $A$에서 $A$의 부분집합⁠(subset)⁠ 전체로 가는 대응은 모든 부분집합을 덮을 수 없습니다. $A$에서 {참, 거짓}으로 가는 함수 하나가 곧 $A$의 부분집합 하나(참이 나오는 원소들의 모임)이기 때문입니다. 칸토어의 정리(멱집합⁠(power set)⁠, 곧 부분집합 전체의 집합은 언제나 원래 집합보다 크다)입니다. 앞의 표가 A = {1, 2, 3}에서 본 바로 그 경우입니다.

같은 뼈대에 다른 것을 끼우면 괴델의 불완전성 정리⁠(incompleteness theorem)⁠의 핵심 단계, 곧 "이 문장은 증명되지 않는다"처럼 자기 자신에 대해 말하는 문장을 만드는 단계가 나오고, 러셀의 역설과 튜링의 정지 문제도 같은 모양으로 설명됩니다(뒤의 것들은 뒷날 여러 사람이 풀어 적었습니다). 1절과 3절에서 본 괴물, 곧 자기 참조로 모순이나 불가능을 끌어내는 논법의 공통 뼈대가 범주의 언어로 한 줄이 된 것입니다. 대각선 논법이 불변량⁠(invariant)⁠, 세기와 함께 "없다"를 증명하는 세 가지 무기 가운데 하나라는 이야기는 「불가능의 증명」 7절에서, 로베어가 집합과 논리 전체를 화살표로 다시 쓴 과정은 「화살표만으로 본 수학」 7절에서 볼 수 있습니다.

7 · 1978년 에든버러타입을 적지 않아도: 힌들리–밀너

이 절의 물음은 이것입니다. 프로그래머가 타입을 하나도 적지 않아도, 기계가 프로그램만 보고 타입을 알아낼 수 있을까? 답은 "대개 그렇다"이고, 방법은 중학교에서 배운 연립방정식 풀기와 닮았습니다.

로빈 밀너는 1970년대 초, 컴퓨터로 증명을 돕는 체계 LCF를 만들고 있었습니다. 스탠퍼드에서 시작해 에든버러 대학으로 가져온 작업입니다. 1971년 존 매카시의 스탠퍼드 인공지능⁠(artificial intelligence)⁠ 연구소에 들어간 그는 데이나 스콧이 제안한 '계산 가능한 함수의 논리'(LCF라는 이름이 여기서 왔습니다)로 프로그램의 성질을 증명하는 일을 기계로 돕는 체계를 만들었습니다. 그런데 이 첫 체계는 정해진 명령만 하나씩 쳐 넣을 수 있어서, 같은 모양의 증명을 되풀이할 때마다 사람이 손으로 다시 해야 했습니다.

1973년 에든버러로 옮긴 밀너는 명령들을 조합하는 프로그램을 쓸 수 있게 하기로 했습니다. 사용자가 증명 전략을 프로그램으로 짜게 하고, 그 프로그램을 쓰는 언어로 ML(메타 언어)을 만들었습니다. ML의 타입에는 영리한 장치가 있었습니다. '정리'라는 타입의 값은 논리의 추론 규칙을 통해서만 만들 수 있게 해서, 사용자가 무슨 프로그램을 짜든 가짜 정리가 나올 수 없게 한 것입니다. 타입 검사가 곧 증명의 안전장치였습니다.

그런데 3절의 언어처럼 모든 변수에 타입을 일일이 적는 것은 번거롭습니다. 게다가 "목록을 뒤집는 함수"는 정수의 목록에도 글자의 목록에도 쓸 수 있어야 하니 타입을 하나로 정해 적을 수도 없습니다. 밀너는 1978년 논문 「프로그래밍에서 타입 다형성⁠(polymorphism)⁠의 이론」에서 타입을 하나도 적지 않은 프로그램의 가장 일반적인 타입을 기계가 찾아내는 방법(알고리즘 W)을 내놓았습니다. 그리고 이렇게 타입이 정해진 프로그램은 실행 중에 "잘못될 수 없다"는 것을 증명했습니다. 웨일스의 로저 힌들리가 1969년 조합 논리에서 이미 같은 생각에 이르렀기에, 오늘날 이 방법을 힌들리–밀너 타입 추론⁠(type inference)⁠이라고 부릅니다. 둘 다 1965년 존 앨런 로빈슨이 자동 정리 증명을 위해 만든 단일화⁠(unification)⁠ 알고리즘을 씁니다.

방법은 방정식 풀기와 같습니다. 모르는 타입마다 $\alpha, \beta, \ldots$ 같은 이름을 붙이고, 프로그램에서 방정식을 뽑아 푸는 것입니다. $\lambda x.\, M$의 타입은 그냥 ($x$의 타입) → ($M$의 타입)으로 적으면 되니, 방정식을 만드는 규칙은 하나뿐입니다. 적용 $M\,N$이 있으면 "$M$의 타입 = ($N$의 타입) → (결과의 타입)"입니다. 프로그램 로 해 봅시다. 그림 아래의 ▶| 단추를 누를 때마다 방정식 하나가 풀리고, 그 아래 식에 남은 방정식과 지금까지 정한 것이 나옵니다.

λf. λx. f (f x), 곧 "함수를 두 번 적용하라"를 따라가 봅시다. 처음에는 $f : \alpha$, $x : \beta$이고, 바깥 적용의 결과를 $\gamma$, 안쪽 적용 $f\,x$의 결과를 $\delta$라 합니다. 안쪽 적용 $f\,x$에서 $\alpha = \beta \to \delta$, 바깥 적용에서 $\alpha = \delta \to \gamma$가 나옵니다. 첫 방정식으로 $\alpha$를 정하면 둘째는 $\beta \to \delta = \delta \to \gamma$가 되고, 화살표끼리 같으려면 앞끼리, 뒤끼리 같아야 하니 $\beta = \delta = \gamma$입니다. 그러면 $f : \gamma \to \gamma$, $x : \gamma$이고 전체의 타입은 $(\gamma \to \gamma) \to \gamma \to \gamma$입니다. 이름을 α부터 다시 붙이면 답은 $(\alpha \to \alpha) \to \alpha \to \alpha$. "어떤 타입이든 자기 자신으로 가는 함수를 주면, 그 타입의 값을 받아 같은 타입의 값을 돌려주겠다"입니다. 이 타입은 가장 일반적인 타입(주 타입⁠, principal type⁠)이어서, 이 프로그램이 가질 수 있는 다른 모든 타입, 예를 들어 (정수 → 정수) → 정수 → 정수는 $\alpha$에 무언가를 넣어 얻어집니다. 힌들리와 밀너의 정리는 타입이 있는 모든 프로그램에 이런 주 타입이 있고 알고리즘이 그것을 찾는다는 것입니다(완전성은 1982년 루이스 다마스와 밀너가 증명했습니다).

이제 λx. x x를 골라 보세요. 방정식은 $\alpha = \alpha \to \beta$ 하나입니다. $\alpha$가 오른쪽 안에 들어 있어서, 풀려고 넣을수록 식이 길어지기만 합니다. 알고리즘은 이것을 '발생 검사⁠(occurs check)⁠'로 알아채고 멈춥니다. 1절의 $x \in x$, 3절의 $\omega$가 여기서는 풀리지 않는 방정식으로 나타납니다.

정리하면, 타입 추론은 모르는 타입을 미지수로 두고 방정식을 풀어 가장 일반적인 답을 찾는 일입니다.

힌들리–밀너 추론은 실제 프로그램에서는 대개 빠릅니다. 하지만 일부러 꼬아 만든 프로그램에서는 타입이 프로그램 길이의 지수 함수보다도 빨리 길어질 수 있고, 타입이 있는지 판정하는 일조차 최악의 경우 다항 시간⁠(polynomial time)⁠에 끝내는 알고리즘이 없다는 것(DEXPTIME-완전, 곧 입력 길이의 지수 함수만큼의 시간이 드는 문제들 가운데 가장 어려운 축이라는 뜻)이 1990년에 증명되었습니다. 다항 시간이란 입력 길이 n에 대해 걸음 수가 $n^2$, $n^3$처럼 n의 거듭제곱 정도로 묶인다는 뜻입니다. 더 강한 타입도 있습니다. 1972년 파리의 장이브 지라르가, 1974년 미국의 존 레이놀즈가 따로 만든 시스템 F⁠(System F)⁠는 "모든 타입 $\alpha$에 대해"를 타입 안에 직접 쓸 수 있게 했습니다(다형성). 대신 시스템 F에서는 타입을 적지 않은 프로그램의 타입을 찾는 일이 결정 불가능하다는 것이 1990년대에 증명되었습니다. 표현력과 자동 추론은 한쪽을 얻으면 다른 쪽을 내주어야 하는 관계입니다.

다형성은 5절의 자연성과 뜻밖의 방식으로 만납니다. 레이놀즈의 1983년 연구와 필립 와들러의 1989년 논문 「공짜로 얻는 정리」에 따르면, 타입이 $\forall \alpha.\, \mathrm{List}\,\alpha \to \mathrm{List}\,\alpha$('모든 타입 α에 대해, α의 목록을 받아 α의 목록을 낸다')인 함수는 어떤 것이든 자동으로 자연 변환입니다. 모든 $\alpha$에 대해 한 가지 방식으로 동작해야 하니 원소를 들여다볼 수가 없고, 그래서 5절의 네모가 저절로 닫힙니다. 정렬은 이 타입을 가질 수 없습니다. 원소를 비교하는 방법이 따로 있어야 하기 때문입니다. 타입만 보고 프로그램의 성질을 정리로 얻는 것입니다. (끝나지 않는 계산이나 예외가 있는 언어에서는 이 정리에 조건이 조금 붙습니다.)

ML의 후손은 널리 퍼졌습니다. 표준 ML과 OCaml, F#이 ML을 직접 잇고, 1990년 위원회가 만든 하스켈이 같은 추론 위에 서 있습니다. 이 위원회는 1987년 9월 미국 포틀랜드의 함수형 언어⁠(functional programming language)⁠ 학회에서, 비슷한 순수 함수형 언어가 열 개 넘게 따로 자라는 상황을 하나로 모으자는 뜻으로 꾸려졌습니다. 언어 이름은 커리의 이름에서 따왔습니다. 곱과 합으로 새 타입을 짓고 경우를 나누어 처리하는 방식은 1980년 에든버러의 언어 Hope에서 시작되었고, 6절의 대수적 자료형 그대로입니다. 러스트, 스위프트, 코틀린, 스칼라, 타입스크립트 같은 오늘날의 언어들도 이 전통에서 타입 추론과 대수적 자료형(또는 그것을 닮은 장치)을 가져왔습니다. 모두 힌들리–밀너를 그대로 쓰지는 않고, 각자의 사정에 맞게 고쳐 씁니다.

커리–하워드에서 오늘까지. 몬트리올, 스완지와 에든버러, 스톡홀름과 파리 근교의 연구소, 그리고 증명 보조기가 수학의 큰 정리를 만난 케임브리지, 피츠버그, 본으로 이어지는 선을 따라가 보세요. 과학 줄(청록)에는 LCF, Coq, 하스켈 같은 도구가 있습니다.

8 · 1989년계산의 부작용에도 타입을: 모지의 모나드⁠(monad)⁠

이 절의 물음은 이것입니다. 수학의 함수는 같은 입력에 늘 같은 출력을 냅니다. 실제 프로그램은 그렇지 않습니다. 실패하기도 하고, 저장된 값을 바꾸기도 하고, 화면에 글을 쓰고, 네트워크의 답을 기다립니다. 이런 '부작용'을 람다 계산과 범주론의 깔끔한 세계에 어떻게 들일까요?

에든버러에서 박사 학위를 받은 에우제니오 모지는 1989년 논문 「계산 람다 계산과 모나드」에서 답을 내놓았습니다. $A$ 값을 내는 계산을 타입 $T A$의 값으로 보자는 것입니다. 여기서 $T$는 모나드입니다. 범주론에서 1950–60년대부터 알려진 구조입니다(이름의 내력은 이 절 끝에 적었습니다). 대수적 위상수학의 계산 도구가 30년 뒤 프로그램의 부작용을 다루는 틀이 된 것입니다.

가장 쉬운 예는 실패할 수 있는 계산입니다. $T A = A + 1$, 곧 "$A$ 값이거나, '없음'"입니다. 계산 세 개를 이어 봅시다. 먼저 $1/x$(0이면 실패), 다음은 $\sqrt{\ }$(음수면 실패), 마지막은 $1/(z - 1)$($z = 1$이면 실패)입니다. 손으로 해 보면, x = 4일 때 1/4 = 0.25, 그 제곱근 0.5, 1/(0.5 − 1) = −2로 끝까지 갑니다. x = 1이면 1, 1까지 가다가 셋째 단계에서 1/(1 − 1)이 되어 실패합니다. 입력을 끌어 바꿔 보세요. 지금은 $x =$ 입니다.

한 단계가 실패하면 나머지는 건너뛰고 '없음'을 넘깁니다. 이 '이어 붙이기'를 매번 손으로 쓰지 않게 해 주는 것이 모나드입니다. 모나드는 세 가지로 이루어집니다. 타입을 타입으로 보내는 함자 $T$, 보통 값을 계산으로 감싸는 $\mathrm{return} : A \to T A$, 그리고 효과가 있는 함수 둘을 이어 붙이는 방법입니다. 실패의 예에서 return은 값 v를 '실패하지 않은 v'로 감싸는 일이고, 이어 붙이기는 '앞 단계가 성공했으면 그 값을 다음 단계에 넣고, 실패했으면 실패를 그대로 넘기는' 일입니다. $f : A \to T B$와 $g : B \to T C$를 이은 것을 $f \mathbin{>\!\!=\!\!>} g : A \to T C$로 적으면('f 다음 g'라 읽습니다. $A$를 받아 먼저 $f$를 실행하고, 그 결과를 $g$에 넘깁니다. 실패의 예라면 성공했을 때만 넘깁니다), 모나드 법칙은 다음 세 줄입니다.

말로 읽으면, 첫째와 둘째 줄은 "아무 효과 없이 감싸기만 하는 return을 앞이나 뒤에 이어 붙여도 달라지는 것이 없다"이고, 셋째 줄은 "세 단계를 이을 때 앞의 둘을 먼저 잇든 뒤의 둘을 먼저 잇든 같다"입니다.

왜 하필 이 법칙들일까요? 5절의 범주의 정의를 다시 보세요. 항등 화살표는 이어 붙여도 아무것도 바꾸지 않고, 이어 붙이기는 괄호를 어디에 치든 같습니다. 모나드 법칙은 $A \to T B$ 꼴의 '효과 있는 함수'들이 그 자체로 하나의 범주를 이룬다는 말과 정확히 같습니다(클라이슬리 범주⁠, Kleisli category⁠). 그래서 쓸모가 있습니다. 세 단계짜리 계산을 앞의 두 단계와 뒤의 한 단계로 묶든, 앞의 한 단계와 뒤의 두 단계로 묶든 뜻이 같으니, 프로그래머는 긴 계산을 마음대로 함수로 쪼개고 다시 합칠 수 있습니다. 정리하면, 모나드는 효과 있는 함수들도 보통 함수처럼 이어 붙일 수 있게 해 주는 구조입니다.

"모나드는 자기 함자들의 범주의 모노이드⁠(monoid)⁠일 뿐"이라는 매클레인 교과서의 유명한 문장도 같은 말입니다. 모노이드는 결합 법칙을 따르는 곱셈과 항등원⁠(identity element)⁠만을 요구하는 대수 구조이고(수의 곱셈과 1이 그 예입니다), 모나드는 그 곱셈 자리에 함자의 합성을 놓은 것입니다. 또 모든 수반 함자의 쌍이 모나드 하나를 낳고, 거꾸로 모든 모나드는 수반에서 나온다는 것은 1965년 하인리히 클라이슬리가, 그리고 따로 에일렌베르크와 존 무어가 보였습니다.

필립 와들러가 1990년대 초, 특히 1992년 논문 「함수형 프로그래밍의 본질」로 모지의 생각을 함수형 프로그래밍에 소개했습니다. 하스켈에는 절실한 사정이 있었습니다. 순수 함수만 쓰는 언어라 화면에 글을 쓰거나 파일을 읽는 일을 깔끔하게 적을 방법이 없었고, 하스켈의 설계자들 스스로 초기의 입출력이 몹시 어색했다고 회고합니다. 1996년 5월의 하스켈 1.3 보고서가 입출력 전체를 모나드로 다루는 방식을 표준으로 정했습니다. 오늘날의 언어에도 흔적이 많습니다. 값이 없을 수도 있는 식을 a?.b?.c처럼 이어 쓰는 문법, 실패를 곧바로 위로 넘기는 러스트의 ?, 네트워크의 답을 기다리는 async/await가 모두 모나드의 이어 붙이기를 편하게 쓰게 해 주는 문법입니다. 다만 자바스크립트의 Promise는 감싼 것을 한 번 더 감싸면 저절로 풀어 버리는 탓에 모나드 법칙을 엄밀히 지키지는 않습니다. 이름이 모나드인지보다 법칙을 지키는지가 중요합니다.

모나드라는 구조는 1958년 프랑스의 로제 고드망이 층의 코호몰로지(공간의 조각마다 붙인 자료를 전체로 이어 붙일 때 생기는 걸림돌을 재는 계산)를 구하는 '표준 구성'으로 처음 썼고, 1960–70년대에는 '트리플'이라는 이름으로 많이 불렸으며, 1960년대 후반 장 베나부가 제안한 '모나드'라는 이름이 결국 자리를 잡았습니다.

9 · 1967–2022기계가 검사하는 증명: 오토마스에서 Lean까지

이 절의 물음은 이것입니다. 타입이 수학의 진짜 명제를 말하게 하려면 무엇이 더 필요할까? 그리고 그런 타입으로 실제 수학의 큰 정리를 검사할 수 있을까?

4절 끝에서 남긴 문제로 돌아갑시다. 일상의 타입은 시시한 명제밖에 말하지 못합니다. "정수 두 개를 받아 정수를 내놓는다"는 덧셈에도 뺄셈에도 맞는 타입입니다. 타입이 "이 함수는 $n$과 0을 받으면 $n$을 내놓는다" 같은 것을 말하려면, 타입이 값에 따라 달라질 수 있어야 합니다. 이런 타입을 의존 타입⁠(dependent type)⁠이라고 합니다.

예를 들어 원소의 타입이 $A$이고 길이가 $n$인 목록의 타입을 $\mathrm{Vec}\,A\,n$으로 적으면(타입 안에 수 n이 들어 있습니다), 목록의 첫 원소를 꺼내는 함수의 타입을 $\mathrm{Vec}\,A\,(n+1) \to A$로 적을 수 있습니다. 길이가 $n+1$인 목록은 적어도 원소가 하나 있으니 첫 원소가 반드시 있습니다. 그래서 이 함수를 빈 목록(길이 0)에 쓰는 잘못은 실행하기 전에 타입 오류가 됩니다. 0은 어떤 $n$에 대해서도 $n+1$의 꼴이 아니기 때문입니다.

그러면 2절의 BHK 표의 마지막 줄이 이제 문자 그대로 프로그램이 됩니다. "모든 자연수 n에 대해 n + 0 = n"의 증명은, 수 n을 받아 "n + 0 = n"의 증명을 돌려주는 함수입니다. 3을 넣으면 "3 + 0 = 3"의 증명이, 7을 넣으면 "7 + 0 = 7"의 증명이 나옵니다. 돌려주는 것의 타입이 넣은 값 n에 따라 달라진다는 점이 보통의 함수 타입 $A \to B$와 다릅니다. 일반적으로 "모든 $x$에 대해 $P(x)$"의 증명은 $x$를 받아 $P(x)$의 증명을 돌려주는 함수이고, 이런 함수의 타입을 Π 타입('파이 타입')이라 부릅니다. 한편 "$P(x)$인 $x$가 있다"의 증명은 $x$ 하나와 증명의 쌍입니다. "짝수인 수가 있다"라면 (4, "4 = 2 × 2"의 증명)입니다. 쌍의 둘째 것의 타입이 첫째 값에 따라 달라지는 이 타입을 Σ 타입('시그마 타입')이라 부릅니다. 이름은 6절의 세기에서 왔습니다. Π는 여러 수의 곱을, Σ는 여러 수의 합을 한꺼번에 적는 기호입니다. 함수 타입 $B^A$의 원소 수가 B의 원소 수를 A의 원소 개수만큼 곱한 것이었듯, Π 타입의 원소 수는 넣는 값마다 달라지는 타입들의 원소 수를 모두 곱한 것입니다. 마찬가지로 Σ 타입의 원소 수는 첫째 값마다 가능한 둘째 것의 개수를 모두 더한 것입니다.

자연수에 관한 수학적 귀납법⁠(mathematical induction)⁠의 증명은 자연수 위의 재귀 함수가 됩니다. $0$의 경우를 증명하고, $n$의 증명을 받아 $n+1$의 증명을 만드는 함수를 주면, 그 함수를 $n$번 되풀이해 어떤 $n$의 증명이든 만들어 냅니다. 3의 증명이 필요하면, 0의 증명에 그 함수를 세 번 적용해 1, 2, 3의 증명을 차례로 얻습니다. 재귀 함수가 반드시 끝나야 하는 까닭이 여기서 보입니다. 끝나지 않는 '증명'은 아무것도 건네지 않기 때문입니다.

이 생각을 처음 기계로 만든 사람은 네덜란드 에인트호번의 니콜라스 호베르트 더브라윈입니다. 1967년 그가 시작한 오토마스는 수학 문헌을 기계가 검사할 수 있게 적는 언어였고, 명제를 타입으로 다루는 생각을 하워드와는 따로 썼습니다. 1977년 그의 학생 L. S. 판벤템 유팅은 에드문트 란다우의 해석학⁠(mathematical analysis)⁠ 교과서 『해석학의 기초』 한 권 전체를 오토마스로 옮겨 검사했습니다. 자연수에서 출발해 분수, 실수, 복소수⁠(complex number)⁠를 차례로 세우는 이 교과서 한 권이 기계가 한 줄씩 검사하는 오토마스 글이 되었고, 판벤템 유팅은 이 작업으로 1979년 박사 학위를 받았습니다.

스톡홀름의 페르 마르틴뢰프는 1970년대에 의존 타입 이론을 직관주의 수학의 기초로 다듬었습니다. 그의 첫 체계(1971)에는 '모든 타입의 타입'이 자기 자신을 원소로 가지는 규칙이 있었습니다. 지라르가 1972년 그 체계에서 모순을 찾아냈습니다. 부랄리포르티 역설⁠(Burali-Forti paradox)⁠을 타입으로 옮긴 것입니다. 순서수⁠(ordinal number)⁠는 '첫째, 둘째, 셋째, …'를 무한 너머까지 이어 가는 순서의 수입니다. 모든 순서수를 모으면 그것이 다시 더 큰 순서수를 낳으니, '가장 큰 순서수'를 생각하면 모순이 생긴다는 것이 이 역설입니다. 러셀의 역설과 같은 집안입니다. 마르틴뢰프는 타입들을 모은 '우주'를 0층, 1층, 2층, …으로 나누어, 어느 우주도 자기 자신을 원소로 갖지 않게 해서 이를 고쳤습니다. 70년 전 러셀이 한 처방이 그대로 되풀이된 것입니다.

그 뒤를 이은 것이 오늘날의 증명 보조기들입니다. 1985년 파리 근교 INRIA의 티에리 코캉과 제라르 위에는 구성의 계산⁠(calculus of constructions)⁠을 만들었습니다. 의존 타입과 7절에서 본 '모든 타입에 대해'를 함께 쓸 수 있는 타입 체계입니다. 1989년 그 위에서 Coq가 나왔습니다(2025년 Rocq로 이름을 바꾸었습니다). 공티에는 이것으로 2005년 무렵 4색 정리를 검사했고, 2012년에는 여러 동료와 6년에 걸쳐 군론⁠(group theory)⁠의 홀수 차수 정리를 검사했습니다. 파이트–톰프슨 정리라고도 부르는 이 정리는, 원소의 개수가 홀수인 유한군⁠(finite group)⁠은 모두 가해군⁠(solvable group)⁠이라는 것입니다. 가해군은 교환 법칙이 성립하는 군들로 차례차례 쪼갤 수 있는 군입니다. 사람이 쓴 원래 증명만 250쪽이 넘는 정리입니다.

밀너의 LCF에서 이어진 HOL(고차 논리, Higher-Order Logic) 계열 체계는 처치의 1940년 단순 타입 이론을 논리로 씁니다. 토머스 헤일스는 1998년 공 쌓기에 관한 케플러의 추측을 증명했지만, 컴퓨터 계산이 많은 증명을 심사한 이들은 "99% 확신한다"는 이상의 말을 하지 못했습니다. 헤일스가 이끈 플라이스펙 계획은 2014년 8월 HOL Light와 Isabelle로 증명 전체의 검사를 마쳤습니다.

증명 보조기가 수학 밖에서 먼저 돈을 번 곳은 반도체 공장이었습니다. HOL은 1980년대 케임브리지의 마이크 고든이 칩의 설계가 명세대로 동작한다는 것을 증명하려고 LCF를 고쳐 만든 체계입니다. 1994년 여름, 쌍둥이 소수⁠(twin primes)⁠의 역수⁠(inverse)⁠ 합을 계산하던 수학자 토머스 나이슬리가 인텔 펜티엄 칩의 나눗셈이 드물게 틀린 값을 낸다는 것을 알아챘습니다. 나눗셈 회로가 쓰는 표에서 몇 칸이 빠져 있었던 것입니다. 인텔은 칩을 바꿔 주느라 4억 7,500만 달러쯤을 썼고, 그 뒤 칩 회사들은 연산 회로를 시험만 하지 않고 증명 보조기로 검사하기 시작했습니다. 인텔의 존 해리슨은 HOL Light로 부동소수점(컴퓨터가 유효숫자 몇 자리와 지수로 소수⁠(prime number)⁠를 적는 방식) 나눗셈과, 사인⁠(sine)⁠이나 로그 같은 함수의 값을 계산하는 방법이 정확하다는 것을 증명했고, 그 HOL Light가 플라이스펙의 도구가 되었습니다. 나이슬리의 계산 이야기는 「소수를 세는 사람들」 8절에 있습니다.

2013년 마이크로소프트 연구소에서 레오나르두 드 모라가 시작한 Lean과, 2017년 사용자들이 만들기 시작한 수학 도서관 mathlib은 증명 보조기를 연구 수학의 현장으로 데려왔습니다. 2020년 12월 필즈상⁠(Fields Medal)⁠ 수상자 페터 숄체는 자신도 모든 세부를 확신하지 못하는 최근 결과 하나를 기계로 검사해 달라는 도전을 내걸었습니다(액체 텐서⁠(tensor)⁠ 실험). 요한 코멜린이 이끈 사람들이 2021년 6월 핵심 부분을, 2022년 7월 전체를 Lean으로 검사했습니다. 2023년 말에는 팀 가워스, 벤 그린, 프레디 매너스, 테런스 타오가 조합론⁠(combinatorics)⁠의 추측 하나(다항 프라이먼–루자 추측의, 덧셈과 곱셈을 2로 나눈 나머지⁠(remainder)⁠로 하는 수 체계⁠(number system)⁠ {0, 1} 위의 벡터 공간의 경우)를 증명했고, 그 증명은 발표 3주 남짓 만에 Lean으로 검사되었습니다.

무엇이 보장되는지 정확히 말해 둡시다. 증명 보조기가 확인하는 것은 "이 프로그램의 타입이 이 명제이다", 곧 적힌 명제가 적힌 공리에서 따라 나온다는 것입니다. 믿어야 하는 것은 셋입니다. 타입을 검사하는 작은 핵심 프로그램, 사용한 공리, 그리고 기계에게 준 명제가 우리가 뜻한 명제와 같다는 것입니다. 마지막 것은 기계가 대신해 줄 수 없습니다. 틀린 명제를 정확히 증명할 수도 있기 때문입니다. 머리말에서 본 티모치코의 물음에 증명 보조기가 내놓는 답도 여기에 있습니다. 컴퓨터를 믿는 몫을 없애지는 못하지만, 믿어야 할 것을 수많은 경우의 계산에서 작고 공개된 핵심 프로그램 하나로 줄입니다. 또 Lean은 선택공리(비어 있지 않은 집합들 각각에서 원소를 하나씩 동시에 고를 수 있다는 공리)를 공리로 두고(배중률은 여기서 정리로 따라 나옵니다), mathlib은 이 공리를 자유롭게 사용해 고전 수학을 그대로 전개합니다. 그런 증명은 여전히 기계가 검사하는 '프로그램'이지만, 2절의 뜻에서 무언가를 계산해 건네는 구성은 아닙니다. 커리–하워드는 증명 보조기를 가능하게 한 설계 원리이지, 모든 수학이 구성적이어야 한다는 결론이 아닙니다.

이 이야기의 마지막 장은 한 수학자의 불안에서 나왔습니다. 2002년 필즈상을 받은 블라디미르 보예보츠키는 뒷날, 자신이 1989년 공저한 논문의 주장이 틀렸다는 지적을 1998년에 받았지만 스스로 확신하기까지 15년이 걸렸다고 회고했습니다(그 경위와, 아무도 틀린 줄을 짚지 못한 채 결과가 조용히 버려진 사정은 「틀린 증명이 만든 수학」 8절에 있습니다). 사람의 검토만으로는 복잡한 증명을 믿을 수 없다고 느낀 그는, 수학을 처음부터 기계가 검사할 수 있는 기초 위에 다시 세우는 일에 나섰습니다.

그가 무엇을 했는지 보려면, 먼저 타입 이론에서 '같다'가 어떻게 다뤄지는지 알아야 합니다. 마르틴뢰프 타입 이론에서는 "a와 b가 같다"도 하나의 명제이니, 커리–하워드에 따라 하나의 타입입니다. 이 '같음' 타입을 $a = b$로 적고, 그 원소는 "a와 b가 같다"의 증명입니다. 그러면 뜻밖의 물음이 생깁니다. 같다는 증명이 서로 다른 것으로 둘 이상 있을 수 있을까요?

수의 경우라면 이 물음이 이상하게 들리지만, 타입끼리의 '같음'을 생각하면 자연스럽습니다. 원소가 둘인 두 타입 {0, 1}과 {빨강, 파랑}을 봅시다. 둘을 같은 꼴로 짝짓는 방법은 두 가지입니다. 0을 빨강, 1을 파랑과 짝짓거나, 0을 파랑, 1을 빨강과 짝짓는 것입니다. 두 타입이 '같은 꼴'이라고 말할 때, 그 근거가 서로 다른 두 가지로 있는 셈입니다.

보예보츠키가 붙잡은 생각은 같음 타입⁠(identity type)⁠ $a = b$를 공간 속의 경로로 읽는 것이었습니다. $a = b$의 증명은 점 $a$에서 점 $b$로 가는 길이고, 두 증명이 같다는 증명은 한 길을 다른 길로 연속해서 옮기는 변형(두 길 사이를 채우는 면)입니다. 이런 연속 변형을 호모토피라고 부릅니다. 길이 여럿일 수 있듯 같음의 증명도 여럿일 수 있습니다. 원 위의 한 점에서 출발해 제자리로 돌아오는 길로 '가만히 있기', '한 바퀴 돌기', '두 바퀴 돌기'가 있는데, 원을 벗어나지 않고는 어느 것도 다른 것으로 연속해서 바꿀 수 없는 것과 같습니다. 그러면 타입은 점과 길과 면과 그 위의 모든 층으로 이루어진 공간으로 읽힙니다. 이 읽기의 싹은 1990년대 마르틴 호프만과 토마스 슈트라이허의 모형에 있었고, 2000년대 중반 스티브 어위디와 마이클 워런도 보예보츠키와 따로 같은 해석에 이르렀습니다.

그 위에서 그는 일가성 공리⁠(univalence axiom)⁠를 내놓았습니다. 타입들을 모은 한 '우주'(타입들의 타입. 앞에서 본, 층으로 나눈 우주 가운데 하나) 안의 두 타입 $A, B$에 대해

≃는 '동치'라고 읽습니다. 타입 사이의 동치는 같은 꼴로 짝짓는 대응이고, {0, 1}처럼 집합과 같이 행동하는 타입 사이에서는 빠짐도 겹침도 없는 일대일 짝짓기입니다. 식의 왼쪽은 "A와 B가 같다는 것의 증명들"의 타입, 오른쪽은 "A와 B 사이의 동치들"의 타입이고, 공리는 이 둘이 다시 동치라고 말합니다. 곧 "같다는 것"과 "같은 꼴이다"가 같은 것이라는 공리입니다. 앞의 예로 말하면, {0, 1}과 {빨강, 파랑}이 같다는 증명은 짝짓기의 수만큼, 곧 정확히 두 개 있습니다. 정확히는, 같음의 증명을 동치로 바꾸는 표준적인 대응(같은 것은 당연히 같은 꼴이니 늘 있는 대응) 자체가 동치라는 것입니다.

이것이 왜 쓸모 있을까요? 수학자들은 늘 같은 꼴인 대상을 같은 것처럼 다룹니다. 원소 이름만 다른 두 군은 같은 군이라고 말합니다. 보통의 집합론에서 이것은 말버릇일 뿐이라, 매번 "이 성질은 같은 꼴을 따라 옮겨진다"를 따로 확인해야 합니다. 일가성 공리 아래에서는 이것이 정리가 됩니다. 같은 꼴이라는 증명이 곧 같음의 증명으로 바뀌고, 타입 이론에서는 무엇이든 같음의 증명을 따라 옮길 수 있으니, 한쪽에 대해 증명한 것은 모두 다른 쪽에도 성립합니다. 이것이 가능한 까닭은 물을 수 있는 질문이 다르기 때문입니다. 집합론에서는 "이 군의 원소 가운데 수 1이 있는가"처럼 같은 꼴을 따라 옮겨지지 않는 질문도 할 수 있지만, 타입 이론의 언어로는 그런 질문을 애초에 적을 수 없습니다. 정리하면, 일가성 공리는 '같은 꼴이면 같은 것으로 다뤄도 된다'는 수학자의 습관을 공리 하나로 정확하게 만든 것입니다.

2012–13년 프린스턴 고등연구소의 특별 연도에 모인 수학자와 컴퓨터 과학자들이 함께 쓴 책 『호모토피 타입 이론⁠(homotopy type theory)⁠』(2013)이 이 생각을 정리했습니다. 공리로 덧붙인 일가성은 계산을 멈추게 합니다. 기계가 그 공리를 만나면 더 풀 방법이 없기 때문입니다. 예를 들어 자연수를 내놓아야 하는 프로그램이 끝까지 계산해도 0, 1, 2 같은 수가 되지 않고, 공리 앞에서 멈춘 식으로 남을 수 있습니다. 2015년 무렵 티에리 코캉과 동료들이 내놓은 입방 타입 이론(길을 0과 1 사이의 구간에서 오는 함수로 직접 다루는 체계)에서는 일가성이 공리가 아니라 계산할 수 있는 정리가 됩니다.

10 · 이어지는 길증명과 프로그램이 닿는 곳

명제를 타입으로, 증명을 프로그램으로 읽는 커리–하워드 대응, 기계가 타입을 찾아 주는 타입 추론, 값에 따라 달라지는 의존 타입과 그 위의 호모토피 타입 이론은 수학의 여러 갈래와 이어져 있습니다.

• 계산의 한계로: 이 글에서 본 체계의 타입 검사는 실행하지 않고도 반드시 끝나는 판정이지만, 프로그램이 멈추는지는 판정할 수 없습니다(정지 문제). 모든 계산이 끝나는 언어가 끝나는 계산조차 모두 담지 못하는 까닭도 같은 대각선 논법입니다. 재귀 연산자⁠(operator)⁠ fix를 더해 끝나지 않는 계산을 허락하면, 그 뜻은 영역 이론⁠(domain theory)⁠의 최소 고정점⁠(least fixed point)⁠으로 정합니다. 타입만으로는 적기 어려운 '이 반복문은 t 이상인 첫 칸을 돌려준다' 같은 성질은 호어 논리⁠(Hoare logic)⁠의 불변식으로 증명합니다. 괴델과 튜링의 이야기는 「기계가 풀 수 없는 문제」에 있습니다.
• 무한으로: 러셀의 층과 브라우어르의 직관주의는 무한을 어떻게 다룰지를 두고 나온 두 가지 대답이고, 칸토어의 정리를 한 줄로 줄인 로베어의 고정점 정리는 무한에도 크기의 차이가 생기는 까닭을 보여 줍니다. 집합과 멱집합의 크기는 「무한에도 크기가 있다」에서 이어집니다.
• 세기로: 6절에서 타입의 원소를 센 규칙(곱은 곱, 합은 합, 함수는 거듭제곱)은 경우의 수⁠(number of cases)⁠를 세는 조합론의 곱의 법칙⁠(rule of product)⁠과 합의 법칙⁠(rule of sum)⁠ 그 자체입니다. 재귀적인 타입의 원소를 세면 생성함수⁠(generating function)⁠가 나옵니다. 리스트나 나무 같은 재귀 타입은 $X \mapsto 1 + A \times X$ 같은 규칙의 가장 작은 해, 곧 시작 대수이고, 그 구조를 따라 값을 접어 가는 함수(fold, 예를 들어 목록의 합)가 하나로 정해진다는 사실이 수학적 귀납법을 범주의 말로 적은 것입니다. 「세지 않고 세기」에서 이어 보세요.
• 구조로: 범주론은 군의 준동형, 위상수학의 연속 함수, 선형 사상을 같은 말로 다룹니다. 함자와 자연 변환, 요네다 보조정리, 수반은 대상을 안이 아니라 관계로 보는 표현 바꾸기를 가장 멀리 밀고 간 형태입니다. 순서 집합 사이의 수반은 갈루아 연결⁠(Galois connection)⁠이 되어 정수 나눗셈과 곱셈, 체와 군의 대응 같은 오래된 짝을 한 말로 적고, 곱 대신 텐서곱⁠(tensor product)⁠으로 대상을 나란히 놓는 모노이드 범주는 선형대수와 확률⁠(probability)⁠ 과정까지 같은 그림으로 다룹니다. 이 어휘가 최대공약수⁠(greatest common divisor)⁠와 교집합⁠(intersection)⁠, 벡터 공간의 쌍대, 연쇄법칙⁠(chain rule)⁠, 내림과 올림에서 각각 어떻게 일하는지는 「화살표만으로 본 수학」에서 직접 조작하며 볼 수 있습니다.
• 귀납으로: 수학적 귀납법의 증명은 재귀 함수이고, 증명 보조기는 그 재귀가 끝나는지를 검사해 증명의 타당성을 지킵니다. 무엇이 증명되었는지를 기계가 확인하는 증명 보조기는 4색 정리처럼 사람이 검산하기 어려운 증명을 믿게 해 주는 도구입니다. 4색 문제의 긴 역사는 「일곱 다리의 도시」에 있습니다.
• 학습하는 기계로: 신경망⁠(neural network)⁠을 학습시키는 자동 미분⁠(automatic differentiation)⁠은 프로그램이 계산하는 함수의 도함수⁠(derivative function)⁠를 계산하는 일이라, 프로그램을 수학적 대상으로 다루는 이 글의 관점과 가깝습니다. 2024년 7월 구글 딥마인드는 자사의 AlphaProof가 그해 국제수학올림피아드 여섯 문제 가운데 세 문제를 Lean으로 검사되는 증명으로 풀었다고 발표했습니다. 문제를 Lean의 명제로 옮기는 일은 사람이 했고, 기하⁠(geometry)⁠ 문제 하나는 다른 시스템이 풀었습니다. 언어 모델⁠(language model)⁠이 쓴 증명을 믿을 수 있게 하는 방법의 하나가 바로 기계의 타입 검사입니다. 규모는 곧 커졌습니다. 2024년 10월 영국 임피리얼 칼리지의 케빈 버저드는 페르마의 마지막 정리⁠(Fermat's Last Theorem)⁠의 증명을 사람들이 함께 Lean으로 옮기는 5년짜리 계획을 시작했습니다. 그런데 앤트로픽은 자사의 언어 모델 Claude 에이전트⁠(agent)⁠ 여럿이 2026년 8월 7일부터 11일 동안 그 정리의 증명 전체를 Lean으로 옮겼다고 발표했습니다. 발표에 따르면 와일스와 테일러의 논증을 다몽, 다이아몬드, 테일러가 1995년에 정리한 판을 따랐고, 첫 단계의 환원은 버저드 계획의 설계도를 따랐으며, Lean의 표준 공리 셋 말고는 아무것도 가정하지 않았습니다. 다만 기계가 쓴 1,300만 줄 남짓의 코드는 아직 사람이 읽고 다듬어 mathlib에 들일 수 있는 꼴이 아니고, 이미 있는 증명을 옮긴 것이지 새 수학을 보탠 것은 아닙니다. 기계가 증명을 쓰는 속도⁠(velocity)⁠가 빨라질수록, 9절에서 말한 마지막 믿음, 곧 기계에게 준 명제가 우리가 뜻한 명제와 같다는 것을 사람이 확인하는 일이 더 무거워집니다. 배우는 기계의 수학은 「배우는 기계」에, 다음 낱말을 맞히는 언어 모델이 왜 그럴듯하게 틀리는지는 「다음 단어를 맞히는 기계」에 있습니다.
• 논리로: 불 대수⁠(Boolean algebra)⁠의 참과 거짓은 6절에서 원소가 있는 집합과 없는 집합이 되었습니다. 참인지 거짓인지만 묻는 논리에서, 증명 자체를 대상으로 삼는 논리로 옮겨 간 것이 이 글의 이야기입니다. 토포스⁠(topos)⁠에서는 명제들이 불 대수가 아니라 헤이팅 대수(배중률이 성립하지 않아도 되는, 직관주의 논리의 대수)를 이루어, 내부 논리가 일반적으로 직관주의 논리가 되고, 가정을 딱 한 번씩만 쓰게 하면 '그리고'가 '둘 다 가진다'(⊗)와 '둘 가운데 원하는 쪽을 고를 수 있다'(&)로 갈라지는 선형 논리⁠(linear logic)⁠가 됩니다.
• 대화로: 2절의 BHK 해석은 증명을 '건네는 방법'으로 읽었습니다. 1958년 파울 로렌첸은 한 걸음 더 나가, 명제가 참이라는 것을, 그 명제를 주장하는 사람에게 모든 반박을 이겨 내는 전략이 있다는 뜻으로 읽었습니다. 규칙을 자연스럽게 정하면 이기는 명제가 정확히 직관주의 논리의 정리이고, 앞의 답으로 되돌아가 다시 답하는 것을 허락하면 고전 논리의 정리가 됩니다. 4절의 풀이에서 본 '말을 바꾸는 수법'과 같은 것입니다. 「이기는 쪽이 존재한다」 8절에서 이어집니다.
• 말로: 6절의 람베크는 타입으로 문장의 문법을 계산했고, 5절의 요네다는 프로그래밍 언어 ALGOL을 정의하는 국제 모임에 참여했습니다. 문법을 규칙으로 적는 전통은 파니니에서 촘스키의 위계와 문맥 자유 문법⁠(context-free grammar)⁠까지 이어지고, 프로그램 글을 읽어 구조를 찾는 모든 컴파일러⁠(compiler)⁠가 그 위에 서 있습니다. 「말을 세는 기계」에서 이어집니다.
• 틀린 증명으로: 1절에서 프레게의 체계를 무너뜨린 러셀의 편지, 9절에서 보예보츠키를 증명 보조기로 이끈 15년 묵은 오류는 모두 "무엇이 정확히 틀렸는가"라는 물음이 새 분야를 연 예입니다. 「틀린 증명이 만든 수학」 6절과 8절에 두 이야기가 자세히 있습니다.
• 같은 계산의 다른 얼굴로: 8절의 모노이드, 곧 결합 법칙과 항등원만 요구하는 구조는 최단 경로⁠(shortest path)⁠와 경우의 수와 가장 그럴듯한 해석을 한 알고리즘으로 묶는 반환(모노이드 두 개를 분배법칙⁠(distributive law)⁠으로 엮은 구조)의 바탕이기도 합니다. 타입의 곱과 합이 분배법칙 $A \times (B + C) \cong A \times B + A \times C$를 따르는 것처럼, 그 알고리즘이 성립하는 까닭도 분배법칙 하나입니다. 「같은 계산, 다른 덧셈」에서 이어집니다.