単純な型付きラムダ計算

単純型ラムダ計算（⁠${\displaystyle \lambda ^{\to }}$型理論の一形態あるラムダ計算は、型コンストラクタが1つしかない型付き解釈である（${\displaystyle \to }$⁠ )関数型を構築する。これは、型付きラムダ計算の標準的かつ最も単純な例である。単純な型付きラムダ計算は、型なしラムダ計算の逆説的な使用を避ける試みとして、1940 年にアロンゾ・チャーチによって最初に導入された。 ^{[ 1 ]}

単純型という用語は、積、余積、自然数などの構成要素（System T）や、完全再帰（PCFなど）を用いた単純型ラムダ計算の拡張を指す場合にも使用されます。対照的に、多相型（ System Fなど）や依存型（Logical Frameworkなど）を導入するシステムは、単純型とはみなされません。完全再帰を除く単純型は、そのような構造のチャーチ符号化が1 文字のみで実現できるため、依然として単純型とみなされます。 ${\displaystyle \to }$また、適切な型変数も使用できますが、多態性や依存性は使用できません。

1930年代、アロンゾ・チャーチはロジスティック法を用いようとした。^{[ a ]}記号表現に基づく形式言語としての彼のラムダ計算は、可算無限の公理と変数の系列から成り、 ^{[ b ]}抽象化とスコープを表す有限個の基本記号の集合、およびそれぞれ否定、選言、全称量化、選択を表す4つの定数、^{[ d ] [ e ]さらに、有限個の}規則IからVIの集合も含まれていた。この有限個の規則の集合には、規則Vのモーダス・ポネンス、およびそれぞれ置換と一般化を表す規則IVとVIが含まれていた^。 [ ^d ]^{規則Iから}IIIは、ラムダ計算ではアルファ、ベータ、イータ変換として知られている。チャーチは、解釈のない記号表現を記述するための構文言語（つまりメタ数学言語）としてのみ英語を用いようとした。^{[ f ]}

1940年、チャーチは記号式における型を表すために添え字表記を採用した。^{[ b ]}チャーチは発表の中で、2つの基本型のみを使用した。${\displaystyle o}$「命題の種類」と${\displaystyle \iota }$「タイプの個人」について。${\displaystyle o}$項定数はなく、${\displaystyle \iota }$1 つの項定数を持つ。通常、基底型が 1 つだけの微積分は、${\displaystyle o}$⁠、が考慮されます。ギリシャ文字の添え字⁠${\displaystyle \alpha }$⁠、 ⁠${\displaystyle \beta }$⁠、など は型変数を表します。括弧付きの添え字は${\displaystyle (\alpha \beta )}$関数型を表します${\displaystyle \beta \to \alpha }$⁠ . Church 1940 p.58 では「矢印または」を使用しました。${\displaystyle \to }$⁠ ' は を表し、はの略語です。 ^{[ g ]} 1970年代までには、単独の矢印表記が使用されるようになりました。たとえば、この記事では、添え字のない記号が使用されています。${\displaystyle \sigma }$そして$\displaystyle \tau }$型の範囲は、無限の公理が規則 I から VI を型に適用した結果であることが判明しました (ペアノ公理を参照)。非公式には、関数型は${\displaystyle \sigma \to \tau }$型 の入力が与えられた場合に、 となる関数のタイプを指します。${\displaystyle \sigma }$⁠、タイプの出力を生成します⁠$\displaystyle \tau }$慣例として、${\displaystyle \to }$右側の同僚たち：${\displaystyle \sigma \to \tau \to \rho }$と読みます。${\displaystyle \sigma \to (\tau \to \rho )}$⁠ .

型を定義するために、一連の基本型、${\displaystyle B}$⁠、まず定義する必要があります。これらは、アトミック型または型定数と呼ばれることもあります。これが確定すると、型の構文は次のようになります。

${\displaystyle \tau \;{{:}{:=}}\;\tau \to \tau \mid T\quad \mathrm {ただし} \quad T\in B.}$

例えば、${\displaystyle B=\{a,b\}}$⁠、で始まる無限の型セットを生成します。${\displaystyle a}$⁠、 ⁠${\displaystyle b}$⁠、 ⁠${\displaystyle a\to a}$⁠、 ⁠${\displaystyle a\to b}$⁠、 ⁠${\displaystyle b\to b}$⁠、 ⁠${\displaystyle b\to a}$⁠、 ⁠${\displaystyle a\to (a\to a)}$⁠、...、 ⁠${\displaystyle (b\to a)\to (a\to b)}$⁠、...

基本型には、一連の項定数も固定されています。例えば、基本型の1つがnatであると仮定すると、その項定数は自然数となる可能性があります。

