型理論

一般的に、型理論における証明の望ましい結論は、型占有の結論である。^{[ 17 ]}型占有の決定問題（略称は⁠${\displaystyle \exists t.\Gamma \vdash t:\tau$ ?} ⁠ ) は:

文脈が与えられた場合${\displaystyle \Gamma }$⁠そしてタイプ⁠${\displaystyle \tau }$⁠、項が存在するかどうかを判断する⁠${\displaystyle t}$型を割り当てることができる${\displaystyle \tau }$型環境において${\displaystyle \Gamma }$⁠ .

ジラールのパラドックスは、型の占有が、カリー・ハワード対応との整合性に強く関連していることを示している。健全なシステムであるためには、占有されていない型が存在しなければならない。

型理論には通常、以下のような規則がいくつか含まれます。

• 判断（この場合は文脈と呼ばれる）を作成する
• 文脈に仮定を追加する（文脈の弱化）
• 前提条件を再構成する
• 仮定を用いて変数を作成する
• 判断の平等性における反射性、対称性、推移性を定義する
• ラムダ項の適用における置換を定義する
• 等号のすべての相互作用（代入など）を列挙する
• 型ユニバースの階層を定義する
• 新しいタイプの存在を主張する

また、「ルールによる」タイプごとに、4種類のルールが存在します。

• 「型形成」ルールは、型の作成方法を規定する。
• 「用語導入」ルールは、「pair」や「S」などの標準的な用語とコンストラクタ関数を定義します。
• 「項消去」ルールは、「first」、「second」、「R」などの他の関数を定義します。
• 「計算」ルールは、型固有の関数を用いて計算を実行する方法を規定する。

規則の例については、興味のある読者はホモトピー型理論の書籍の付録A.2を参照するか^{[ 15 ]} 、またはMartin-Löfの直観主義型理論^{[ 18 ]を読むとよい。}

ペル・マルティン＝レーフは、構成的数学の基礎として直観主義型理論を提案した。^{[ 14 ]}構成的数学では、「ある型が存在する」ことを証明する際に、${\displaystyle x}$不動産付き${\displaystyle P(x)}$⁠「、特定の${\displaystyle x}$そしてそれが特性を持っているという証明${\displaystyle P}$型理論では、存在は依存積型を用いて実現され、その証明にはその型の項が必要となる。

非構成的証明の一例として、背理法による証明がある。最初のステップは、${\displaystyle x}$存在しないことを反証する。その段階からの結論は「${\displaystyle x}$存在しない」。最後のステップは、二重否定によって、${\displaystyle x}$存在する。構成的数学では、二重否定を取り除く最後のステップで、${\displaystyle x}$存在する。^{[ 19 ]}

基礎として提案されている型理論のほとんどは構成的であり、証明支援系で使用される型理論のほとんどもこれに該当します。型理論には、規則または仮定によって非構成的な機能を追加することも可能です。これには、現在の継続での呼び出しなどの継続に対する演算子が含まれます。しかし、これらの演算子は、正準性やパラメトリック性といった望ましい特性を損なう傾向があります。

型理論を扱う多くのプログラム（例えば、対話型定理証明器）は、型推論も行います。これにより、ユーザーの操作を最小限に抑えつつ、ユーザーが意図するルールを選択できるようになります。

圏論の当初の動機は基礎主義とはかけ離れていましたが、この2つの分野は深い繋がりがあることが判明しました。ジョン・レーン・ベルが書いているように、「実際、圏自体をある種の型理論と見なすことができます。この事実だけでも、型理論が集合論よりも圏論にずっと密接に関係していることを示しています。」簡単に言うと、圏は対象を型（またはソート[21]）と見なすことで型理論と見なすことができます。つまり、^{「大まかに}言えば、圏は構文を取り除いた型理論と考えることができます。」このようにして、多くの重要な結果が導き出されます。^{[ 22 ]}

• デカルト閉圏は型付きλ計算（ランベック、1970）に対応する。
• C-モノイド（積と指数関数と1つの非終端オブジェクトを持つ圏）は、型付けされていないλ計算（1980年頃にランベックとダナ・スコットによって独立に発見された）に対応する。
• 局所的にデカルト閉圏は、マルティン＝レーフ型の理論に対応する（シーリー、1984）。

