名前の通り、型を用いたラムダ計算を扱う

イメージ的には以下のような階層関係

それ以外の型付きラムダ計算

基本型 (basic type)以外のものを扱うような型付きラムダ計算のこと

\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 pp.1-2

この点において、普通の?型システムとは研究の方向性が異なるらしい

普通の?方は、プログラミング言語などに応用されるが、

では、ラムダ計算の方は何に応用されていくんだろう

論理学とか、計算機の停止性とかなんかな、

関連

参考

『圏論の歩き方』 4章

型付きラムダ計算と停止性の話

基本

かりースタイルとチャーチスタイル