윌리엄 하워드(William Alvin Howard)

윌리엄 하워드는 1926년 캐나다 밴쿠버에서 태어났습니다. 브리티시컬럼비아 대학과 일리노이 대학을 거쳐, 1956년 시카고 대학에서 매클레인의 지도로 박사 학위를 받았습니다. 그의 분야는 증명 이론, 곧 증명 자체를 수학의 대상으로 삼아 그 구조와 힘을 재는 학문입니다. 1930년대 괴델의 불완전성 정리⁠(incompleteness theorem)⁠ 이후 증명 이론가들은 어떤 체계의 증명이 얼마나 강한지, 무모순성⁠(consistency)⁠을 무엇으로 보장할 수 있는지를 캐고 있었습니다. 하워드는 그 한가운데서 일하다가, 논리학과 컴퓨터 과학을 잇는 가장 유명한 관찰 하나를 짧은 원고에 적었습니다.

나이 세 ·

관찰의 출발점은 커리였습니다. 커리는 조합자⁠(combinator)⁠의 타입⁠(type)⁠이 함의 논리의 공리⁠(axiom)⁠와 같은 모양이고, 함수⁠(function)⁠ 적용이 전건 긍정⁠(modus ponens)⁠과 같다는 것을 알아차렸습니다. 하워드는 1969년 원고 「구성의 공식-타입 개념」에서 이것을 논리 전체로 넓혔습니다. '$A$이고 $B$'는 두 값의 쌍의 타입 $A \times B$, '$A$이면 $B$'는 함수의 타입 $A \to B$, '$A$ 또는 $B$'는 둘 중 하나에 꼬리표를 단 값의 타입, 거짓은 값이 하나도 없는 타입에 대응합니다. 그러면 명제의 증명은 그 타입의 값, 곧 프로그램이 됩니다. 예를 들어 '$A$이고 $B$이면 $B$이고 $A$'의 증명은 쌍 $p$를 받아 둘째 성분과 첫째 성분을 바꾸어 담는 함수입니다(위의 식). 증명에서 '$A \wedge B$에서 $B$를 꺼낸다'는 단계가 프로그램에서는 $\pi_2$, 곧 쌍의 둘째 성분을 꺼내는 연산입니다.

여기까지는 증명과 프로그램의 모양이 같다는 이야기입니다. 하워드의 더 깊은 발견은 움직임까지 같다는 것이었습니다. 증명에는 돌아가는 길이 생길 수 있습니다. 먼저 $A$와 $B$에서 '$A \wedge B$'를 만들고, 곧바로 거기서 $A$를 꺼내는 증명은 처음부터 $A$의 증명을 쓰는 것으로 줄일 수 있습니다. 1965년 다그 프라비츠는 이런 돌아가는 길을 모두 없애는 '정규화'를 체계적으로 연구했습니다. 하워드는 이 줄이기가 프로그램에서는 $\pi_1 \langle a, b\rangle \Rightarrow a$라는 계산 한 걸음이고, '$A$를 가정해 $B$를 증명한 뒤 그 가정을 실제 증명으로 채우는' 줄이기는 함수를 인자에 적용해 대입하는 람다 계산의 베타 줄이기와 정확히 같다는 것을 보였습니다. 증명을 정규형⁠(normal form)⁠으로 만드는 일이 프로그램을 끝까지 계산하는 일입니다. 그러니 함의와 '그리고'만 쓰는 직관주의⁠(intuitionism)⁠ 명제 논리⁠(propositional logic)⁠에서 '모든 증명은 정규화된다'는 증명론⁠(proof theory)⁠의 정리는, 단순 타입 람다 계산⁠(simply typed lambda calculus)⁠에서 '타입이 붙은 모든 프로그램은 멈춘다'는 계산의 정리와 같은 말이 됩니다. 하워드는 증명의 절단 제거⁠(cut elimination)⁠와 람다 식의 줄이기 사이의 이 대응을 동료 윌리엄 테이트의 연구에서 시사받았다고 밝혔습니다.

원고는 거기서 멈추지 않았습니다. '모든 $x$에 대해 $P(x)$'와 '어떤 $x$가 있어 $P(x)$'까지 대응시키려면, 타입이 값 $x$에 따라 달라져야 합니다. '$x$를 받아 $P(x)$의 증명을 돌려주는 함수'의 타입은 돌려주는 값의 타입이 받은 값에 달려 있습니다. 하워드는 이런 타입을 도입해 산술의 증명까지 대응을 넓혔고, 이것이 오늘날 의존 타입⁠(dependent type)⁠이라 부르는 생각의 이른 형태입니다. 같은 무렵 네덜란드의 니콜라스 호버르트 더브라위언은 컴퓨터로 수학 증명을 확인하는 언어 오토마트(1967)에서 독립적으로 같은 생각에 이르렀고, 1970년대 스웨덴의 마르틴뢰프가 이것을 하나의 기초⁠(basics)⁠ 이론으로 세웠습니다.

