数学におけるコンビネータ論理
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/09/10 14:50 UTC 版)
「コンビネータ論理」の記事における「数学におけるコンビネータ論理」の解説
コンビネータ論理は元来、本質的に量化変数を消去することによって量化変数の役割を明確にするような「pre-logic」を意図していた。量化変数を消去する方法にはクワインの述語関手論理がある。コンビネータ論理の表現力は一階述語論理を超える一方、述語関手論理の表現力は一階述語論理と同等である。 コンビネータ論理の最初の発明者であるモイセイ・シェインフィンケリ(ロシア語版、英語版)は、1924年の論文以降それについて何も出版していない(ヨシフ・スターリンが1929年に権力を確固なものとしてからはほとんど出版を行なっていない)。1927年後半、カリーはプリンストン大学の講師として働いているときにコンビネータを再発見した。1930年代後半、アロンゾ・チャーチとプリンストン大学の彼の教え子が、ラムダ計算というライバルとなる関数抽象の形式化を考案し、コンビネータ論理より人気を博すこととなった。こうした歴史的偶然のために、理論計算機科学が60〜70年代にコンビネータ論理に関心を持ち始めるまで、この分野のほとんどすべての業績は、ほとんどカリーとその教え子、もしくはベルギーのロベール・フェイ(英語版)によるものであった。Curry and Feys (1958) および Curry et al. (1972) はコンビネータ論理の初期の歴史についてのサーベイ論文である。より最近のコンビネータ論理とラムダ計算の比較については Barendregt(オランダ語版、英語版) (1984) を参照されたい(デイナ・スコットが60〜70年代に考案したコンビネータ論理のためのモデル理論についても触れている)。
※この「数学におけるコンビネータ論理」の解説は、「コンビネータ論理」の解説の一部です。
「数学におけるコンビネータ論理」を含む「コンビネータ論理」の記事については、「コンビネータ論理」の概要を参照ください。
- 数学におけるコンビネータ論理のページへのリンク