Simply typed lambda calculus とは

タイプ理論の形式である単純型のラムダ計算( λ {\displaystyle \lambda ^{\to }} )は、ラムダ計算の型付き解釈であり、関数型を構築する1つの型のコンストラクタのみを使用します。これは型付きラムダ計算のカノニカルで簡単な例です。単純に型付けされたラムダ計算は、元来、型なしラムダ計算の逆説的な使用を避ける試みとして、1940年にAlonzo Churchによって導入されたものであり、多くの望ましい興味深い特性を示しています。
シンプルタイプという用語は、製品、副産物または自然数(System T)、または完全再帰(PCFなど)などの単純型のラムダ計算の拡張を指すためにも使用されます。対照的に、多態型(システムFのような)や従属型(論理的フレームワークのような)を導入するシステムは単純に型付けされたものとはみなされません。前者は、完全な再帰を除いて、そのような構造の教会符号化は {\displaystyle \to } と適切な型変数を使って行うことができるため、多形性や依存性はできません。