Alonzo Church

Alonzo Church 는 컴퓨터과학 이론의 초석을 세운 대표적인 미국의 수학자, 논리학자중 일인이다. 워싱턴에서 태어난 그는 Princeton 대학에서 Oswald Veblen 의 지도로 박사학위를 받았으며 1929 년에 모교의 수학과 교수가 되었다.

그는 "undecidable problem" 의 존재를 보여준 유명한 1936 년의 논문에서 lambda calculus 를 개발하여 널리 알려졌다. 이러한 결과는 기계적 장치로 해결할 수없는 문제의 존재를 보여준 정지문제 (halting problem) 에 대한 Alan Turing 의 유명한 논문보다도 앞선것이었다. 그와 Turing 은 lambda calculus 와 Turing machine 이 Turing 의 halting problem 에서 동등한 능력을 가진다는 것을 보였으며, 연이어서 다양한 변형 "mechanical processes for computation" 들이 동등한 계산능력을 가진다는 것이 증명되었다. 이러한 것이 Church-Turing thesis 가 된것이다. 처음 그것이 제안되었을때 여러 논쟁이 있었기 때문에 Church's Thesis 와 Turing's Thesis 로 따로 알려졌었다.

Church 는 1967 년까지 모교에 있다가 그후에 California 로 옮겼다. 그의 lambda calculus 는 일반적인 함수형 프로그래밍 언어뿐 아니라 Lisp 계열의 컴퓨터언어의 설계에 영향을 주었다. Church boolean 의 개념은 그의 이름을 기념한 것이다. ............. (Wikipedia : Alonzo Church)

컴퓨터는 세상의 모든 문제를 풀 수 있다고 생각하십니까? 아마도 당장 부정적인 대답이 돌아올 법 합니다. 그렇습니다. 우리가 일상 생활에서 끊임없이 만나는 정서적 문제가 컴퓨터에 의해 해결될 수 있으리라고는 생각되지 않습니다. (설령 먼 미래라고 하더라도 말이죠.)....... 그러면 문제의 정의를 다소 제한해 봅시다. 수학적으로 엄밀히 기술되는 문제들은 예외없이 컴퓨터에 의해 풀 수 있을까요? 질문이 이렇게 되면 앞서의 질문보다는 대답하기가 훨씬 신중해질 것 같습니다......... 답을 말씀드리지요. "풀 수 없습니다!" 이러한 결론이 내려지기까지의 역사를 살펴보는 것이 아마 도움이 될 것입니다.

컴퓨터 능력의 한계에 관한 많은 연구 결과는 20세기초에 수리논리학(mathematical logics) 분야에서 수행된 것입니다. 따라서 우리가 지금 사용하는 컴퓨터의 능력은 컴퓨터가 발명되기 전부터 충분히 예견되고 있었습니다........ 20세기가 시작될 무렵, 수학자 Hilbert는 어떤 수학적인 명제가 입력으로 주어질 때 이의 참과 거짓을 알아내는 알고리즘을 찾고자 하는 일종의 `수학 자동화' 연구를 시작하였습니다. 그후 1931년에 이 방면의 연구에서의 금자탑이라고 할 수 있는 Kurt Godel 의 논문이 발표되었습니다. 즉 그러한 알고리즘은 존재할 수 없음을 증명한 유명한 `불완전성 정리(Incompleteness Theorem)'를 발표한 것입니다. 그의 결과를 간단하게 설명하면, 모든 수학적인 논리 체계에는 그 논리 자체로써는 증명할 수 없는 참인 명제들이 존재한다는 것입니다.

이렇게 일단 풀 수 없는 문제가 존재함이 증명된 후 많은 학자들은 풀 수 있는 문제들에 대한 연구에 몰두하여 여러가지 계산 모델들을 제안하였습니다. 그 예들로는 클레이너(Kleene)가 시작하고 쳐치(Church)가 많이 공헌한 순환함수론(Recursive Function Theory : RFT ), 역시 쳐치의 람다 산술(Lambda Calculus), 포스트(Post)의 포스트 시스템(Post System), 또 마코프(Markov)의 마코프 알고리즘(Markov Algorithm), 그리고 전산학도들에게 가장 친숙한 앨런 튜링(Alan Turing)의 튜링 기계(Turing Machine) 등이 있습니다.

