単純な型付けのラムダ計算

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

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

構文

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

1940 年に Church は記号式で型を表すための下付き表記法を採用しました。^{[ b ]} Church は発表の中で、「命題の型」と「個体の型」の 2 つの基本型のみを使用しました。型には項定数がありませんが、 には項定数が 1 つあります。1 つの基本型 (通常は⁠ ⁠ )のみを使用した計算がよく検討されます。ギリシャ文字の添え字⁠ ⁠、⁠ ⁠などは型変数を表します。括弧で囲まれた添え字は関数型⁠ ⁠を表します。Church 1940 p.58 では「矢印または⁠ ⁠」を使用して、 が を表し、がの略語であることを示します。^{[ g ]} 1970 年代までには、独立した矢印表記法が使用されるようになりました。たとえば、この記事では添え字のない記号と は複数の型にまたがることができます。無限の数の公理は、規則IからVIを型に適用することの帰結であることが明らかになった（ペアノ公理を参照）。非公式には、関数型とは、型⁠ ⁠の入力が与えられたときに型⁠ ⁠の出力を生成する関数の型を指す。慣例により、は右側に関連付けられ、⁠ ⁠と読みます。 ${\displaystyle o}$ ${\displaystyle \iota}$ ${\displaystyle o}$ ${\displaystyle \iota}$ ${\displaystyle o}$ ${\displaystyle \alpha}$ ${\displaystyle \beta}$ ${\displaystyle (\alpha \beta )}$ ${\displaystyle \beta \to \alpha }$ ${\displaystyle \to}$ ${\displaystyle \sigma }$ ${\displaystyle \tau}$ ${\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 {where} \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 x.e\mid e\,e}$

一方、型付きラムダ計算では、すべての抽象化(つまり関数) は引数の型を指定する必要があります。

入力ルール

与えられた型のラムダ項の型付けが適切である集合を定義するには、項と型の間の型付け関係を定義します。まず、型付けコンテキスト（または型付け環境） を導入します。これは型付け仮定の集合です。型付け仮定は⁠ ⁠という形式であり、これは変数が⁠ ⁠型であることを意味します。 ${\displaystyle \Gamma ,\Delta ,\dots }$ ${\displaystyle x{\mathbin {:}}\sigma }$ ${\displaystyle x}$ ${\displaystyle \sigma }$

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

${\displaystyle {\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x{\mathbin {:}}\sigma }}}$ （1）	${\displaystyle {\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c{\mathbin {:}}T}}}$ （2）
${\displaystyle {\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e{\mathbin {:}}\tau }{\Gamma \vdash (\lambda x{\mathbin {:}}\sigma .~e){\mathbin {:}}(\sigma \to \tau )}}}$ （3）	${\displaystyle {\frac {\Gamma \vdash e_{1}{\mathbin {:}}\sigma \to \tau \quad \Gamma \vdash e_{2}{\mathbin {:}}\sigma }{\Gamma \vdash e_{1}~e_{2}{\mathbin {:}}\tau }}}$ （4）