カテゴリー論理として知られるこの相互作用は、それ以来活発な研究の対象となっており、例えばジェイコブス（1999）のモノグラフを参照されたい。

ホモトピー型理論は、型理論と圏論を組み合わせようとする試みです。特に型間の等式に焦点を当てています。ホモトピー型理論は、主に等式型の扱い方において直観主義型理論とは異なります。2016年に、正規化を伴うホモトピー型理論である立方体型理論が提案されました。^{[ 23 ] [ 24 ]}

最も基本的な型はアトムと呼ばれ、アトムの型を持つ項はアトム項として知られています。型理論に含まれる一般的なアトム項は自然数であり、多くの場合、型 ⁠ で表記されます。${\displaystyle {\mathsf {nat}}}$⁠、ブール論理値（ ⁠${\displaystyle {\texttt {true}}}$そして​​${\displaystyle {\texttt {false}}}$⁠ )、タイプ⁠で表記${\displaystyle {\mathsf {bool}}}$⁠、および型が異なる可能性のある形式変数。 ^{[ 17 ]}例えば、以下は原子項である可能性があります。

• ${\displaystyle 42:{\mathsf {nat}}}$
• ${\displaystyle {\texttt {true}}:{\mathsf {bool}}}$
• ${\displaystyle x:{\mathsf {nat}}}$
• ${\displaystyle y:{\mathsf {bool}}}$

原子型に加えて、ほとんどの現代の型理論では関数も許容されます。関数型は矢印記号を導入し、帰納的に定義されます。${\displaystyle \sigma }$そして${\displaystyle \tau }$は型であり、表記法は${\displaystyle \sigma \to \tau }$は、型のパラメータを受け取る関数の型です。${\displaystyle \sigma }$そして型⁠の項を返します${\displaystyle \tau }$⁠ . この形式の型は単純型として知られています。 ^{[ 17 ]}

以下の用語のように、一部の用語は単純な型を持つものとして直接宣言できます。${\displaystyle \mathrm {add} }$これは、2 つの自然数を順番に入力として受け取り、1 つの自然数を返します。

${\displaystyle \mathrm {add}$ :{\mathsf {nat}}\to ({\mathsf {nat}}\to {\mathsf {nat}})}

厳密に言えば、単純な型は入力と出力がそれぞれ1つずつしか許されないので、上記の型をより忠実に解釈すると次のようになる。${\displaystyle \mathrm {add} }$自然数を入力として受け取り、次の形式の関数を返す関数です。${\displaystyle {\mathsf {nat}}\to {\mathsf {nat}}}$括弧は、${\displaystyle \mathrm {add} }$タイプがありません${\displaystyle ({\mathsf {nat}}\to {\mathsf {nat}})\to {\mathsf {nat}}}$⁠、これは自然数の関数を受け取り、自然数を返す関数になります。慣例として、矢印は右結合であるため、括弧は省略できます。${\displaystyle \mathrm {add} }$⁠のタイプ。 ^{[ 17 ]}

新しい関数項はラムダ式を用いて構築することができ、ラムダ項と呼ばれます。これらの項は帰納的にも定義されます。ラムダ項は次の形式をとります。${\displaystyle (\lambda v.t)}$⁠、そこで${\displaystyle v}$は形式変数であり、${\displaystyle t}$は用語であり、その型は表記されます。${\displaystyle \sigma \to \tau }$⁠、そこで${\displaystyle \sigma }$は、タイプです。${\displaystyle v}$⁠、そして${\displaystyle \tau }$は、タイプです。${\displaystyle t}$⁠ . ^{[ 17 ]}次のラムダ項は、入力された自然数を2倍にする関数を表します。

${\displaystyle (\lambda x.\mathrm {add} \,x\,x):{\mathsf {nat}}\to {\mathsf {nat}}}$