한마디로 하면 이러한 것들은, `풀 수 있는 문제' 혹은 `알고리즘을 만들어 낼 수 있는 문제' 또는 `컴퓨터를 이용하여 풀 수 있는 문제' 의 계산 모델들 중 하나입니다........ 이 제안된 계산 모델들은 풀 수 있는 문제의 범위를 결정하는 목적으로 이용되었습니다. (이런 시도는 대개 1935년을 전후하여 된 것으로, 현대적인 컴퓨터가 발명되기 이전에 이미 사람들은 알고리즘으로 풀 수 있는 문제들에 관심을 기울인 것입니다.)

서로 다르게 정의되어 성능면에서도 차이가 있을 걸로 생각되는 여러가지 모델들이 실제로는 계산 능력면에서 동등함이 밝혀졌으며, 이에 근거하여 이 모델들에 의해서 계산될 수 있는 문제들이 바로 알고리즘을 이용하여 풀 수 있는 문제들과 정확히 일치할 것이라는 가정이 있는데, 이를 `쳐치-튜링 논제(Church-Turing Thesis)'라고 합니다. (이 가정은 아직 증명되지 않고 있지만 옳을거라는 심증이 아주 강하기 때문에 가정(conjecture)이라 하지 않고 논제(thesis)라고 합니다.)...........

Turing Machine이나 RFT나 모두 `해결가능한 문제 부류'를 규정하기 위한 모델들입니다. 그것들의 모형화 능력도 모두 동일하고요. (단지 어느 응용 분야에 보다 편리하게 적용 또는 이용할 수 있느냐의 차이가 있을 뿐입니다.) Turing Machine은 이 문제에 대해 `기계적' 접근을 하고 있고, RFT는 겉모습이 보다 수학적으로 보이는(?) `함수적' 접근을 하고 있지요. 앗! 이렇게 쓰니까 완전히 그 이름의 동어반복일 뿐이군요... .....

약간 더 부연을 하자면, 어떤 입력을 보고 우리가 바라는 결과를 만들어 내는 문제에 대해 그것을 달성하는 `유한 자동장치(Finite Automata; FA)'를 구성해 나갑니다. 점점 더 일반적이고(따라서 어려운) 문제 부류를 제시하고 그것을 해결하는 점점 더 복잡하고 정교한 기계를 만들어 가지요. (전산학과 분들이라면 잘 아시겠지만 Turing Machine은 지금까지 알려진 가장 강력한 FA이지요.) 이렇게 하여 우리가 생각할 수 있는 가장 강력한 FA가 풀 수 있는 문제의 집단이 해결가능한 문제 부류라고 결정하는 것이 `기계적' 접근 방식이고요, 누구나 계산가능하다는 것에 동의하는 기초적인 함수들로부터 출발하여 그 함수들을 조합하여 역시 계산가능한 함수를 만들어내는 방법을 추가하면서 계산가능한 함수들의 범위를 넓혀 나가서 `해결가능한 문제'(= 계산가능한 함수) 부류를 결정하는 것이 `함수적' 접근 방식입니다. Church-Turing Thesis는 이 두 가지 접근 방식으로 결정된 해결가능한 문제의 범위가 `진정으로 알고리즘을 만들 수 있는 문제'의 부류와 동일하다는 것이고요. ........... (Introduction to computer science : 성신여대 김도형)

......... 일반적으로 어떤 현상의 의미를 표현하기 위한 가장 좋은 도구는 수학이다. 수학은 그 현상의 의미를 명확하고 정확하게 표현할 수 있으며, 이를 바탕으로 새로운 현상을 찾을 수 있도록 도와준다. 자연 현상을 설명하는 이론들의 경우, 예로부터 종교적인 방법, 철학적인 방법 등 많은 방법이 연구되어 왔으나 이 중 가장 성공적인 이론은 뉴턴의 운동 법칙과 같은 수학적인 이론들이다. 이 수학적인 이론들은 자연에서 일어나는 많은 현상의 의미를 명쾌하게 설명할 수 있었으며, 심지어는 우리가 전에는 전혀 알 수 없었던 사실들까지 알도록 해 주었다. 현대의 문명도 이러한 수학적인 이론들을 기본으로 하여 발전할 수 있었다.

