알론조 처치: 컴퓨터 지능의 잊힌 설계자

• Alonzo Church는 Alan Turing만큼 대중적으로 알려지지 않았지만, λ-calculus와 계산 가능성 이론으로 컴퓨팅의 논리적 기반을 세운 논리학자임
• 1936년의 Church-Turing thesis는 효과적으로 계산 가능한 함수가 Turing machine 또는 그와 동등한 체계로 계산될 수 있다는 틀을 제공함
• Hilbert의 Entscheidungsproblem에 대해 모든 수학 명제를 판정하는 결정적 알고리듬은 없다는 답을 내놓으며, 계산의 한계를 명확히 함
• Princeton에서 Stephen Kleene, J. Barkley Rosser, Alan Turing 등을 지도했고, Turing은 Church의 지도 아래 Ph.D.를 마침
• 그의 추상적 작업은 현대 컴파일러, 인터프리터, 함수형 프로그래밍, 스마트폰 앱과 AI까지 이어지는 계산의 계보에 남아 있음

---

대중적 명성보다 큰 이론적 영향

• Alan Turing은 Turing Test로 컴퓨팅과 인공지능의 대중적 역사에서 더 자주 언급되지만, Church는 Turing의 사고와 작업에 큰 영향을 준 인물임
• 계산이 무엇인지 이해하고 AI를 평가하는 개념을 형성하는 데 Church의 작업이 중요한 기반이 됨
• Church의 기여가 없었다면 인공지능과 그 평가 방식에 대한 현재의 개념도 상당히 달라졌을 수 있음

생애와 학문적 성향

• Church는 1903년 6월 14일 Washington, D.C.에서 태어난 조용하고 말수가 적은 논리학자였음
• 어린 시절 공기총 사고로 한쪽 눈을 실명했거나 부분적으로 시력을 잃었다는 기록이 있음
• 1920년 Connecticut의 preparatory school을 마친 뒤 같은 해 Princeton에서 대학 교육을 시작했고, 1927년에 박사 과정을 마침
• Harvard, Göttingen, Amsterdam에서 National Research Fellow로 시간을 보낸 뒤 Princeton으로 돌아와 학문적 업적의 많은 부분을 쌓음
• 정갈한 칠판 글씨와 꼼꼼한 성격으로 알려졌으며, 중요한 논문을 보존하려고 Duco cement로 덮기도 했음

λ-calculus와 계산 가능성

• Church의 가장 깊은 기여는 컴퓨터과학이라는 이름이 생기기 전 그 토대가 된 λ-calculus임
• 1936년 Church는 이론 컴퓨터과학의 핵심 개념인 Church-Turing thesis를 정식화함
  • 효과적으로 계산 가능한 함수는 Turing machine 또는 그와 동등한 체계로 계산될 수 있다는 내용임
  • 기계가 이론적으로 무엇을 할 수 있는지 이해하는 틀을 제공함
  • 알고리듬적 절차가 닿을 수 있는 경계도 함께 드러냄
• 이 명제는 기반적 개념이지만, ‘effective computability’의 해석과 물리적 계산, 인간 지능의 본질을 둘러싼 논의와 한계도 남아 있음
• Turing이 기계적 절차를 논리적 형태로 옮기는 Turing machine을 제안했다면, Church는 그런 기계를 이론적으로 뒷받침하는 순수 추상화를 제공함

현대 프로그래밍과 함수형 사고

• λ-calculus의 영향은 오늘날 프로그램 작성 원리에서도 보이며, 합성, 고차 함수, 불변성을 강조하는 방식과 연결됨
• 이 형식 체계는 추상적 수학 문제를 코드화하고 기계적으로 해결할 수 있게 했으며, 현대 컴파일러와 인터프리터 아키텍처의 기반이 됨
• 현대 프로그래머에게 λ-calculus는 Lisp, Haskell, Python이나 JavaScript의 일부 패러다임에서 볼 수 있는 중첩 함수 집합처럼 보일 수 있음
• λ-calculus의 추상화는 함수를 first-class citizen으로 다루는 함수형 프로그래밍의 기초가 됨

Entscheidungsproblem과 계산의 한계