変数は${\displaystyle x}$そして（ラムダ項の型から暗黙的に）型は でなければならない。${\displaystyle {\mathsf {nat}}}$⁠ . 用語${\displaystyle \mathrm {add} \,x\,x}$タイプがあります⁠${\displaystyle {\mathsf {nat}}}$これは、関数適用推論規則を2回適用することで確認できます。したがって、ラムダ項の型は${\displaystyle {\mathsf {nat}}\to {\mathsf {nat}}}$つまり、これは自然数を引数として受け取り、自然数を返す関数であるということです。

ラムダ項は名前を持たないため、匿名関数です^{[ d ] 。匿名関数の概念は多くのプログラミング言語に見られます。}

型理論の強みは、推論規則によって項をどのように組み合わせることができるかを規定することにある。^{[ 5 ]}関数を持つ型理論には、関数適用の推論規則もある。${\displaystyle t}$タイプの用語です${\displaystyle \sigma \to \tau }$⁠、そして${\displaystyle s}$タイプの用語です${\displaystyle \sigma }$⁠、そして適用${\displaystyle t}$へ​${\displaystyle s}$⁠、しばしば書かれる⁠${\displaystyle (t\,s)}$⁠、タイプがあります⁠${\displaystyle \tau }$例えば、型表記法がわかっている場合${\displaystyle 0:{\textsf {nat}}}$⁠、 ⁠${\displaystyle 1:{\textsf {nat}}}$⁠、そして⁠${\displaystyle 2:{\textsf {nat}}}$⁠ 、すると関数適用から以下の型表記を推論できる。 ^{[ 17 ]}

• ${\displaystyle (\mathrm {add} \,1):{\textsf {nat}}\to {\textsf {nat}}}$
• ${\displaystyle ((\mathrm {add} \,2)\,0):{\textsf {nat}}}$
• ${\displaystyle ((\mathrm {add} \,1)((\mathrm {add} \,2)\,0)):{\textsf {nat}}}$

括弧は演算の順序を示しますが、慣例として関数適用は左結合であるため、適切な場合は括弧を省略できます。^{[ 17 ]}上記の3つの例の場合、最初の2つではすべての括弧を省略でき、3つ目は次のように簡略化できます。${\displaystyle \mathrm {add} \,1\,(\mathrm {add} \,2\,0):{\textsf {nat}}}$⁠ .

ラムダ項を許容する型理論には、推論規則も含まれる。${\displaystyle \beta }$-削減と${\displaystyle \eta }$-還元。これらは関数適用の概念をラムダ項に一般化したものです。記号的には、次のように記述されます。

• ${\displaystyle (\lambda v.t)\,s\rightarrow t[v\colon =s]}$（⁠${\displaystyle \beta }$（削減）。
• ${\displaystyle (\lambda v.t\,v)\rightarrow t}$、 もし${\displaystyle v}$は自由変数ではありません${\displaystyle t}$（⁠${\displaystyle \eta }$（削減）。

最初の簡約では、ラムダ項を評価する方法を説明します。ラムダ式が${\displaystyle (\lambda v.t)}$用語に適用されます${\displaystyle s}$⁠、1 はすべての出現箇所を置き換えます${\displaystyle v}$で${\displaystyle t}$と共に​${\displaystyle s}$⁠。2番目の簡約は、ラムダ式と関数型の間の関係を明確にします。${\displaystyle (\lambda v.t\,v)}$がラムダ項であれば、それは${\displaystyle t}$これは関数項です。なぜなら、これは に適用されているからです。${\displaystyle v}$したがって、ラムダ式は単に と同等です。${\displaystyle t}$⁠、どちらも1つの引数を受け取り、適用します${\displaystyle t}$それに対して。^{[ 5 ]}

例えば、次の用語は${\displaystyle \beta }$削減された。

${\displaystyle (\lambda x.\mathrm {add} \,x\,x)\,2\rightarrow \mathrm {add} \,2\,2}$

型と項の等価性の概念も確立する型理論では、対応する推論規則が存在する。${\displaystyle \beta }$-平等と${\displaystyle \eta }$-平等。^{[ 17 ]}