単純型ラムダ計算の構文は、基本的にラムダ計算そのものの構文と同じです。${\displaystyle x{\mathbin {:}}\tau }$変数${\displaystyle x}$タイプは⁠$\displaystyle \tau }$構文という用語は、バッカス・ナウア記法では、変数参照 、抽象化、適用、または定数である。

${\displaystyle e\;{{:}{:=}}\;x\mid \lambda x\mathbin {:} \tau .e\mid e\,e\mid c}$

どこ${\displaystyle c}$は項定数です。変数参照${\displaystyle x}$抽象化バインディング内にある場合はバインドされます。${\displaystyle x}$項は、未束縛変数がない場合に閉じている。

それに対し、型付けのないラムダ計算の構文には、そのような型付けや項定数は存在しない。

${\displaystyle e\;{{:}{:=}}\;x\mid \lambda xe\mid e\,e}$

型付きラムダ計算では、すべての抽象化（つまり関数）は引数の型を指定しなければならない。

特定の型の型付けされたラムダ項の集合を定義するには、項と型の間の型付け関係を定義する。まず、型付けコンテキスト、または型付け環境を導入する。${\displaystyle \ガンマ ,\デルタ ,\ドット }$これらは型付けに関する仮定の集合です。型付けに関する仮定は次の形式をとります。${\displaystyle x{\mathbin {:}}\sigma }$⁠、つまり変数${\displaystyle x}$タイプがあります⁠${\displaystyle \sigma }$⁠ .

型付け関係${\displaystyle \Gamma \vdash e{\mathbin {:}}\sigma }$は、${\displaystyle e}$タイプの用語です${\displaystyle \sigma }$文脈において${\displaystyle \Gamma }$この場合${\displaystyle e}$型が適切である（型が⁠${\displaystyle \sigma }$型付け関係のインスタンスは型付け判断と呼ばれます。型付け判断の妥当性は、型付け規則を使用して構築された型付け導出を提供することによって示されます（この導出では、行の上の前提から行の下の結論を導出できます）。単純型付けラムダ計算では、次の規則を使用します。 ^{[ h ]}

言葉で言うと、

1. もし${\displaystyle x}$型を持つ${\displaystyle \sigma }$その文脈では、${\displaystyle x}$タイプがあります⁠${\displaystyle \sigma }$⁠ .
2. 項定数は適切な基本型を持つ。
3. ある特定の状況下で${\displaystyle x}$タイプを持つ⁠${\displaystyle \sigma }$⁠、${\displaystyle e}$タイプがあります⁠${\displaystyle \tau }$⁠、そして同じ文脈で、 ⁠${\displaystyle x}$⁠、 ⁠${\displaystyle \lambda x{\mathbin {:}}\sigma .~e}$型を持つ${\displaystyle \sigma \to \tau }$⁠ .
4. ある状況下では、${\displaystyle e_{1}}$タイプがあります⁠${\displaystyle \sigma \to \tau }$⁠、そして${\displaystyle e_{2}}$タイプがあります⁠${\displaystyle \sigma }$⁠、それから${\displaystyle e_{1}~e_{2}}$タイプがあります⁠${\displaystyle \tau }$⁠ .

空のコンテキストで入力可能な用語、つまり閉じた用語の例は次のとおりです。

• あらゆるタイプに対応${\displaystyle \tau }$⁠、用語${\displaystyle \lambda x{\mathbin {:}}\tau .x{\mathbin {:}}\tau \to \tau }$（恒等関数／Iコンビネータ）、
• タイプ別⁠${\displaystyle \sigma ,\tau }$⁠、用語${\displaystyle \lambda x{\mathbin {:}}\sigma .\lambda y{\mathbin {:}}\tau .x{\mathbin {:}}\sigma \to \tau \to \sigma }$（Kコンビネータ）
• タイプ別⁠${\displaystyle \tau ,\tau ',\tau ''}$⁠、用語${\displaystyle \lambda x{\mathbin {:}}\tau \to \tau '\to \tau ''.\lambda y{\mathbin {:}}\tau \to \tau '.\lambda z{\mathbin {:}}\tau .xz(yz):(\tau \to \tau '\to \tau '')\to (\tau \to \tau ')\to \tau \to \tau ''}$（Sコンビネーター）

これらは、組み合わせ論理の基本コンビネータの型付きラムダ計算表現です。

各タイプ${\displaystyle \tau }$順序、番号が割り当てられる${\displaystyle o(\tau )}$⁠ . 基本型の場合、${\displaystyle o(T)=0}$⁠ ; 関数型の場合、 ⁠${\displaystyle o(\sigma \to \tau )={\mbox{max}}(o(\sigma )+1,o(\tau ))}$つまり、型の順序は、最も左にネストされた矢印の深さを測定する。したがって、次のようになる。

${\displaystyle o(\iota \to \iota \to \iota )=1}$

${\displaystyle o((\iota \to \iota )\to \iota )=2}$

上記の説明は、単純型ラムダ計算の構文を定義する唯一の方法ではありません。

標準的な意味論を前提とすると、単純型ラムダ計算は強く正規化される。すなわち、すべての還元シーケンスは最終的に終了する。^{[ 10 ]}これは、型付け規則によって再帰が許可されていないためである。固定点コンビネータとループ項の型を見つけることは不可能である。${\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)}$再帰は、特別な演算子を用意することで言語に追加できます。${\displaystyle {\mathtt {fix}}_{\alpha }}$タイプの${\displaystyle (\alpha \to \alpha )\to \alpha }$あるいは、一般的な再帰型を追加するという方法もあるが、どちらも強力な正規化を排除してしまう。