컴퓨터 소프트웨어의 경우에도 그 의미하는 바를 표현하는 가장 좋은 방법은 수학을 이용하는 방법이다. 소프트웨어가 의미하는 바를 정확하게 집어낼 수 있으려면 그 소프트웨어의 코드가 의미하는 바, 예를 들면 코드가 수행하는 일 등을 명확하게 표현할 수 있어야 한다. 그 표현으로부터 새로운 이론 및 사실을 끌어낼 수 있다면 더 좋을 것이다. 자연 과학에서처럼 이러한 것을 가능하게 하는 것은 바로 수학이다. 컴퓨터 과학에서도 소프트웨어의 의미하는 바를 정확하게 수학적으로 표현하기 위해 많은 모델이 연구되고 있다.

소프트웨어가 의미하는 바를 수학적으로 표현한 모델의 하나로 람다 계산법(Lambda Calculus)이 있다. 어떤 소프트웨어가 하는 일은 무언가를 계산하는 것이라는 관점에서 살펴 볼 수 있다. 람다 계산법은 이 계산이라는 것을 수학적으로 표현한 것이다. 람다 계산법은 현재까지 알려진 직관적으로 계산 가능한 모든 것들을 표현할 수 있으며 따라서 모든 소프트웨어가 계산하는 과정을 이것을 이용하여 표현할 수 있다. 이 람다 계산법을 확장하여 계산이라는 과정 중에서 일어나는 자료의 형이 올바른 것인지를 판단할 수 있도록 타입이라는 개념을 추가한 타입을 갖는 람다 계산법(Typed Lambda Calculus)도 있다.

이 람다 계산법으로 표현된 구조의 의미를 분석할 수 있는 수학적인 도구 중의 하나로는 도메인 이론(Domain theory)이 있다. 람다 계산법으로 표현된 모든 소프트웨어, 그리고 그 소프트웨어가 사용하는 메모리 같은 구조는 어떤 자료 형(Data type)들을 입력으로 받고, 특정한 자료 형을 출력으로 내 놓는다. 따라서 이러한 것들을 입력과 출력에 해당하는 각 자료들 간의 함수로 표현 할 수 있다. 이러한 자료 형들이 각각 어떤 특정한 자료 도메인(Data domain)들에 포함되어 있다고 할 때, 이 프로그램의 도메인을 분석할 수 있도록 하는 것이 도메인 이론이다............ (컴퓨터 소프트웨어의 수학적 의미 : KAIST 배경민)

....... 프로그램 언어의 근간을 이루는 Abstract Syntax와 Semantic Formalism에 대한 연구가 컴퓨터가 개발되기도 전인 아주 오래 전부터 이미 많은 논리학자들에 연구되어왔다는 것이었다. "19세기 로직과 21세기 컴퓨팅“에 관한 에세이를 보면 실제로 이미 19세기에 많은 논리학자들이 프로그램의 이상적인 개념을 Formalized 했었다는 것을 알 수 있다.

Church는 지금으로부터 70년 전인 1932년에 처음으로 Lamda Calculus를 소개했으며, 1936년에는 머신에 의해 계산될 수 있는 모든 함수들을 표현하기 위하여 Lamda Calculus가 이용될 수 있음을 깨닫게 되었다. 또한 이 당시에 Lamda Calculus와는 완전히 독립적으로 Turing은 계산될 수 있는 함수들을 정의하기 위하여 Turing Machine을 발표하였는데, 놀랍게도 계산될 수 있음을 정의하기 위하여 이용된 두 가지의 Formulation이 동등하다는 것을 인식하게 되었다. 그 후 Turing과 Church는 몇 년간 공동으로 연구를 수행했으며, 그 후에 Church와 Turing의 연구 결과를 자세히 파악하고 있었던 John Von Neuman에 의하여 현재 우리가 잘 알고 매일 사용하고 있는 Stored Program Computer의 구조개념이 발표되게 되었다.