• Church는 논리와 철학의 다른 영역에도 중요한 기여를 했고, 대표적 사례가 Entscheidungsproblem에 대한 작업임
• Entscheidungsproblem은 David Hilbert가 1928년에 제기한 결정 문제로, 어떤 수학 명제의 참 여부도 판정할 수 있는 결정적 알고리듬이 존재하는지를 물었음
• Church는 그런 알고리듬이 존재하지 않는다는 부정적 답을 내놓았고, 이 결과는 Church's Theorem으로 알려짐
• 이 발견은 결정 이론에 깊은 영향을 줬으며, 계산만으로 달성할 수 있는 것의 한계를 강조함

Princeton의 지적 중심과 제자들

• Church는 당대의 중요한 논리학자와 컴퓨터과학자들을 지도한 멘토였음
• 그의 학문적 계보에는 Stephen Kleene, J. Barkley Rosser, Alan Turing이 포함됨
• Turing은 Princeton에서 Church의 지도 아래 Ph.D.를 마침
• David Kaplan은 새 대학원생들에게 Church의 수업을 들어보라고 권하며, 관심 분야가 아니더라도 손자들에게 이야기하게 될 경험이라고 말했다고 전해짐
• 1930년대 Princeton은 John von Neumann, Kurt Gödel, Church가 함께한 현대 논리 발전의 지적 중심지였음

잘 보이지 않는 유산

• Church는 Turing, von Neumann, Gödel 등에 비해 같은 수준의 대중적 명성을 얻지 못함
• 그의 유산은 전시 암호 해독의 영웅담이나 이른 죽음의 비극처럼 대중적 상상력을 끌기 쉬운 형태가 아니었음
• 스마트폰에서 실행되는 수십억 개의 프로그램은 그 논리를 λ-calculus의 추상 함수까지 거슬러 올라갈 수 있음
• 단순한 앱부터 인공지능까지, 계산의 보이지 않는 DNA는 Church의 작업에서 중요한 계보를 이어받음
• Church의 천재성은 스펙터클이 아니라 세계를 바꾸는 엄밀한 구조와 조용한 우아함 속에 있었음

[GN⁺]

Hacker News 의견들

