알론조 처치
Alonzo Church
생애
“알고리즘으로 계산할 수 있다”는 일상어를 여러 형식 체계가 만나는 수학적 질문으로 바꾼 논리학자. 처치는 1930년대 초 람다 표기와 함수의 치환·축약만으로 계산을 표현하는 람다 계산을 발전시켰다. 1936년 람다 정의 가능성으로 결정 문제의 부정적 해답을 제시했고, 튜링은 독립적으로 추상 기계 모형을 제시했다. 두 모형과 일반재귀함수 등이 같은 계산 가능한 함수 부류를 준다는 것은 수학적 동치 정리다. 반면 ‘직관적으로 효과적인 모든 절차가 이 부류에 들어간다’는 교회–튜링 명제는 물리 법칙에서 증명되는 정리가 아니라 경험과 형식화가 뒷받침하는 논제다. 튜링 기계 역시 실제 장치가 아니라 종이·기호·상태로 계산을 모델링한 추상 수학이다. 람다 계산은 이후 함수형 프로그래밍과 언어 의미론에 큰 영향을 주었고, 처치는 학술지 편집과 클레이니·로서·튜링 등 제자 지도를 통해 논리학 공동체를 키웠다.
결정적 순간
람다 계산 도입 — Set of Postulates for the Foundation of Logic
프린스턴1932~1933년 논문에서 λ-추상과 적용을 포함한 형식 체계를 제시했다. 전체 논리 체계는 모순 문제를 겪었지만 함수 계산 부분은 독립적으로 발전해 오늘날의 무타입 람다 계산이 됐다.
Church's theorem — Hilbert 결정 문제의 부정 해답
프린스턴람다 정의 가능성과 재귀함수의 관점에서 일반적인 결정 절차가 존재하지 않음을 보였다. 튜링은 독립적인 기계 모형으로 같은 부정적 결론에 도달했고, 형식 모형들의 동치가 이어서 확립됐다.
Journal of Symbolic Logic 창간 — 43년 편집
프린스턴1936년 Journal of Symbolic Logic 창간, 1979년까지 43년간 편집. 수리논리학·기초론의 세계 표준 학술지. 튜링·괴델·콰인·크리스의 주요 논문이 모두 여기에 게재. 처치 이후 편집장 Anil Nerode·Sol Feferman으로 계승.
Turing의 박사 지도교수 — Princeton 1936-1938
프린스턴튜링은 자신의 계산 가능성 논문을 완성한 뒤 프린스턴에 와 처치의 지도 아래 1938년 《순서수에 기초한 논리 체계》로 박사학위를 받았다. 독립 연구 뒤에 사제 관계가 형성됐다는 순서가 중요하다.
이 사람이 없었다면
아래 내용은 확인된 역사적 사실이 아니라, 이 인물의 영향을 생각해 보는 가정입니다.
초보자는 λx.x+1에 3을 넣어 치환한다. 중급에서는 α-변환과 β-축약으로 작은 프로그램을 계산한다. 고급에서는 람다 계산·튜링 기계·일반재귀함수 사이 번역을 만들고, 전문 단계에서는 계산 가능성의 동치 정리와 교회–튜링 명제, 결정 불가능성·타입 이론·프로그램 의미론의 경계를 구분한다.