言葉で言えば、

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 }$ に対して、項（恒等関数/Iコンビネータ）${\displaystyle \lambda x{\mathbin {:}}\tau .x{\mathbin {:}}\tau \to \tau }$
• 型⁠ ⁠${\displaystyle \sigma ,\tau }$ の場合、項（Kコンビネータ）、および${\displaystyle \lambda x{\mathbin {:}}\sigma .\lambda y{\mathbin {:}}\tau .x{\mathbin {:}}\sigma \to \tau \to \sigma }$
• 型⁠ ⁠${\displaystyle \tau ,\tau ',\tau ''}$ の場合、項(S コンビネータ)。${\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 ''}$

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

それぞれの型には順序、つまり数値が割り当てられます。基本型の場合は ⁠ ⁠ 、関数型の場合は⁠ ⁠です。つまり、型の順序は最も左にネストされた矢印の深さを表します。したがって、 ${\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}$

セマンティクス

内的解釈と外的解釈

大まかに言えば、単純型付きラムダ計算に意味を割り当てる方法は 2 つあり、型付き言語全般に関しては、固有 vs. 外在的、オントロジー vs. 意味論、チャーチスタイル vs. カリースタイルなど様々に呼ばれます。^{[ 1 ] [ 7 ] [ 8 ]} 固有意味論は型付けの適切な用語にのみ意味を割り当てます。より正確には、型付け導出に直接意味を割り当てます。この結果、型注釈のみが異なる用語に異なる意味を割り当てることができます。たとえば、整数の恒等項とブール値の恒等項は異なる意味を持つ場合があります (従来意図されている解釈は、整数の恒等関数とブール値の恒等関数です)。対照的に、外在意味論は型付けに関係なく、型なし言語で解釈される場合と同じように用語に意味を割り当てます。この見方では、とは同じもの (つまり、 ⁠ ⁠と同じもの) を意味します。 ${\displaystyle \lambda x{\mathbin {:}}{\mathtt {int}}.~x}$ ${\displaystyle \lambda x{\mathbin {:}}{\mathtt {bool}}.~x}$ ${\displaystyle \lambda x{\mathbin {:}}{\mathtt {int}}.~x}$ ${\displaystyle \lambda x{\mathbin {:}}{\mathtt {bool}}.~x}$ ${\displaystyle \lambda x.~x}$

本質的意味論と外在的意味論の区別は、ラムダ抽象化における注釈の有無と関連付けられることがあるが、厳密に言えばこの用法は不正確である。注釈付き用語に外在的意味論を定義することは、単に型を無視することによって（つまり、型消去によって）可能である。同様に、注釈なし用語に、文脈から型を推測できる場合（つまり、型推論によって）本質的意味論を与えることも可能である。本質的アプローチと外在的アプローチの本質的な違いは、型付け規則を言語を定義するものと見なすか、それともより原始的な基礎言語の特性を検証するための形式主義と見なすかという点だけである。以下で論じる様々な意味論的解釈のほとんどは、本質的観点と外在的観点のどちらからも見ることができる。

方程式理論

単純型付きラムダ計算（STLC）は、型なしラムダ計算と同じβη同値性の方程式理論を持つが、型制約を受ける。ベータ削減の方程式は^{[ i ]である。}

${\displaystyle (\lambda x{\mathbin {:}}\sigma .~t)\,u=_{\beta }t[x:=u]}$

および⁠ ⁠ の文脈ではいつでも成立するが、イータ縮小の式^{[ j ]}${\displaystyle \Gamma }$ ${\displaystyle \Gamma ,x{\mathbin {:}}\sigma \vdash t{\mathbin {:}}\tau }$ ${\displaystyle \Gamma \vdash u{\mathbin {:}}\sigma }$

${\displaystyle \lambda x{\mathbin {:}}\sigma .~t\,x=_{\eta }t}$

が成り立ち、⁠ ⁠において自由出現しない。型付きラムダ計算の利点は、STLCにより潜在的に終了しない計算を短縮（つまり、削減）できることである。^{[ 9 ]}${\displaystyle \Gamma \vdash t{:}\sigma \to \tau }$ ${\displaystyle x}$ ${\displaystyle t}$

操作的意味論

同様に、単純型ラムダ計算の操作的意味論は、型なしラムダ計算と同様に、名前呼び出し、値呼び出し、またはその他の評価戦略を用いて固定することができます。あらゆる型付き言語と同様に、型安全性はこれらすべての評価戦略の基本的な特性です。さらに、後述する強い正規化特性は、あらゆる評価戦略がすべての単純型項で停止することを意味します。^{[ 10 ]}

カテゴリカルセマンティクス

積型、ペアリング演算子、および射影演算子（-同値性を持つ）を備えた単純型ラムダ計算は、ヨアヒム・ラムベックによって初めて観察されたように、カルティシアン閉圏（CCC）の内部言語である。^{[ 11 ]} 任意のCCCが与えられた場合、対応するラムダ計算の基本型はオブジェクトであり、項は射である。逆に、基本型のコレクションと与えられた項上の積型とペアリング演算子を備えた単純型ラムダ計算は、型をオブジェクトとし、射を項の同値類とするCCCを形成する。 ${\displaystyle \beta \eta }$

対句、射影、単位項には型付け規則があります。2つの項 と が与えられた場合、項は型を持ちます。同様に、項がある場合、項 と が存在し、これらは直積の射影に対応します。型1の単位項は と書き、発音は「nil」で、最終的なオブジェクトです。方程式理論も同様に拡張され、 ${\displaystyle s{\mathbin {:}}\sigma }$ ${\displaystyle t{\mathbin {:}}\tau }$ ${\displaystyle (s,t)}$ ${\displaystyle \sigma \times \tau }$ ${\displaystyle u{\mathbin {:}}\tau _{1}\times \tau _{2}}$ ${\displaystyle \pi _{1}(u){\mathbin {:}}\tau _{1}}$ ${\displaystyle \pi _{2}(u){\mathbin {:}}\tau _{2}}$ ${\displaystyle \pi _{i}}$ ${\displaystyle ()}$

${\displaystyle \pi _{1}(s{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )=s{\mathbin {:}}\sigma }$

${\displaystyle \pi _{2}(s{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )=t{\mathbin {:}}\tau }$

${\displaystyle (\pi _{1}(u{\mathbin {:}}\sigma \times \tau ),\pi _{2}(u{\mathbin {:}}\sigma \times \tau ))=u{\mathbin {:}}\sigma \times \tau }$

${\displaystyle t{\mathbin {:}}1=()}$

この最後は、「 t がタイプ 1 の場合、 nil に減少します」と読みます。

上記は、型をオブジェクトとしてとることでカテゴリに変換できます。射は、x が変数（型⁠ ⁠）であり、tが項（型⁠ ⁠ ）であるペアの同値類です。項には、（任意選択で） xを除いて自由変数は含まれません。言語における項の集合は、この項の集合を抽象化と適用の操作によって閉包したものです。 ${\displaystyle \sigma \to \tau }$ ${\displaystyle (x{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )}$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$

この対応は、カルティシアン閉カテゴリのカテゴリと単純型付きラムダ理論のカテゴリ間の 「言語準同型」と関数を含むように拡張できます。

この対応の一部は、線形型システムを使用することで、閉じた対称モノイドカテゴリに拡張できます。

証明理論的意味論

単純型付きラムダ計算は、カリー・ハワード同型性を介して、命題直観論理の含意部分、すなわち含意命題計算と密接に関連しています。つまり、項は自然演繹の証明に正確に対応し、存在する型はまさにこの論理の トートロジーです。

^{チャーチ（1940 ）[ 1 ]} p.58はロジスティック法から公理図式^{[ 1 ]} p.60を構築し、ヘンキン（1949） ^{[ 3 ]}はこれに型領域（例えば自然数、実数など）を付与した。ヘンキン（1996）p.146はチャーチのロジスティック法がモデル理論を介して数学（ペアノ算術と実解析） ^{[ 4 ]}の基礎を提供しようとしたことを説明した。

代替構文

上記の説明は、単純型付きラムダ計算の構文を定義する唯一の方法ではありません。1 つの代替案は、型注釈を完全に削除して（構文が型なしラムダ計算と同じになるように）、項がHindley–Milner 型推論によって適切に型付けされていることを保証することです。推論アルゴリズムは停止性があり、健全で、完全です。項が型付け可能である場合は常に、アルゴリズムはその型を計算します。より正確には、項の主型を計算します。これは、注釈のない項（ ⁠ ⁠${\displaystyle \lambda x.~x}$ など）が複数の型（⁠ ⁠${\displaystyle {\mathtt {int}}\to {\mathtt {int}}}$ 、⁠ ⁠${\displaystyle {\mathtt {bool}}\to {\mathtt {bool}}}$ など、すべて主型⁠ ⁠${\displaystyle \alpha \to \alpha }$ のインスタンス）を持つことが多いためです。

単純型ラムダ計算のもう一つの表現は、双方向型チェックに基づいています。これは、Hindley-Milner推論よりも多くの型注釈を必要としますが、記述はより容易です。型システムは、それぞれ記述されたチェックと合成の両方を表す2つの判断に分かれています。操作的には、3つの要素、、、はすべてチェック判断への入力ですが、合成判断はとのみを入力として受け取り、型を出力として生成します。これらの判断は、以下の規則によって導出されます。 ${\displaystyle \Gamma \vdash e\Leftarrow \tau }$ ${\displaystyle \Gamma \vdash e\Rightarrow \tau }$ ${\displaystyle \Gamma }$ ${\displaystyle e}$ ${\displaystyle \tau }$ ${\displaystyle \Gamma \vdash e\Leftarrow \tau }$ ${\displaystyle \Gamma \vdash e\Rightarrow \tau }$ ${\displaystyle \Gamma }$ ${\displaystyle e}$ ${\displaystyle \tau }$

${\displaystyle {\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x\Rightarrow \sigma }}}$ [1]	${\displaystyle {\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c\Rightarrow T}}}$ [2]
${\displaystyle {\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e\Leftarrow \tau }{\Gamma \vdash \lambda x.~e\Leftarrow \sigma \to \tau }}}$ [3]	${\displaystyle {\frac {\Gamma \vdash e_{1}\Rightarrow \sigma \to \tau \quad \Gamma \vdash e_{2}\Leftarrow \sigma }{\Gamma \vdash e_{1}~e_{2}\Rightarrow \tau }}}$ [4]
${\displaystyle {\frac {\Gamma \vdash e\Rightarrow \tau }{\Gamma \vdash e\Leftarrow \tau }}}$ [5]	${\displaystyle {\frac {\Gamma \vdash e\Leftarrow \tau }{\Gamma \vdash (e{\mathbin {:}}\tau )\Rightarrow \tau }}}$ [6]

ルール[1]～[4]は、チェック判定と統合判定の慎重な選択を除けば、上記のルール(1)～(4)とほぼ同じであることに注目してください。これらの選択は次のように説明できます。

1. がコンテキスト内にある場合、 ⁠ ⁠の型を合成できます。${\displaystyle x{\mathbin {:}}\sigma }$ ${\displaystyle \sigma }$ ${\displaystyle x}$
2. 項定数の型は固定されており、合成することができます。
3. あるコンテキストでが型を持つことを確認するには、 でコンテキストを拡張し、 が型⁠ ⁠を持つことを確認します。${\displaystyle \lambda x.~e}$ ${\displaystyle \sigma \to \tau }$ ${\displaystyle x{\mathbin {:}}\sigma }$ ${\displaystyle e}$ ${\displaystyle \tau }$
4. 型を（何らかのコンテキストで）合成し、型と照合する場合（同じコンテキストで）、型⁠ ⁠を合成します。${\displaystyle e_{1}}$ ${\displaystyle \sigma \to \tau }$ ${\displaystyle e_{2}}$ ${\displaystyle \sigma }$ ${\displaystyle e_{1}~e_{2}}$ ${\displaystyle \tau }$

合成規則は上から下へ読み進むのに対し、検査規則は下から上へ読み進むことに注意してください。特に、規則[3]のラムダ抽象化については注釈を付ける必要がないことに注意してください。これは、関数を検査する型から、束縛変数の型を推論できるためです。最後に、規則[5]と[6]について以下のように説明します。

5. が型⁠ ⁠であることを確認するには、型⁠ ⁠を合成するだけで十分です。${\displaystyle e}$ ${\displaystyle \tau }$ ${\displaystyle \tau }$
6. 型⁠ ⁠に対してチェックする場合、明示的に注釈が付けられた用語は⁠ ⁠を合成します。 ${\displaystyle e}$ ${\displaystyle \tau }$ ${\displaystyle (e{\mathbin {:}}\tau )}$ ${\displaystyle \tau }$

最後の2つの規則は合成とチェックを強制するため、型付けは適切だが注釈が付いていない項は、十分な型注釈を挿入すれば双方向システムでチェックできることは容易に理解できます。実際、注釈はβ-redex でのみ必要です。

一般的な観察

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

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

重要な結果

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

注記

1. アロンゾ・チャーチ(1956)数学論理入門pp.47-68 ^{[ 2 ]}
2. Church 1940, p.57では、変数の型を下付き文字で表している: ^{[ 1 ]}${\displaystyle a_{\alpha },b_{\alpha },...z_{\alpha },...{\bar {a}}_{\alpha },{\bar {b}}_{\alpha },...{\bar {z}}_{\alpha },...}$
3. Church 1940, p.57: 2番目と3番目の基本記号（）はスコープを表す: ^{[ 1 ]}${\displaystyle \lambda ,(,),N_{oo},A_{ooo},\Pi _{o(o\alpha )},\iota _{\alpha (o\alpha )}}$
4. Church 1940, p.60:はそれぞれ否定、選言、全称量化、選択を表す4つの定数です。^{[ 1 ]}${\displaystyle N_{oo},A_{ooo},\Pi _{o(o\alpha )},\iota _{\alpha (o\alpha )}}$
5. 教会 1940 年、p.59 ^{[ 1 ]} ヘンキン 1949 年、p.160; ^{[ 3 ]}ヘンキン 1996 p.144 ^{[ 4 ]}
6. チャーチ 1940, p.57 ^{[ 1 ]}
7. Church 1940 p.58には24の省略された式が記載されている。 ^{[ 1 ]}
8. この記事では、以下の4つのタイピング判断を言葉で示しています。タイピング環境です。 ^{[ 5 ]}${\displaystyle \Gamma }$
9. 「 ⁠ ⁠${\displaystyle =_{\beta }}$ 」は、式 u を x に置き換えた結果を t の形式で生成するプロセスを表します。
10. 「 ⁠ ⁠${\displaystyle =_{\eta }}$ 」は、x に適用された形式 t の展開を生成するプロセスを示します。

1. Church, Alonzo (1940年6月). 「単純な型理論の定式化」(PDF) . Journal of Symbolic Logic . 5 (2): 56– 68. doi : 10.2307/2266170 . JSTOR  2266170. S2CID 15889861. 2019年1月12日時点 のオリジナル(PDF)からのアーカイブ。
2. チャーチ、アロンゾ（1956）『数理論理学入門』
3. レオン・ヘンキン（1949年9月）「一階関数微積分の完全性」 p.160
4. レオン・ヘンキン（1996年6月）「私の完全性証明の発見」
5. 快楽主義的学習：楽しみのために学ぶ（最終更新日：2021年11月25日 14:00 UTC）タイピング判断を理解する
6. Pfenning, Fr​​ank, Church and Curry: Combining Intrinsic and Extrinsic Typing (PDF)、p. 1 、 2022年2月26日閲覧
7. カリー、ハスケルB (1934-09-20). 「組合せ論理における機能性」 .米国科学アカデミー紀要. 20 (11): 584–90 . Bibcode : 1934PNAS...20..584C . doi : 10.1073/ pnas.20.11.584 . ISSN 0027-8424 . PMC 1076489. PMID 16577644 .   （外部型の組み合わせ論理を提示し、後に他の人によってラムダ計算に適応された）^{[ 6 ]}
8. レイノルズ, ジョン(1998). 『プログラミング言語の理論』 ケンブリッジ大学出版局, イギリス. pp. 327, 334. ISBN 9780521594141。
9. ノーマン・ラムゼイ（2019年春）ラムダ計算の縮約戦略
10. Tait, WW (1967年8月). 「有限型関数の内包的解釈I」 . The Journal of Symbolic Logic . 32 ( 2): 198– 212. doi : 10.2307/2271658 . ISSN 0022-4812 . JSTOR 2271658. S2CID 9569863 .   
11. Lambek, J. (1986). 「カルティシアン閉圏と型付きλ計算」 .結合子と関数型プログラミング言語. コンピュータサイエンス講義ノート. 第242巻. Springer. pp.  136– 175. doi : 10.1007/3-540-17184-3_44 . ISBN 978-3-540-47253-7。
12. スタットマン、リチャード（1979年7月1日）「型付きλ計算は初等再帰的ではない」理論計算機科学誌、9 (1): 73– 81. doi : 10.1016/0304-3975(79)90007-0 . hdl : 2027.42/23535 . ISSN 0304-3975 . 
13. メアソン, ハリー G. (1992年9月14日). 「スタットマン定理の簡単な証明」.理論計算機科学. 103 (2): 387– 394. doi : 10.1016/0304-3975(92)90020-G . ISSN 0304-3975 . 
14. スタットマン、リチャード（1979年7月）「型付きλ計算は初等再帰的ではない」理論計算機科学誌、9 (1): 73– 81. doi : 10.1016/0304-3975(79)90007-0 . hdl : 2027.42/23535 . ISSN 0304-3975 . 
15. Berger, U.; Schwichtenberg, H. (1991年7月). 「型付きラムダ計算における評価関数の逆」 . [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science . pp.  203– 211. doi : 10.1109/LICS.1991.151645 . ISBN 0-8186-2230-X. S2CID  40441974 .
16. Huet, Gérard P. (1973年4月1日). 「三階述語論理における統一の決定不可能性」. Information and Control . 22 (3): 257– 267. doi : 10.1016/S0019-9958(73)90301-X . ISSN 0019-9958 . 
17. Baxter, Lewis D. (1978年8月1日). 「三次二項統一問題の決定不可能性」 .情報制御. 38 (2): 170–178 . doi : 10.1016/S0019-9958(78)90172-9 . ISSN 0019-9958 . 
18. Goldfarb, Warren D. (1981年1月1日). 「第二階統一問題の決定不可能性」.理論計算機科学. 13 (2): 225– 230. doi : 10.1016/0304-3975(81)90040-2 . ISSN 0304-3975 . 
19. スターリング、コリン (2009年7月22日). 「高階マッチングの決定可能性」.論理的手法コンピュータサイエンス. 5 (3) 757: 1– 52. arXiv : 0907.3804 . doi : 10.2168/LMCS-5(3:2)2009 . S2CID 1478837 . 
20. シュヴィヒテンベルク、ヘルムート (1975 年 9 月 1 日)。"Definierbare Funktionen imλ-Kalkül mit Typen"。Archiv für mathematische Logik und Grundlagenforschung (ドイツ語)。17 (3): 113–114。土井: 10.1007/BF02276799。ISSN 1432-0665。S2CID 11598130。  
21. フリードマン、ハーヴェイ (1975). 「関数間の等式」 .論理コロキウム. 数学講義ノート. 第453巻. シュプリンガー. pp.  22– 37. doi : 10.1007/BFb0064870 . ISBN 978-3-540-07155-6。
22. スタットマン、R. (1983 年 12 月 1 日)。「-定義可能な関数と変換」。数学ロジックとグルンドラーゲンフォルシュングのアーカイブ。23 (1): 21–26 .土井: 10.1007/BF02023009。ISSN 1432-0665。S2CID 33920306。${\displaystyle \lambda }$ ${\displaystyle \beta \eta }$   
23. Plotkin, GD (1973).ラムダ定義可能性と論理関係(PDF) (技術レポート). エディンバラ大学. 2022年9月30日閲覧。
24. Jung, Achim; Tiuryn, Jerzy (1993). 「ラムダ定義可能性の新たな特徴づけ」 .型付きラムダ計算とその応用. コンピュータサイエンス講義ノート. 第664巻. Springer. pp.  245– 257. doi : 10.1007/BFb0037110 . ISBN 3-540-56517-5。
25. ローダー、ラルフ (2001). 「λ-定義可能性の決定不可能性」 .論理、意味、そして計算. シュプリンガー・オランダ. pp.  331– 342. doi : 10.1007/978-94-010-0526-5_15 . ISBN 978-94-010-3891-1。

外部リンク

• ローダー、ラルフ（1998年2月）「単純型ラムダ計算に関するノート」
• スタンフォード哲学百科事典の「チャーチのタイプ理論」の項目