• Paradigms of Artificial Intelligence Programming(PDF/EPUB: https://github.com/norvig/paip-lisp)에 나온 lambda 이름의 유래가 좋았음
  Alonzo Church가 Russell과 Whitehead의 Principia Mathematica 표기에서 묶인 변수 위에 쓰던 캐럿 x̂(x + x)를 1차원 문자열로 만들려고 ^x(x + x)처럼 앞으로 옮겼고, 비어 있는 캐럿이 어색해 대문자 람다 Λx(x + x)로 바꿨다가 혼동을 피하려고 소문자 λx(x + x)가 됐다는 이야기임
  John McCarthy가 Princeton에서 Church의 학생이었고, 1958년 Lisp를 만들 때 당시 키펀치에 그리스 문자가 없어 (lambda (x) (+ x x))를 썼고 지금까지 남았다는 내용임
  그래서 이 글의 주제처럼 Church는 Lisp 회고에서 자주 등장하며, 컴퓨팅 역사에 관심이 거의 없는 사람들에게나 “잊힌” 인물일 수 있음

  • 그 유래가 난해한 기호 이상의 의미를 갖길 바랐지만, 실제로는 아닌 듯함
    Dana Scott에 따르면 Church 본인은 그 선택을 “eeny, meeny, miny, moe”식의 임의 선택이라고 했고, Barendregt식 설명도 최근 University of Birmingham 강연에서 반박했다고 함
    프랑스어권에서는 “personne lambda”가 보통 사람·익명인을 뜻해서 익명 함수와 잘 맞아 보이고, 형용사 lambda도 “일반적/평범한”이라는 뜻이라 그리스 알파벳 중간쯤의 글자가 평균적인 것을 나타낸다는 느낌은 있음
    https://math.stackexchange.com/questions/64468/why-is-lambda...
  • “Lisp는 보통 표현적인 이름을 선호한다”지만, lambda 말고도 car/cdr은 그리스 문자는 아니어도 전혀 투명한 이름은 아님
  • PAIP는 인공지능 주제 자체는 세월이 꽤 탔지만, 전체적으로는 훌륭한 책임
    프로그래밍의 여러 주제를 다루고, 함수형 프로그래밍에 노출이 적었던 사람에게는 낯설 수 있는 패러다임도 열어 줌
  • Alonzo Church의 람다 표기 기원에 대한 이 반복되는 이야기가 사실인지는 분명하지 않음
    Church가 특정 의미보다 그리스 문자 중 임의 선택에 가까웠다고 암시한 다른 사례는 https://en.wikipedia.org/wiki/Lambda_calculus#Origin_of_the_...에 있음
  • lambda calculus라는 용어를 처음 만든 사람이 누구였는지 궁금함
    McCarthy가 Lisp를 시작하기 전인지 후인지도 궁금함

• “Church의 람다 계산법과 Turing 기계는 동등한 계산 능력을 갖지만, Turing 기계는 가변 상태를 쓴다는 점이 다르다. 오늘날까지도 함수형 언어와 명령형 언어 사이에 균열이 있는 것은 Church와 state의 분리 때문이다”
  이 인용문은 오래전부터 알고 있었지만 원 출처를 못 찾겠음
  편집: Guy Steele의 “언어의 함수형·람다 계산 부분과 부작용을 일으키는 부분을 섞지 않으려는 사람들이 있다. 그들은 Church와 state의 분리를 믿는 듯하다”에서 온 것일 수도 있음

  • Guy의 그 인용은 2001 Lightweight Languages Workshop에서 이어진 MIT 메일링 리스트에서 나온 것임
    원문 아카이브는 여기 있음: https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/...
  • Niklaus Wirth 이름 농담도 떠오름
    유럽인은 대체로 그의 이름을 제대로 “Nick-louse Veert”라고 발음하지만, 미국인은 “Nickel's Worth”로 망친다는 농담임
    즉 유럽인은 이름으로 부르고, 미국인은 가치로 부른다는 말임
    https://en.m.wikiquote.org/wiki/Niklaus_Wirth
  • Peter Norvig 쪽에서 나온 것 같음. 형제 댓글을 보면 됨

• Church에 관한 정말 놀라운 글을 읽고 싶다면 Rota의 회고를 추천함
  https://www34.homepage.villanova.edu/robert.jantzen/princeto...의 첫 번째 절임
  관련 링크로는 Alonzo Church, 92, Theorist of the Limits of Mathematics(1995) - https://news.ycombinator.com/item?id=12240815 - 2016년 8월, Gian-Carlo Rota on Alonzo Church (2008) - https://news.ycombinator.com/item?id=9073466 - 2015년 2월이 있음

  • Rota의 회고는 Church 부분뿐 아니라 전체 웹페이지, 즉 “Fine Hall in its golden age: Remembrances of Princeton in the early fifties” 전체가 그의 책 Indiscrete Thoughts의 한 장임
    책 전체가 읽을 만함

• 그의 이름을 딴 Alonzo 프로그래밍 언어는 거의 잊혔음
  https://dl.acm.org/doi/pdf/10.1145/68127.68139

• 특히 Frege와 Russell의 작업을 잇는 논리 철학과 의미/지시 이론은 대부분 잊혔음
  Church가 이 주제로 논문을 많이 냈지만 Wikipedia 같은 곳에서는 거의 다뤄지지 않음
  그래도 Stanford Encyclopedia of Philosophy 항목은 좀 낫다: https://plato.stanford.edu/entries/church/
  다만 그것도 그의 주요 작업 일부를 놓친다고 들었고, 수학자에게는 너무 철학적이고 철학자에게는 너무 기술적이었을 것 같음

  • 관련해서 E.J. Lemmon은 Beginning Logic에서 중요한 논리학 책들을 꼽으며 Church의 Introduction to Mathematical Logic 0장이 모든 철학자에게 여러 번 읽힐 만하다고 썼음

• 핵심 논점은 아니지만, 블로그 글에 AI 생성 삽화를 쓰는 건 좀 자제했으면 함
  Church의 실제 사진은 퍼블릭 도메인에도 있는데, 이 삽화는 그와 딱히 닮지도 않았고 글이 인기를 얻으면서 이미 이미지 검색 결과에 나타나고 있음
  5분 넘게 생성할 가치도 없을 정도의 삽화라면 그냥 빼는 편이 낫지 않을까 싶음
  그래도 꼭 “AI” 생성 이미지를 써야 한다면 최소한 그렇게 캡션을 달아야 함

  • 지적 고맙고 미안함
    온라인 사진을 가져오는 게 내키지 않았고, 이 이미지는 ‘가짜’ 닮은꼴이 되지 않게 하려고 7번째로 만든 결과였으며 어느 정도 닮았다고 느꼈음
    JvN 이미지는 꽤 잘 만들었지만, 앞으로는 인물처럼 보이는 가짜 닮은꼴 대신 상징 이미지를 쓰는 편이 맞겠음

• “컴퓨터 지능의 설계자”라는 표현은 과한 듯함
  Church가 뛰어난 논리학자였던 건 맞지만, 여기서 컴퓨터 지능이 AI/ML을 뜻한다면 그의 기여는 사실상 없음
  별개로 람다 계산법이 진짜 수학인지도 잘 모르겠고, 영리한 표기법에 더 가까워 보임
  표기법의 장점은 주관적이며, Church가 자기 아이디어가 특정 프로그래밍 언어 설계에 영감을 준 데 별 관심이 없었다는 점도 흥미로움

  • “Lambda calculus”는 때때로 단순 형식 람다 계산법을 뜻하며, 이는 단순 형식 이론(STT), 즉 “Church의 형식 이론”을 가리키는 데 주로 쓰임
    STT는 고차 논리와도 자주 동일시되는데, 기본 “개체”와 진리값 T/F라는 두 원시 형식, 그리고 함수 형식 (a --> b)만으로 임의의 논리적 대상을 표현할 수 있기 때문임
    STT는 분명 Church의 발명이고, 현대 형식 이론들에 큰 영향을 줬으며, Haskell 같은 복잡한 형식 체계를 가진 프로그래밍 언어에도 영향을 줬음

• 완전히 논증할 수는 없지만, 직감상 Turing과 그가 상징하는 것은 AI 쪽에서 결국 높이 평가되는 반면 Church는 반대처럼 보임
  전자는 순수성, 가능한 최소 조건, 추상적이고 “순수한” 계산에서 출발했고, 후자는 우리가 실제로 어떻게 사고할 수 있는지에 관심이 있었으며 구현보다 표현과 추상화의 확장에 더 신경 쓴 듯함

  • 한 관점으로 보면 Turing은 전쟁 중 실용 컴퓨터를 만들었지만, 이후 자기 정부에 의해 컴퓨터를 계속 만들지 못하게 되어 이론으로 물러나야 했음
    Church는 컴퓨터 실무 경험이 없었고 수학 이론 자체를 확장하려는 쪽에 가까웠음
    둘의 협업과 대서양을 사이에 둔 소통은 실용과 이론을 결합해 명령형/함수형 이중성, Church-Turing 정리, 정지 문제와 Church 정리의 관계 같은 핵심 이론을 단단히 만들었음
    경쟁으로 보는 건 잘못이고, 컴퓨터 과학에는 “두 아버지”가 있다는 말이 여러 이유에서 적절함
    특히 Turing의 죽음까지 생각하면 더 그렇다
    또한 Turing이 구현에 관심이 없었던 것은 아니며, 실제 구현으로 돌아가고 싶었지만 허용되지 않았다는 점을 빼놓으면 안 됨
    영국 정부의 기밀 분류가 달랐다면 무엇이 달라졌을지 큰 비극과 질문이 남지만, 그랬다면 우리 시간선에서 이론을 그렇게 잘 굳힌 Church와의 협업을 잃었을 수도 있음

• 1982년 8월 CMU에서 열린 ACM Symposium on LISP and Functional Programming에서 Alonzo Church와 Haskell Curry를 만날 수 있었던 건 행운이었음
  Curry는 분명 건강이 좋지 않았고 학회 후 약 2주 뒤 세상을 떠났지만, Church는 건강해 보였고 이후 약 13년을 더 살았음
  리셉션에서 Gerry Sussman이 방을 돌며 두 사람을 소개할 때 매우 들떠 있었고, 우리에게도 그들을 만난 것은 큰 감격이었음

• Church의 큰 기여 중 하나는 그의 제자들이었음
  한곳에서 놀라운 사상가들이 쏟아져 나왔음