- 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の天才性はスペクタクルではなく、世界を変える厳密な構造と静かな優雅さの中にあった
1件のコメント
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...
プログラミングのさまざまな話題を扱っており、関数型プログラミングにあまり触れてこなかった人にはなじみの薄いパラダイムも開いてくれる
Church が特定の意味というより、ギリシャ文字の中からの任意の選択に近かったことを示唆する別の例は https://en.wikipedia.org/wiki/Lambda_calculus#Origin_of_the_... にある
McCarthy が Lisp を始める前なのか後なのかも気になる
「Church のラムダ計算と Turing 機械は同等の計算能力を持つが、Turing 機械は可変状態を使う点が異なる。今日に至るまで関数型言語と命令型言語の間に亀裂があるのは、Church と state の分離のためだ」
この引用はずっと前から知っていたが、元の出典が見つからない
追記: Guy Steele の「言語の関数型・ラムダ計算部分と、副作用を起こす部分を混ぜたくない人たちがいる。彼らは Church と state の分離を信じているようだ」から来ているのかもしれない
元のアーカイブはここにある: https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/...
ヨーロッパ人はたいてい彼の名前を正しく「Nick-louse Veert」と発音するが、アメリカ人は「Nickel's Worth」に台無しにする、というジョーク
つまり、ヨーロッパ人は名前で呼び、アメリカ人は価値で呼ぶ、ということ
https://en.m.wikiquote.org/wiki/Niklaus_Wirth
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月がある
本全体が読む価値がある
彼の名を冠した 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/
ただ、それでも彼の主要な仕事の一部を取りこぼしていると聞いたし、数学者には哲学的すぎ、哲学者には技術的すぎたのだろうとも思う
本筋ではないが、ブログ記事にAI生成イラストを使うのは少し控えてほしい
Churchの実際の写真はパブリックドメインにもあるのに、このイラストは彼に特に似ているわけでもなく、記事が人気を得るにつれてすでに画像検索結果に出てきている
5分以上かけて生成する価値もないようなイラストなら、単に外したほうがいいのではないかと思う
それでもどうしても「AI」生成画像を使う必要があるなら、少なくともそうキャプションを付けるべきだ
オンラインの写真を持ってくるのに気が進まず、この画像は「偽物のそっくりさん」にならないようにしようとして7回目に作った結果で、ある程度は似ていると感じていた
JvNの画像はかなりうまく作れたが、今後は人物に見える偽のそっくり画像ではなく、象徴的な画像を使うほうが適切だろう
「コンピュータ知能の設計者」という表現は大げさに思える
Churchが優れた論理学者だったのは確かだが、ここでコンピュータ知能がAI/MLを意味するなら、彼の貢献は実質的にない
それとは別に、ラムダ計算が本当に数学なのかもよく分からず、巧妙な記法に近いように見える
記法の利点は主観的なものだし、Churchが自分のアイデアが特定のプログラミング言語設計に着想を与えたことにあまり関心を持っていなかった点も興味深い
STTは高階論理ともよく同一視される。基本的な「個体」と真理値T/Fという2つの原始型、そして関数型
(a --> b)だけで任意の論理的対象を表現できるからだSTTは間違いなくChurchの発明であり、現代の型理論に大きな影響を与え、Haskellのような複雑な型体系を持つプログラミング言語にも影響した
完全に論証できるわけではないが、直感的には、Turingと彼が象徴するものはAIの側で最終的に高く評価される一方、Churchはその逆のように見える
前者は純粋性、可能な最小条件、抽象的で「純粋な」計算から出発し、後者は私たちが実際にどう思考できるかに関心を持ち、実装よりも表現と抽象化の拡張を重視していたように思える
Churchにはコンピュータ実務の経験はなく、数学理論そのものを拡張しようとする側に近かった
2人の協力と大西洋を挟んだコミュニケーションは、実用と理論を結びつけ、命令型／関数型の二重性、Church-Turingの定理、停止問題とChurchの定理の関係といった中核理論を堅固にした
これを競争として見るのは誤りで、コンピュータ科学には「2人の父」がいるという言い方は、いくつもの理由で適切だ
特にTuringの死まで考えるとなおさらである
また、Turingが実装に関心がなかったわけではなく、実際の実装に戻りたかったが許されなかった、という点を抜かしてはならない
英国政府の機密指定が違っていたら何が変わっていたのか、大きな悲劇と疑問が残るが、そうであれば、私たちの時間軸で理論をあれほどよく固めたChurchとの協力を失っていたかもしれない
1982年8月にCMUで開かれた ACM Symposium on LISP and Functional Programming で、Alonzo ChurchとHaskell Curryに会えたのは幸運だった
Curryは明らかに健康状態がよくなく、学会の約2週間後に亡くなったが、Churchは元気そうに見え、その後さらに約13年生きた
レセプションでGerry Sussmanが部屋を回りながら2人を紹介していたとき、とても興奮しており、私たちにとっても彼らに会えたことは大きな感激だった
Churchの大きな貢献の一つは、彼の弟子たちだった
一つの場所から驚くべき思想家たちが次々と輩出された