型付きラムダ計算
イメージ的には以下のような階層関係mrsekut.icon
それ以外の型付きラムダ計算
$ \mathbb{T}と基本型の種類
$ \mathbb{T}はそこで取り扱う全ての型の集合
基本型が一つの型全体は$ \mathbb{T}^0と表記する
例えばboolやstringがなく、numberとその関数型のみの世界
この唯一の型のことは$ 0型として扱う
可算無限個の基本型を考えるときの型全体は$ \mathbb{T}^\infinと表記する
型付きラムダ計算では$ \mathbb{T}^0か$ \mathbb{T}^\infin上で議論することが多いらしい $ \lambda x^{A}.M:A\rightarrow B.
最初のxの肩に乗っているのが引数の型
コロンの後に書かれているのはラムダ抽象の型
この表記に2回Aが出てくる理由はあるのかな。コロンの後の方だけで十分に思えるが
省略されることもあるみたい
型の付くプログラムは必ず停止する？
型なしラムダ計算と表示が異なるかは不明
やってることは同じ
$ (\lambda x^A.M)(N)=M[N/x] .
型付きラムダ計算では、「正しく型付けされた計算は全て停止する」こと保証するような体系を考える ref TaPL.icon pp.1-2
この点において、普通の?型システムとは研究の方向性が異なるらしい
普通の?方は、プログラミング言語などに応用されるが、
では、ラムダ計算の方は何に応用されていくんだろうmrsekut.icon
論理学とか、計算機の停止性とかなんかな、
関連
参考
型付きラムダ計算と停止性の話
基本
かりースタイルとチャーチスタイル