空の型には項がありません。型は通常次のように記述されます。${\displaystyle \bot }$または⁠${\displaystyle \mathbb {0} }$⁠。空の型の用途の 1 つは、型の占有の証明です。型の場合、${\displaystyle a}$⁠ 、型⁠の関数を導出することは一貫性がある${\displaystyle a\to \bot }$⁠、それから${\displaystyle a}$そこは無人地帯であり、つまり、そこには何の条件も存在しない。

単位型には、正準項がちょうど 1 つあります。型は次のように記述されます。${\displaystyle \top }$または${\displaystyle \mathbb {1} }$そして、唯一の正準項は次のように書かれる。${\displaystyle \ast }$⁠。ユニットタイプは、タイプの居住証明にも使用されます。タイプの場合、${\displaystyle a}$⁠ 、型⁠の関数を導出することは一貫性がある${\displaystyle \top \to a}$⁠、それから${\displaystyle a}$居住されている、つまり、1つ以上の用語を持つ必要がある。

ブール型には、正確に2つの標準項があります。この型は通常次のように記述されます。${\displaystyle {\textsf {bool}}}$または${\displaystyle \mathbb {B} }$または⁠${\displaystyle \mathbb {2} }$⁠。通常、標準的な用語は${\displaystyle \mathrm {true} }$そして​${\displaystyle \mathrm {false} }$⁠ .

自然数は通常、ペアノ算術のスタイルで実装されます。標準的な用語があります。${\displaystyle 0:{\mathsf {nat}}}$ゼロの場合。ゼロより大きい標準値には、後継関数の反復適用を使用します。${\displaystyle \mathrm {S}$ :{\mathsf {nat}}\to {\mathsf {nat}}} ⁠ .

製品タイプ、${\displaystyle \times }$は2つのタイプに依存し、その項は一般的に順序対として表される。${\displaystyle (s,t)}$⁠ . そのペア${\displaystyle (s,t)}$製品タイプ⁠${\displaystyle \sigma \times \tau }$⁠、そこで${\displaystyle \sigma }$は、${\displaystyle s}$そして${\displaystyle \tau }$は、タイプです。${\displaystyle t}$各製品タイプは通常、消去関数で定義されます。${\displaystyle \mathrm {first}$ :\sigma \times \tau \to \sigma } および⁠${\displaystyle \mathrm {second}$ :\sigma \times \tau \to \tau } ⁠。

• ${\displaystyle \mathrm {first} \,(s,t)}$返します${\displaystyle s}$⁠、そして
• ${\displaystyle \mathrm {second} \,(s,t)}$返します${\displaystyle t}$⁠ .

順序対の他に、この型は論理積と論理積の概念にも使用されます。

和型は次のように記述されます。${\displaystyle +}$または⁠${\displaystyle \sqcup }$プログラミング言語では、和型はタグ付き共用体と呼ばれることがあります。各型${\displaystyle \sigma \sqcup \tau }$通常はコンストラクタで定義されます${\displaystyle \mathrm {left}$ :\sigma \to (\sigma \sqcup \tau )} および⁠${\displaystyle \mathrm {right}$ \tau \to (\sigma \sqcup \tau )} ⁠ は単射であり、消去関数で${\displaystyle \mathrm {match}$ :(\sigma \to \rho )\to (\tau \to \rho )\to (\sigma \sqcup \tau )\to \rho } となるように、

• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {left} \,x)}$返します${\displaystyle f\,x}$⁠、そして
• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {right} \,y)}$返します${\displaystyle g\,y}$⁠ .

和型は、論理和と和集合の概念に使用されます。

ポリモーフィズムにより、エリミネータ関数はすべての製品タイプに対して一般的に定義できます。${\displaystyle \mathrm {first}$ :\forall \,\sigma \,\tau .\sigma \times \tau \to \sigma } および⁠${\displaystyle \mathrm {second}$ :\forall \,\sigma \,\tau .\sigma \times \tau \to \tau } ⁠。

• ${\displaystyle \mathrm {first} \,(s,t)}$返します${\displaystyle s}$⁠、そして
• ${\displaystyle \mathrm {second} \,(s,t)}$返します${\displaystyle t}$⁠ .