원고는 1969년에 쓰였지만 정식 출판은 11년 뒤였습니다. 그동안 복사본이 연구자들 사이를 돌며 읽혔고, 1980년 커리의 80세를 기리는 논문집 『H. B. 커리에게: 조합 논리⁠(combinatory logic)⁠, 람다 계산, 형식주의⁠(formalism)⁠ 논문집』에 실렸습니다. 1970년대에는 캐나다의 요아힘 람베크가 같은 대응이 범주론⁠(category theory)⁠의 데카르트 닫힌 범주⁠(cartesian closed category)⁠와도 이어진다는 것을 보여, 이 셋의 대응을 '커리–하워드–람베크 대응'이라 부르기도 합니다. 명제는 타입이자 범주⁠(category)⁠의 대상이고, 증명은 프로그램이자 대상 사이의 화살이라는 것입니다.

그의 본업인 증명 이론에서도 이름이 남았습니다. 1968년 논문은 클리퍼드 스펙터가 괴델의 디알렉티카 해석을 해석학(2계 산술)으로 넓히려고 도입한 '바 재귀⁠(recursion)⁠'로, 바 귀납이라는 강한 증명 원리를 해석했습니다. 1972년에는 귀납적 정의의 이론이 얼마나 강한지를 서수로 재는 분석을 했습니다. 그 분석에 나오는 거대한 가산 서수는 오늘날 바흐만–하워드 서수라 불리며, 여러 체계의 증명 강도를 재는 표준 눈금 가운데 하나입니다. 그는 일리노이 대학 시카고 캠퍼스에서 오래 가르쳤고, 2018년 미국 수학회 펠로가 되었으며, 2026년 3월 시카고에서 99세로 세상을 떠났습니다.

이 대응에 대한 흔한 오해 하나를 짚어 둡니다. 대응은 직관주의 논리⁠(intuitionistic logic)⁠에서 가장 깨끗하게 성립합니다. '$A$ 또는 $A$가 아니다'는 고전 논리에서는 늘 참이지만, 그 증명이 프로그램이라면 어느 쪽인지를 실제로 알려 주어야 하는데, 모든 $A$에 대해 그런 프로그램은 없습니다(정지 문제⁠(halting problem)⁠를 생각해 보면 됩니다). 고전 논리까지 대응을 넓히려면 1990년 티머시 그리핀이 보인 것처럼 계산을 되감는 '계속'이라는 더 강한 제어 연산이 필요합니다. 대응은 모든 논리와 모든 언어에 공짜로 성립하는 것이 아니라, 논리와 언어를 맞추어 고를 때 성립합니다.

이어지는 곳. 증명을 프로그램으로 읽는 대응 전체는 커리–하워드 대응에서, 그 대응이 가장 깨끗하게 성립하는 논리는 직관주의 논리에서 직접 따라가 볼 수 있습니다. 증명을 줄이는 일과 같은 계산은 람다 계산과 단순 타입 람다 계산에, 쌍과 꼬리표 붙은 값의 타입은 대수적 자료형⁠(algebraic data type)⁠에 있습니다. 값에 따라 달라지는 타입은 의존 타입과 마르틴뢰프로, 같은 대응의 범주론 쪽 얼굴은 데카르트 닫힌 범주로, 이 모든 것을 실제로 쓰는 도구는 증명 보조기⁠(proof assistant)⁠로 이어집니다.

관계.

• 스승 손더스 매클레인 — 1956년 시카고 대학에서 매클레인의 지도로 재귀와 정렬 순서에 관한 논문 「k겹 재귀와 정렬 순서」를 써서 박사 학위를 받았습니다.
• 영향을 받음 해스켈 커리 — 커리와 페이스의 『조합 논리』가 적은 '조합자의 타입 = 공리'라는 관찰에서 출발해, 증명의 간단히 하기와 계산의 대응까지 넓혔습니다.
• 영향을 받음 쿠르트 괴델 — 그의 바 재귀 연구는 괴델이 1958년 산술의 무모순성을 고차 함수의 계산으로 해석한 '디알렉티카 해석'과 그 확장을 잇는 작업이었습니다.
• 영향을 줌 페르 마르틴뢰프 — 1969년 원고가 술어 논리⁠(predicate logic)⁠까지 대응을 넓히며 도입한 의존 타입의 생각은 마르틴뢰프의 직관주의 타입 이론⁠(type theory)⁠에 이어졌습니다.

연표.

• 1956년 시카고 대학에서 매클레인의 지도로 박사 학위를 받다
• 1968년 바 재귀로 바 귀납을 해석하는 논문을 내다
• 1969년 원고 「구성의 공식-타입 개념」을 써서 복사본으로 돌리다
• 1972년 뒤에 바흐만–하워드 서수라 불리는 수를 쓴 서수 분석을 발표하다
• 1980년 1969년 원고가 커리 기념 논문집에 정식으로 실리다
• 2018년 미국 수학회 펠로가 되다