単純型付きラムダ計算
Simply Typed Lambda-Calculus, STLC
基本型にも色々含まれるが、どれを選ぶか、いくつ選ぶかは本質ではないらしい
なので、最もシンプルな例として、Booleanのみを扱う単純型付きラムダ計算を考えるとわかりやすい
1958
用いる型の定義
$ a\in\mathbb{A}\Rightarrow a\in \mathbb{T}
$ \sigma,\tau\in\mathbb{T}\Rightarrow (\sigma\to\tau)\in\mathbb{T}
このとき$ \mathbb{T}の元のことを型という 例えば基本型AとBがある場合は以下のようなものが考えられる
A→B、((A→B)→B)→B
単純型付きラムダ計算の意味論
型$ A→Bな関数に対応する集合は、$ A型から$ B型への写像全体の集合
単純mrsekut.icon
再帰的なプログラムを解釈するための意味論 ref 『圏論の歩き方』.icon p.63
これなんていうんだろうmrsekut.icon
データ型をある種の順序集合に、プログラムをある種の連続性を満たす写像に対応させる意味論
帰納的関数の概念に基づいた意味論
関連
参考
規則など