알론조 처치(Alonzo Church)

알론조 처치는 1903년 미국 워싱턴 D.C.에서 태어났고, 평생을 거의 한 대학에서 보냈습니다. 1920년대 그가 공부한 프린스턴은 오즈월드 베블런이 이끌며 미국 수학의 중심으로 막 떠오르던 곳이었습니다. 그 무렵 수학의 가장 큰 물음은 대서양 건너 괴팅겐에서 나왔습니다. 힐베르트는 수학 전체를 몇 개의 공리⁠(axiom)⁠와 기계적인 추론 규칙으로 적고, 그 체계가 모순이 없음을 증명하려 했습니다. 1928년 그는 여기에 결정 문제를 더했습니다. 어떤 논리식이 주어지든 그것이 참인지 아닌지를 유한한 단계 안에 기계적으로 판정하는 방법이 있는가? 문제는 '기계적인 방법'이 무엇인지 아무도 정확히 정의한 적이 없다는 것이었습니다. 처치는 이 정의를 처음 내놓은 사람 가운데 하나이고, 그 정의로 힐베르트의 물음에 '없다'고 처음 답한 사람입니다.

나이 세 ·

그는 1924년 프린스턴을 졸업하고 1927년 베블런의 지도로 박사 학위를 받았습니다. 논문은 체르멜로의 선택공리⁠(axiom of choice)⁠를 다른 가정으로 바꾸면 어떻게 되는지를 다룬 것이었습니다. 이어 국가 연구 장학생으로 하버드에서 1년, 괴팅겐과 암스테르담에서 1년을 보냈는데, 괴팅겐은 힐베르트의 형식주의⁠(formalism)⁠가, 암스테르담은 브라우어르의 직관주의⁠(intuitionism)⁠가 자리한 곳이었습니다(수학 기초론 논쟁⁠(debate on the foundations of mathematics)⁠). 1929년 프린스턴에 돌아와 교수진이 된 그는 1967년까지 그곳에 머물렀습니다. 1930년 프린스턴에 고등연구소가 세워지고 유럽의 수학자들이 몰려들면서, 대학과 연구소를 합친 이 작은 도시는 논리학의 교차로가 되었습니다(프린스턴 고등연구소).

1930년대 초 그는 집합⁠(set)⁠ 대신 함수를 바탕으로 논리를 세우려 했고, 그 도구로 람다 계산을 만들었습니다. 규칙은 두 가지뿐입니다. 하나는 함수를 만드는 것입니다. $\lambda x.\, x + 1$은 '$x$를 받아 $x + 1$을 돌려주는 함수'를 뜻하고, 이름을 붙이지 않아도 됩니다. 다른 하나는 함수를 적용하는 것입니다. $(\lambda x.\, x + 1)\,3$은 몸통의 $x$ 자리에 3을 넣어 $3 + 1$이 됩니다. 이 대입 한 가지가 위의 식의 β-축약⁠(β-reduction)⁠이고, 계산은 이것을 더 줄일 것이 없을 때까지 되풀이하는 일입니다. 눈여겨볼 점은 수조차 함수로 적을 수 있다는 것입니다. 처치는 2를 '어떤 함수 $f$를 받아 두 번 적용하는 함수' $\lambda f.\,\lambda x.\, f(f\,x)$로 정의했습니다. 그러면 3은 세 번 적용하는 함수이고, 덧셈과 곱셈, 참과 거짓, 조건문까지 모두 이런 함수로 만들어집니다. 함수를 값처럼 주고받는다는 이 생각이 오늘날 프로그래밍 언어의 '람다'입니다.