型なしラムダ計算とは異なり、単純型付きラムダ計算はチューリング完全ではありません。単純型付きラムダ計算では、すべてのプログラムが停止します。一方、型なしラムダ計算では、停止しないプログラムが存在し、さらに、プログラムが停止するかどうかを判定できる一般的な判定手順は存在しません。

• テイトは1967年に、${\displaystyle \beta }$-還元は強く正規化する。^{[ 10 ]}結果として${\displaystyle \beta \eta }$-同値性は決定可能である。スタットマンは1979年に正規化問題が非初等的であることを示した^{[ 13 ]。}この証明は後にメアソンによって簡略化された^{[ 14 ]} 。この問題は集合に属することが知られている。${\displaystyle {\mathcal {E}}^{4}}$Grzegorczyk階層[ 15 ^{] 、}より正確にはTOWERと呼ばれる複雑性クラスにおいて完全である^{[ 16 ]}。純粋に意味論的な正規化証明（評価による正規化を参照）は^、 1991年にBergerとSchwichtenbergによって与えられた^{[ 17 ]。}
• 統一問題​${\displaystyle \beta \eta }$-同値性は決定不能です。Huet は 1973 年に 3 階の単一化が決定不能であることを示し^{[ 18 ]}、これは 1978 年に Baxter ^{[ 19 ]}、1981 年に Goldfarb ^{[ 20 ]}によって、2 階の単一化がすでに決定不能であることを示すことで改善されました。高階のマッチング (1 つの項のみが存在変数を含む単一化) が決定可能であるという証明は、2006 年に Colin Stirling によって発表され、完全な証明は 2009 年に公開されました。^{[ 21 ]}
• 自然数は、次のタイプの用語で符号化できます。${\displaystyle (o\to o)\to (o\to o)}$（教会数字）。シュヴィヒテンベルクは1975年に、${\displaystyle \lambda ^{\to }}$拡張多項式は、チャーチ数上の関数として表現できます。^{[ 22 ]}これらは、条件演算子の下で閉じられた多項式とほぼ一致します。
• 完全なモデル${\displaystyle \lambda ^{\to }}$これは、基本型を集合として、関数型を集合論的関数空間として解釈することによって与えられる。フリードマンは1975年に、この解釈が完全であることを示した。${\displaystyle \beta \eta }$-等価性、基底型が無限集合によって解釈される場合。^{[ 23 ]}スタットマンは1983年に、${\displaystyle \beta \eta }$-同値性とは、通常曖昧な、つまり型置換の下で閉じている最大の同値性である（スタットマンの典型的な曖昧性定理）。^{[ 24 ]}このことから、有限モデル特性が成り立つ、つまり有限集合は、によって識別されない項を区別するのに十分であるということが挙げられる。${\displaystyle \beta \eta }$-等価。
• プロトキンは1973年に、ラムダ項で定義可能なモデルの要素を特徴付けるために論理関係を導入した。^{[ 25 ]} 1993年にユングとティウリンは、論理関係の一般形（可変アリティのクリプキ論理関係）がラムダ定義可能性を正確に特徴付けることを示した。^{[ 26 ]}プロトキンとスタットマンは、有限集合から生成されたモデルの与えられた要素がラムダ項で定義可能かどうかは決定可能であると予想した（プロトキン・スタットマン予想）。この予想は2001年にローダーによって誤りであることが示された。^{[ 27 ]}

• Loader, Ralph (1998 年 2 月). 「単純型付きラムダ計算に関するノート」 .
• スタンフォード哲学百科事典の「チャーチの型理論」の項目