An Introduction to Functional Programming Through Lambda Calculusを読んでいたら、最初の章に functional language の歴史が書かれていたので、簡単にまとめて見ました。
Propositional calculus
Propositional calculus Systemで「命題計算系」です。19世紀中頃に、ハミルトン、ドモルガン、ブール達によって、形式化されました。基本的な値としてtrue、falseを使い、基本的な演算子として、and、or、notを使います。Propositional calculusによって、任意の式(expression)が、原理(theorem)(常に真)かどうかを証明(prove)できます。常に真である基本的な式である公理(axioms)から開始し、公理と既知の原理に推論規則(rule of inference)を適用しながら、新しい原理の証明を行います。デジタル回路でも同じ事が表現できます。
wolframの説明 http://mathworld.wolfram.com/PropositionalCalculus.html
Predicate calculus
訳語としては、こちらも命題計算に入りそうですがよくわかりません。Propositional calculusを、数、集合、文字列といった非論理な値に拡張した物です。論理式を論理では無い値に拡張したpredicate*1と、非論理の値に対する演算として関数functionを導入しています。また、連続する値の特徴を記述するために、全称記号(universal quantifier)∀や存在記号(existential quantifier)∃等のquantifiersのアイデアを導入しました。Predicate calculusは、PROLOGの様なロジックプログラミングや、推論規則を使ったエキスパートシステムの基礎になりました。
Propositional calculusとPredicate calculusは、名前と値の対応は変わらず、式は評価の順番を必要としない（どの順番に評価しても結果は同じ）であることが特徴です。
Number theoryとPrincipia Mathematica
19世紀の終わりにペアノが数論(number theory)を形式化(ペアノの公理)しました。ペアノの公理によって、数は0とsuccessor functionによって定義されました。任意の数は0のsuccessorの数で表せるようになりました。数論での証明は、再帰(recursion)と同じような帰納(induction)の形に基づいています。
世紀の変わり目に、ラッセルとホワイトヘッドが、プリンキピア・マテマティカ(Principia Mathematica)で、論理式から数式への直接の導出を試みました。次にヒルベルトが、Prinsipiaが数式を完全に記述できることをデモンストレーションするために、'Program'を提案しました。ヒルベルトは、数学のPrincipiaの記述は、一貫している(consistent)という証明を要求しました(ヒルベルト・プログラム)。残念なことに、1931年に、ゲーデルは数学は自己の無矛盾性を証明できない事を示しました(「不完全性定理」)。
Theory of computability
しかし、ヒルベルトプログラムは、計算可能性理論(Theory of computability)に続く研究を大きく進めました。
1936年に、計算可能性について3つの異なった形式的なアプローチが提案されました。
3つのアプローチは、すべて簡単な基本演算と演算の構成のための簡単なルールで定義されています。大切なことは、すべて証明論(proof theory)であることです。
これらの３つのアプローチはお互いに等価であると示され、ノイマンのマシン（デジタルコンピュータ）によって一般化されました。これによって、あるシステムで得た結果は他の等価なシステムの結果と同じ等価性を持ち、どのシステムも他のシステムをモデル化することができます。実際に、その結果もデジタルコンピュータ言語(computer language)に適用でき、どのシステムもコンピュータ言語を記述することができます。逆に、コンピュータ言語は、どのシステムも記述でき、従ってどのシステムも実装できます。チャーチは、すべての計算可能性の記述は等価であると仮定しました。一方、チャーチのテーゼ(Church's thesis)は形式的には証明できませんでした。
チューリングマシーン、再帰理論、λ計算の違い
チューリングマシーン、再帰理論、λ計算には、大きな違いがあります。チューリングマシーンのアプローチは、代入と評価の順番に基づくシンボルの操作に関心があります。再帰理論とλ計算は、構造化された関数適用としての計算を重要視しています。再帰理論とλ計算は、評価の順番に依存しません。
チューリングは、チューリングマシーンが停止するかどうかを知ることは不可能であるとデモンストレーションしました。チューリングの停止性問題(halting problem)です。これは、再帰理論とλ計算にも当てはまります。しかし、チャーチとロッサーは、違う評価の順番によって停止するなら、その結果は同じになることを示しました。また、特定の評価順序が、他の順序よりも停止しやすい事も示しました。(Church–Rosser theorem)。これは計算にたいして重要な関わりがあります。なぜなら、プログラムのある部分はある順番で、別の部分は別の順番で実行すればより効率的になるからです。実際、プログラミング言語が評価順から独立しているとき、プログラムの一部を平行に実行することが可能になります。
現在、再帰理論とλ計算は、関数プログラミングのバックボーンであり、計算を通して広く応用されています。
*1:私はpredicateを述語と訳さない派。