同様に、和型コンストラクタは、すべての有効な和メンバー型に対して次のように定義できます。${\displaystyle \mathrm {left}$ :\forall \,\sigma \,\tau .\sigma \to (\sigma \sqcup \tau )} および⁠${\displaystyle \mathrm {right}$ :\forall \,\sigma \,\tau .\tau \to (\sigma \sqcup \tau )} ⁠、これらは単射で、消去関数は次のように与えられる。${\displaystyle \mathrm {match}$ :\forall \,\sigma \,\tau \,\rho .(\sigma \to \rho )\to (\tau \to \rho )\to (\sigma \sqcup \tau )\to \rho } が 成り立つ。

• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {left} \,x)}$返します${\displaystyle f\,x}$⁠、そして
• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {right} \,y)}$返します${\displaystyle g\,y}$⁠ .

2つの一般的な型依存性、依存積型と依存和型は、全称量化と存在量化の等価物として機能することで、理論がBHK直観主義論理を符号化することを可能にします。これはカリー・ハワード対応によって形式化されています。^{[ 26 ]}これらは集合論における積と和にも関連しているため、しばしば記号で表されます。${\displaystyle \Pi }$そして​${\displaystyle \Sigma }$それぞれ。

和型は従属ペアで見られ、2番目の型は最初の項の値に依存します。これは、関数が入力に基づいて異なる型の出力を返すことがあるコンピュータサイエンスにおいて自然に発生します。たとえば、ブール型は通常、消去関数で定義されます。${\displaystyle \mathrm {if} }$⁠は 3 つの引数を取り、以下のように動作します。

• ${\displaystyle \mathrm {if} \,{\texttt {true}}\,x\,y}$返します${\displaystyle x}$⁠、そして
• ${\displaystyle \mathrm {if} \,{\texttt {false}}\,x\,y}$返します${\displaystyle y}$⁠ .

一般的な定義${\displaystyle \mathrm {if} }$必要とする${\displaystyle x}$そして${\displaystyle y}$同じ型を持つ。型理論が依存型を許容するならば、依存型を定義することが可能である。${\displaystyle x:{\mathsf {bool}}\,\vdash \,\mathrm {TF} \,x:U\to U\to U}$そのため

• ${\displaystyle \mathrm {TF} \,{\texttt {true}}\,\sigma \,\tau }$返します${\displaystyle \sigma }$⁠、そして
• ${\displaystyle \mathrm {TF} \,{\texttt {false}}\,\sigma \,\tau }$返します${\displaystyle \tau }$⁠ .

種類${\displaystyle \mathrm {if} }$次のように書くことができます。${\displaystyle \forall \,\sigma \,\tau .\Pi _{x:{\mathsf {bool}}}.\sigma \to \tau \to \mathrm {TF} \,x\,\sigma \,\tau }$⁠ .

カリー＝ハワード対応の概念に倣って、アイデンティティ型は、型理論が既に提供している判断的（構文的）等価性とは対照的に、命題的等価性を反映するために導入された型である。

同一性型は、同じ型の2つの項を必要とし、記号 ⁠ で表されます。${\displaystyle =}$例えば、${\displaystyle x+1}$そして${\displaystyle 1+x}$用語は、${\displaystyle x+1=1+x}$は可能なタイプです。正規用語は反射関数で作成されます。${\displaystyle \mathrm {refl} }$⁠。 期間⁠${\displaystyle t}$⁠、呼び出し${\displaystyle \mathrm {refl} \,t}$型に属する正規の用語を返します。${\displaystyle t=t}$⁠ .

型理論における等価性の複雑さは、活発な研究テーマとなっている。ホモトピー型理論は、主に型理論における等価性を扱う注目すべき研究分野である。

帰納型は、多様な型を作成するための一般的なテンプレートです。実際、上記で説明したすべての型、そしてそれ以上の型を、帰納型の規則を用いて定義できます。帰納型を生成する方法としては、帰納再帰と帰納帰納の2つがあります。ラムダ式のみを使用する方法としては、スコット符号化があります。

Rocq（以前はCoqとして知られていた）やLeanなどの証明支援システムの中には、帰納的構成の計算体系に基づいているものがあり、これは帰納型を持つ構成の計算体系である。