型付きラムダ計算

数学およびコンピュータ科学において、型付きラムダ計算とは、ラムダ記号（${\displaystyle \lambda }$）匿名関数の抽象化を表す。この文脈では、型は通常、ラムダ項に割り当てられる構文的な性質を持つオブジェクトである。型の正確な性質は、考慮される計算体系によって異なる（下記の「種類」を参照）。ある観点からは、型付きラムダ計算は型なしラムダ計算の改良と見なすことができるが、別の観点からは、型付きラムダ計算はより基本的な理論であり、型なしラムダ計算は1つの型のみを持つ特殊なケースであると考えることもできる。^{[ 1 ]}

型付きラムダ計算はプログラミング言語の基礎であり、 MLやHaskellなどの型付き関数型プログラミング言語、そして間接的には型付き命令型プログラミング言語の基盤となっています。型付きラムダ計算はプログラミング言語の型システムの設計において重要な役割を果たします。ここで、型付け可能性は通常、プログラムの望ましい特性（例えば、プログラムがメモリアクセス違反を引き起こさないこと）を捉えます。

型付きラムダ計算は、カリー・ハワード同型性を介して数理論理学や証明論と密接に関連しており、特定のカテゴリーの内部言語とみなすことができます。例えば、単純型付きラムダ計算は、デカルト閉圏（CCC）の言語です。^{[ 2 ]}

様々な型付きラムダ計算が研究されてきた。単純型付きラムダ計算は、矢印という1つの型コンストラクタのみを持つ。${\displaystyle \to }$、その型は基本型と関数型のみです。${\displaystyle \sigma \to \tau }$システム T は、単純型ラムダ計算を自然数の型と高階原始再帰で拡張します。このシステムでは、ペアノ算術で証明可能なすべての関数が定義可能です。システム F は、すべての型に対する全称量化を使用することで多相性を可能にします。論理的な観点からは、2 階論理で証明可能なすべての関数を記述できます。依存型を持つラムダ計算は、直観主義型理論、構成計算、および依存型を持つ純粋ラムダ計算である論理フレームワーク(LF)の基礎となっています。純粋型システムに関する Berardi の研究に基づいて、Henk Barendregtは、純粋型ラムダ計算 (単純型ラムダ計算、システム F、LF、構成計算を含む) の関係を体系化するためにラムダキューブを提案しました。^{[ 3 ]}

型付きラムダ計算の中には、サブタイピングの概念を導入するものもある。${\displaystyle A}$は、${\displaystyle B}$すると、すべてのタイプの項${\displaystyle A}$またタイプもある${\displaystyle B}$型付きラムダ計算とサブタイピングは、連言型とシステム F _<:を持つ単純な型付きラムダ計算です。

これまで述べたシステムは、型なしラムダ計算を除いて、すべて強正規化です。つまり、すべての計算は終了します。したがって、すべてのチューリング計算可能な関数を記述することはできません。^{[ 4 ]}また、論理として一貫性があり、つまり、空いている型が存在します。ただし、強正規化しない型付きラムダ計算も存在します。たとえば、すべての型の型 (Type : Type) を持つ依存型付きラムダ計算は、ジラールのパラドックス のために正規化しません。このシステムは、最も単純な純粋型システムでもあり、ラムダキューブを一般化した形式体系です。プロトキンの「計算可能な関数のためのプログラミング言語」(PCF)のような明示的な再帰コンビネータを持つシステムは正規化しませんが、論理として解釈されることを意図していません。実際、PCFは典型的な型付き関数型プログラミング言語であり、型はプログラムが適切に動作することを保証するために使用されるが、必ずしもプログラムが終了することを保証するものではない。

コンピュータプログラミングでは、厳密な型付けを持つプログラミング言語のルーチン（関数、プロシージャ、メソッド）は、型付きラムダ式に密接に対応します。^{[ 5 ]}

• カッパ計算― 高階関数を除外した型付きラムダ計算の類似物

• Barendregt, Henk (1992). "型付きラムダ計算" . Abramsky, S. (編)『背景：計算構造』 . コンピュータサイエンスにおける論理学ハンドブック. 第 2巻. オックスフォード大学出版局. pp. 117–309 . ISBN  9780198537618。
• ブランドル、ヘルムート（2022）。構成の計算 / 型付きラムダ計算