특히 Church에 발표된 Lamda Calculus는 후에 프로그래밍 언어의 개발에 심오한 영향을 끼치게 되는데, 함수를 인자로서 또는 함수를 반환 값으로 이용할 수 있다는 개념은 프로그래밍 언어의 설계에 많은 영향을 끼치게 되었다. 1960년대에 이르러서 Christopher Strachey는 ”Functions as First-class Citizen' 이라는 모토아래 Lamda Calculus 개념이 프로그래밍 언어의 설계에 기본이라고 하였고, 실제로 이러한 Lamda Calculus 개념을 반영하여 설계된 언어로서 Iswim, Scheme, ML, Miranda, O'Caml 등을 소개하면서 1940년대에 형성된 Lamda Calculus가 지금까지의 프로그래밍 언어를 이해하고 설계하는데 핵심이 된다고 말하고 있다.

이제야 내가 지금까지 잘못 알고 있었던 사실 한가지를 이해하게 되었다. 컴퓨터가 개발된 이후에 이러한 컴퓨터를 돌리기 위해 프로그래밍 언어가 덜렁 나온 것이 아니라, 19세기부터의 로직 프로그래밍을 거치고 1930년대의 Lamda Calculus 개념과 Turing Machine 그리고 이를 바탕으로 한 현재 우리가 사용하고 있는 컴퓨터의 기본 구조인 Stored Program Computer의 구조가 나타나게 된 사실에 의하여 “아! 컴퓨터가 프로그램을 돌리기 위해 만들어진 것이구나”라는 사실을 인식하게 되었다..........

C언어는 타입이 조금 틀려도 캐스팅을 통하여 프로그램이 문제없이 돌아가게 해주었으나, nML은 그렇지 않았다. 이러한 타입 캐스팅과 같은 프로그래밍 언어의 특징들은 실생활에서 잘못하면 커다란 문제를 야기시킬 수도 있다. 그런데도 C 언어 컴파일러는 “너 잘했어!” 하며 컴파일을 성공시키고 수행을 시키고 나에게 결과를 잘 주어 왔다. 그리고 지금까지 나는 당연히 이게 맞는 것이고 내가 프로그램을 잘 하고 있는 것인지 알았다. 그런데, 이번에 nML로 두 개의 프로그램을 하면서 무언가 이상하다는 것(분명 작고 간단하고 쉽다고 했는데, 오히려 나에게는 프로그램이 더 여려웠음)을 느꼈고, 특히 타입 오류를 계속 수정하며 시간을 보내면서 적어도 타입에 있어서는 내가 지금까지 안전하지 못한 프로그램을 만들어 왔다는 것을 알게 되었다. 그러면 완전하고 안전한 프로그래밍 언어란 무엇이란 말인가? nML은 왜 안전하고 완전한 프로그래밍 언어인가? 이에 대한 답은 읽을거리를 보고 알게 되었다. 앞에서 이야기하였듯이 nML은 Lamda Calculus를 이용하여 Semantic Formalism을 매우 명확하게 정의하고 있었다는 것이다. 하지만, C는 명확한 정의 없이 지금까지 필요에 따라서 계속해서 추가되고 확장되면서 만들어진 언어라는 것을 알게 되었다. 다시 말하면 C언어는 명확한 Semantic Formalism을 가지고 있지 않다는 것을 알게 되었다. 자, 이제 완전하고 안전한 프로그래밍이 무엇인지 어느 정도 이해했지만, 실생활에서 C와 같은 Imperative 언어에 너무 푹 젖어 버린 나에게 당장은 nML을 이용하여 안전한 프로그램을 만드는 일은 쉽지 않은 일인 것을 알고 있다. 지금까지 누구도 이러한 이야기를 한번도 해주지 않았기 때문에 이러한 진실이 숨어 있었다는 사실조차 몰랐었다. 사실 이번 강의 전에 내가 알고 있었던 프로그래밍 언어에 관한 기본 지식은 프로그래밍 언어에는 Imperative와 Applicative의 두 가지 종류가 있으며, 우리들이 잘 쓰는 C, C++, Java 언어 등은 Imperative 언어이며, 잘 쓰지 않는 Prolog나 Lisp 등은 Applicative 언어이며, Imperative 언어는 머신위주의 언어이고 Applicative 언어는 사람 위주의 언어라고 알고 있는 것이 전부였다. 그래서 프로그램 언어를 전혀 모르는 초등학생에게 C와 Prolog을 둘 다 가르치게 되면 사람위주의 언어인 Prolog에 대한 이해가 더 빠르다고 배운게 전부였다. 물론 나의 경우는 이미 Imperative 언어에 빠져 있었으므로 Prolog가 훨씬 적응하기 어려웠었고, 그 당시 내가 알고 있는 대다수의 전산과 친구들 또한 Prolog가 C에 비해 어렵다고 느끼고 있었다. 지금까지 나는 나름대로 컴퓨터가 프로그램을 돌리기 위해서 나온 것이며, 완전하고 안전한 프로그램이 어떠한 것인지 그리고 내가 어떠한 오류에 빠져 있었는지 알게 되었다.

