基本型 (basic type)の集まりの上で構成される型付きラムダ計算

最もシンプルな型付きラムダ計算といえる

基本型にも色々含まれるが、どれを選ぶか、いくつ選ぶかは本質ではないらしい

なので、最もシンプルな例として、Booleanのみを扱う単純型付きラムダ計算を考えるとわかりやすい

Haskell Brooks Curry、Robert Feys

1958

型付きラムダ計算とCCCと直観主義論理の対応がある

β簡約が必ず終了する

強正規化する

用いる型の定義

基本型 (basic type)の集合\mathbb{A}に対し、集合\mathbb{T}を以下のように定義する

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型への写像全体の集合

単純

再帰的なプログラムを解釈するための意味論 ref p.63

これなんていうんだろう

データ型をある種の順序集合に、プログラムをある種の連続性を満たす写像に対応させる意味論

帰納的関数の概念に基づいた意味論

関数モデルのことかな #??

いくつもの可能世界論でパラメとライズした意味論

関連

参考

TaPL 9章

規則など

『圏論の歩き方』 4章