처음의 계획은 절반만 살아남았습니다. 1935년 그의 두 제자 스티븐 클리니와 바클리 로서가 처치의 논리 체계 전체에서 러셀의 역설⁠(Russell's paradox)⁠과 비슷한 방법으로 모순을 끌어냈습니다. 처치는 논리 부분을 버리고 계산 부분, 곧 순수한 람다 계산만 남겼습니다. 1936년 그와 로서는 이 계산이 믿을 만하다는 핵심 정리를 증명했습니다. 식을 줄이는 순서는 여러 가지일 수 있습니다. $(\lambda x.\, x \times x)(2 + 3)$에서 괄호 안을 먼저 계산하면 $5 \times 5$, 먼저 대입하면 $(2+3) \times (2+3)$이 되지만 끝은 같은 25입니다. 처치–로서 정리⁠(Church–Rosser theorem)⁠는 이것이 언제나 성립한다는 것, 곧 어떤 순서로 줄이든 더 줄일 수 없는 끝(정규형⁠, normal form⁠)에 이른다면 그 끝은 하나뿐이라는 것입니다. 끝에 이르지 못하는 식도 있습니다. $(\lambda x.\, x\,x)(\lambda x.\, x\,x)$는 한 번 줄이면 자기 자신으로 돌아와 끝없이 이어집니다. 이 자기 적용의 기법을 조금 바꾸면, 자기 자신을 부르는 재귀⁠(recursion)⁠와 고정점⁠(fixed point)⁠을 람다 계산 안에서 만들 수 있습니다.

이제 처치는 대담한 제안을 했습니다. 클리니가 알려진 계산 가능한 함수를 하나하나 람다로 적어 내자, 처치는 1935년 봄 '실질적으로 계산할 수 있는 함수'란 곧 람다로 정의할 수 있는 함수라고 정의하자고 발표했습니다. 괴델이 1934년 프린스턴 강의에서 다룬 재귀 함수⁠(recursive function)⁠도 같은 범위라는 것이 곧 밝혀졌습니다. 이것이 오늘날 처치–튜링 논제⁠(Church–Turing thesis)⁠라 불리는 주장의 처치 쪽 절반입니다. 증명할 수 있는 정리가 아니라 '계산'이라는 막연한 말에 정확한 뜻을 주자는 제안이며, 괴델은 처음에 이 제안을 믿지 않았습니다. 정의가 생기자 불가능성을 증명할 수 있게 되었습니다. 1936년 처치는 두 람다 식이 같은 정규형을 갖는지를 판정하는 람다 식은 있을 수 없음을 보였고, 이어 짧은 논문에서 결정 문제에도 같은 부정의 답을 냈습니다. '판정할 수 없다'는 말은 어떤 특정한 식을 풀 수 없다는 뜻이 아닙니다. 모든 입력에 대해 유한한 시간 안에 옳은 답을 내는 하나의 방법이 없다는 뜻입니다.

몇 주 뒤 케임브리지의 스물세 살 앨런 튜링이 같은 결론에 이른 원고를 스승 맥스 뉴먼에게 내밀었습니다. 튜링은 종이 테이프 위의 기호를 읽고 쓰는 가상의 기계로 계산을 정의했는데, 처치의 논문이 먼저 나왔다는 것을 안 뉴먼은 1936년 5월 처치에게 편지를 보내 이 젊은이가 프린스턴에서 공부할 수 있게 해 달라고 부탁했습니다. 튜링은 그해 가을 프린스턴에 왔고, 자기 기계로 계산할 수 있는 함수와 람다로 정의할 수 있는 함수가 정확히 같다는 증명을 논문의 부록으로 붙였습니다. 처치는 1937년 서평에서 튜링의 분석이 계산이라는 말과 이 정의를 곧바로 같다고 느끼게 해 준다고 평하며 '튜링 기계⁠(Turing machine)⁠'라는 이름을 처음 썼습니다. 괴델이 논제를 받아들인 것도 튜링의 기계를 보고 나서였습니다. 튜링은 1938년 처치의 지도로 서수⁠(ordinal)⁠로 논리 체계를 쌓는 논문을 써서 박사 학위를 받고 영국으로 돌아갔습니다(튜링 기계, 정지 문제⁠(halting problem)⁠).

처치는 논리학이라는 분야 자체를 세우는 일에도 힘썼습니다. 1936년 기호 논리학회와 『기호 논리학회지』가 창간되었고, 그는 1979년까지 이 학회지의 서평란을 편집하며 세계에서 나오는 논리학 논문을 거의 빠짐없이 읽고 정리했습니다. 이 서평란과 그가 모은 논리학 문헌 목록은 흩어져 있던 분야를 하나로 묶었습니다. 1940년에는 단순 타입 이론⁠(type theory)⁠을 발표했습니다. 람다 식마다 '수', '수에서 수로 가는 함수' 같은 타입⁠(type)⁠을 붙이고, 타입이 맞지 않는 적용을 금지하는 체계입니다. 그러면 함수가 자기 자신에게 적용되는 $f\,f$ 같은 식이 만들어지지 않아, 러셀이 타입으로 역설을 막으려던 생각이 훨씬 간결한 모양이 됩니다. 이 체계는 오늘날 HOL과 Isabelle 같은 증명 보조기⁠(proof assistant)⁠의 논리로 쓰입니다. 1956년의 교과서 『수리 논리학⁠(mathematical logic)⁠ 입문』은 꼼꼼함으로 이름났습니다.

그는 뛰어난 스승이었습니다. 그의 박사 제자 가운데에는 클리니와 로서, 튜링 말고도 완전성 정리⁠(completeness theorem)⁠의 새 증명을 낸 레온 헹킨, 힐베르트의 열째 문제를 푸는 데 핵심 역할을 한 마틴 데이비스, 계산 가능성⁠(computability)⁠ 이론의 로저스(Hartley Rogers), 논리 퍼즐로 이름난 레이먼드 스멀리언이 있습니다. 마이클 라빈과 데이나 스콧은 1959년 논문에서 유한 오토마톤⁠(finite automaton)⁠에 여러 갈래로 동시에 나아가는 비결정성을 도입해 1976년 튜링상⁠(Turing Award)⁠을 받았습니다. 스콧은 1969년 무렵, 모든 것이 함수이고 함수가 자기 자신에게도 적용될 수 있는 람다 계산에 수학적인 모형을 처음 찾아 주었습니다(영역 이론⁠(domain theory)⁠). 처치 자신도 1957년 명세로부터 회로를 자동으로 합성하는 문제를 내놓아, 오늘날 반응형 시스템 합성이라 불리는 분야의 출발점이 되었습니다. 그는 1967년 UCLA로 옮겨 여든일곱 살인 1990년까지 가르쳤고, 1995년 오하이오에서 세상을 떠났습니다.

람다 계산은 그가 상상한 것보다 훨씬 멀리 갔습니다. 1958년 존 매카시는 인공지능⁠(artificial intelligence)⁠ 연구를 위한 언어 LISP를 만들며 함수를 적는 방법으로 처치의 람다 표기를 빌렸습니다. 매카시는 뒤에 처치의 책에서 그 부분 말고는 잘 이해하지 못했다고 털어놓았습니다. 그 뒤 로빈 밀너의 ML과 하스켈 같은 함수형 언어⁠(functional programming language)⁠는 람다 계산을 거의 그대로 뼈대로 삼았고, 파이썬의 lambda, 자바스크립트의 화살표 함수처럼 오늘날 대부분의 언어가 이름 없는 함수를 씁니다. 타입이 붙은 람다 계산에서는 '타입은 명제이고 프로그램은 그 증명'이라는 커리–하워드 대응⁠(Curry–Howard correspondence)⁠이 드러났고, 이것이 수학의 증명을 컴퓨터로 확인하는 증명 보조기의 바탕이 되었습니다. 결정 문제의 부정적인 답이 계산할 수 없는 것의 목록을 열었다면, 람다 계산은 계산할 수 있는 것을 적는 가장 작은 언어가 된 셈입니다.

이어지는 곳. 그의 계산 모형은 람다 계산에서, 튜링 기계와의 만남은 처치–튜링 논제와 튜링 기계에서 이어집니다. 판정할 수 없는 문제의 대표는 정지 문제이고, 그 증명의 모양은 자기 참조⁠(self-reference)⁠와 대각선에서 러셀의 역설, 불완전성 정리⁠(incompleteness theorem)⁠와 한 줄로 이어집니다. 그가 일한 곳은 프린스턴이고, 제자들이 연 오토마톤⁠(automaton)⁠ 이론은 유한 오토마톤과 정규 표현식⁠(regular expression)⁠에 있습니다.

관계.

• 제자 앨런 튜링 — 1936년 튜링의 논문이 도착하자 뉴먼의 부탁으로 그를 프린스턴에 받아들였고, 1937년 서평에서 '튜링 기계'라는 이름을 처음 썼으며, 1938년 그의 박사 논문을 지도했습니다.
• 영향을 받음 다비트 힐베르트 — 힐베르트가 1928년 수리 논리학의 중심 문제로 내건 결정 문제에 1936년 처음으로 부정의 답을 냈습니다.
• 영향을 받음 쿠르트 괴델 — 괴델이 1934년 프린스턴에서 강의한 재귀 함수를 자기 논제의 근거로 삼았는데, 괴델은 처음에 그 논제를 탐탁지 않게 여기다가 튜링의 분석을 보고 받아들였습니다.
• 영향을 받음 버트런드 러셀 — 1940년의 단순 타입 이론은 러셀의 타입 이론을 람다 계산 위에서 간결하게 다시 세운 것입니다.
• 영향을 줌 존 매카시 — 매카시는 1958년 리스프를 설계하며 이름 없는 함수를 적는 방법으로 처치의 람다 표기를 빌렸습니다.
• 영향을 줌 로빈 밀너 — 밀너의 언어 ML은 타입이 붙은 람다 계산을 뼈대로 삼고, 여기에 다형성⁠(polymorphism)⁠과 타입 추론⁠(type inference)⁠을 더했습니다.

연표.

• 1924년 프린스턴 대학을 졸업하다
• 1927년 베블런 밑에서 선택공리에 관한 논문으로 박사 학위를 받다
• 1928년 괴팅겐과 암스테르담에서 연구하다
• 1929년 프린스턴 대학 수학과의 교수진이 되다
• 1932년 람다 계산을 담은 논리 체계를 발표하다
• 1936년 결정 문제가 풀릴 수 없음을 증명하고 『기호 논리학회지』를 창간하다
• 1938년 튜링이 그의 지도로 박사 학위를 받다
• 1940년 단순 타입 이론을 발표하다
• 1956년 『수리 논리학 입문』을 펴내다
• 1967년 UCLA로 옮기다