그런데, 읽을거리를 읽으면서 그리고 강의를 들으면서 눈에 거슬리고 귀에 거슬리는 마지막 한 가지 사실이 있었으니 바로 “Proofs are Programs" 이었다. ”어떻게 증명과 프로그램이 같은 것이지?“ 강의 시간에 귀류법으로 증명하는 것을 제외한 증명은 프로그램과 같다는 이야기를 들었지만 도대체 이해를 할 수가 없었다. 읽을거리를 보면 Gentzen의 Natural Deduction을 통해 증명을 위한 Formalism을 소개하고 Church의 Lamda Calculus를 통해 프로그램을 위한 Formalism을 소개하여 증명과 프로그램이 정말로 같다는 내용을 설명하고 있는데, 특히 증명을 단순화시키는 과정이 프로그램을 수행하는 의미를 가진다고 이야기하고 있다. 그러나 나는 지금까지 증명과 프로그램이 같다고는 꿈에도 생각해 본 적이 없었다. 아마도 대부분의 전산학과 학생들이 그렇게 생각하였을 것이다 라고 생각한다. 특히, 나는 고등학교 시절부터 수학에 있어서도 다른 부분에 비하여 증명에 대하여 자신이 없었으며, 증명을 좋아하지도 않았다. 다행스럽게도 대학에 들어왔을 때 프로그래밍은 많이 했지만 증명은 그리 많이 하지 않았기 때문에 몹시 행복해 했었다. 그런데, 내가 수행했던 그 많은 프로그래밍과 증명이 같다니 상상할 수 없는 것이었다. 이번 HW4에서 제시된 하노이 타워 문제를 풀기 위해서도 나는 정반대의 과정으로 문제를 풀었다. 다시 말하면 n개의 고리를 가진 하노이 타워 문제가 해답을 가진다는 것을 우선 증명하게 되면, 그러한 사실을 증명하는 과정이 프로그래밍과 같다는 것을 깨닫는 것이 이번 문제의 목적이었는데 나는 먼저 프로그램이 먼저 머리 속에 떠오르는 것이었다. Move에 대한 프로그램이 다 정의된 다음에 이를 바탕으로 증명을 하게 되었는데, 이는 내가 아직 증명하는 것이 익숙하지 않아서 인지 아니면 프로그램을 생각하면서 머리 속에 떠오르는 것들이 이미 증명 단계를 거치고 있는 것인지 하는 의문이 든다. 끝으로 또 한 가지 궁금한 것은 하노이 타워같이 Recursive 문제를 보면 프로그램과 증명이 같다는 것을 결과를 보면 알 수가 있는 것 같은데, 이외의 다른 모든 문제에 있어서도 증명과 프로그램이 같다는 것에 대해서는 좀 더 심도 있게 생각해 보아야 할 것으로 생각된다.

결론적으로 나는 Lamda Calculus와 Turing Machine 그리고 Von Neuman Machine 과의 관계를 통하여 프로그램과 컴퓨터의 정확한 관계에 대한 이해, Lamda Calculus의 Formalism을 통하여 설계되는 완전하고 안전한 프로그램 언어에 대한 이해 그리고 증명을 위한 Natural Deduction과 프로그램을 위한 Lamda Calculus를 통하여 증명과 프로그램이 같다는 것에 대한 부분적인 이해를 얻었다고 생각한다............ (프로그램과 증명이 같다니? : KAIST 김민수)

Andrew Appel : Turing, Godel, and Church at Princeton in the 1930s : Princeton Academics : 2012/08/24

Turing Centennial Conference : Turing, Church, Godel, Computability, Complexity and Randomization : GoodleTechTalks : Michael Rabin, 2012/04/25