20/05/13 13:11:16 uMe8boWM.net
>>607
つづき
型無しラムダ計算
20年ほど時代を下り，1930年代に話題を移そう．若き日の Alonzo Church は，自由変数を用いない*19形式論理学の記法あるいは計算体系として，ラムダ計算を提案する．
初出は1932年の A Set of Postulates for the Foundation of Logic であるようで，表題からも分かる通り，この頃の Church はラムダ計算を論理学の基礎として据えようと考えていたらしく，項として種々の論理定項を含んでいる．
しかし，このオリジナルの体系は証明力が強すぎたため，後に Stephen Kleene と John Barkley Rosser らにより矛盾を導くことが証明された*20．
単純型付ラムダ計算
1940年に発表された A Formulation of the Simple Theory of Types という論文が，型付きラムダ計算の初出とされている．
ラムダ計算と階型理論を統合することで，どのような嬉しい性質が生じるのかはこの論文には記されていないが，ともかく Church は 従来のラムダ計算に加えて，型という概念を導入する．
つづく