>>753
>関係ないが論理主義は型理論で最注目
>彼らは結構正しかった

懐かしい
10年以上まえ、政治板に居たとき 多分コンピューター系の人だと思うが
「型なしラムダ計算」というのを教えて貰った
下記”1930年代に数学者のアロンゾ・チャーチとスティーヴン・コール・クリーネによって、「計算できるとはどういうことか」を厳密に定義するために考案された。当時はまだ電子計算機は実用化されておらず、ラムダ計算は純粋に理論的な数学的体系として発展した。関数を定義する際にギリシャ文字のラムダ（λ）を使う慣習からその名がある”
”チューリングマシン（仮想的な機械のテープとヘッドの動きで計算を表現するモデル）と計算能力において等価である”

(参考)
https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97
ラムダ計算（lambda calculus）は、計算という行為を「関数」の定義と適用だけで表現する計算模型（数理モデル）である。ラムダ算法とも言う。
1930年代に数学者のアロンゾ・チャーチとスティーヴン・コール・クリーネによって、「計算できるとはどういうことか」を厳密に定義するために考案された。当時はまだ電子計算機は実用化されておらず、ラムダ計算は純粋に理論的な数学的体系として発展した。関数を定義する際にギリシャ文字のラムダ（λ）を使う慣習からその名がある。
ラムダ計算は、変数と関数の抽象化、および関数の適用という基本的な操作のみから構成されるが、全ての計算可能関数を表現できるチューリング完全な計算体系である。ラムダ計算は、アラン・チューリングが考案したチューリングマシン（仮想的な機械のテープとヘッドの動きで計算を表現するモデル）と計算能力において等価である。
ラムダ計算は、理論計算機科学や論理学の基礎理論として重要な位置を占めている。特にLISP、Haskell、MLといった関数型言語の理論的基盤となっており、Java（Java 8以降）、C#、Python、JavaScriptなど多くの主流プログラミング言語に導入されている「ラムダ式」（無名関数）の機能は、ラムダ計算の概念に基づいている。
本記事では、チャーチが提唱した元来の「型無しラムダ計算」を中心に述べる。

https://ja.wikipedia.org/wiki/%E5%9E%8B%E4%BB%98%E3%81%8D%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97
型付きラムダ計
型付きラムダ計算（typed lambda calculus）とは、無名の関数の抽象表現にラムダ (
λ というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。

ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。

様々な型付きラムダ計算がこれまで研究されてきた。単純型付きラムダ計算はいくつかの基本型（または型変数）と関数型
σ→τ から成る