型理論

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

文脈が与えられた場合${\displaystyle \Gamma }$⁠そしてタイプ⁠${\displaystyle \tau }$⁠, decide whether there exists a term ⁠${\displaystyle t}$⁠ that can be assigned the type ⁠${\displaystyle \tau }$⁠ in the type environment ⁠${\displaystyle \Gamma }$⁠.

Girard's paradox shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types.

A type theory usually has several rules, including ones to:

• create a judgment (known as a context in this case)
• add an assumption to the context (context weakening)
• rearrange the assumptions
• use an assumption to create a variable
• define reflexivity, symmetry and transitivity for judgmental equality
• define substitution for application of lambda terms
• list all the interactions of equality, such as substitution
• define a hierarchy of type universes
• assert the existence of new types

Also, for each "by rule" type, there are 4 different kinds of rules:

• "type formation" rules say how to create the type
• "term introduction" rules define the canonical terms and constructor functions, like "pair" and "S".
• "term elimination" rules define the other functions like "first", "second", and "R".
• "computation" rules specify how computation is performed with the type-specific functions.

For examples of rules, an interested reader may follow Appendix A.2 of the Homotopy Type Theory book,^[15] or read Martin-Löf's Intuitionistic Type Theory.^[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}$⁠ .

Two common type dependences, dependent product and dependent sum types, allow for the theory to encode BHK intuitionistic logic by acting as equivalents to universal and existential quantification; this is formalized by Curry–Howard correspondence.^[26] As they also connect to products and sums in set theory, they are often written with the symbols ${\displaystyle \Pi }$ and ⁠${\displaystyle \Sigma }$⁠, respectively.

Sum types are seen in dependent pairs, where the second type depends on the value of the first term. This arises naturally in computer science where functions may return different types of outputs based on the input. For example, the Boolean type is usually defined with an eliminator function ⁠${\displaystyle \mathrm {if} }$⁠, which takes three arguments and behaves as follows.

• ${\displaystyle \mathrm {if} \,{\texttt {true}}\,x\,y}$ returns ⁠${\displaystyle x}$⁠, and
• ${\displaystyle \mathrm {if} \,{\texttt {false}}\,x\,y}$ returns ⁠${\displaystyle y}$⁠.

Ordinary definitions of ${\displaystyle \mathrm {if} }$ require ${\displaystyle x}$ and ${\displaystyle y}$ to have the same type. If the type theory allows for dependent types, then it is possible to define a dependent type ${\displaystyle x:{\mathsf {bool}}\,\vdash \,\mathrm {TF} \,x:U\to U\to U}$ such that

• ${\displaystyle \mathrm {TF} \,{\texttt {true}}\,\sigma \,\tau }$ returns ⁠${\displaystyle \sigma }$⁠, and
• ${\displaystyle \mathrm {TF} \,{\texttt {false}}\,\sigma \,\tau }$ returns ⁠${\displaystyle \tau }$⁠.

The type of ${\displaystyle \mathrm {if} }$ may then be written as ⁠${\displaystyle \forall \,\sigma \,\tau .\Pi _{x:{\mathsf {bool}}}.\sigma \to \tau \to \mathrm {TF} \,x\,\sigma \,\tau }$⁠.

Following the notion of Curry–Howard Correspondence, the identity type is a type introduced to mirror propositional equivalence, as opposed to the judgmental (syntactic) equivalence that type theory already provides.

An identity type requires two terms of the same type and is written with the symbol ⁠${\displaystyle =}$⁠. For example, if ${\displaystyle x+1}$ and ${\displaystyle 1+x}$ are terms, then ${\displaystyle x+1=1+x}$ is a possible type. Canonical terms are created with a reflexivity function, ⁠${\displaystyle \mathrm {refl} }$⁠. For a term ⁠${\displaystyle t}$⁠, the call ${\displaystyle \mathrm {refl} \,t}$ returns the canonical term inhabiting the type ⁠${\displaystyle t=t}$⁠.

The complexities of equality in type theory make it an active research topic; homotopy type theory is a notable area of research that mainly deals with equality in type theory.

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

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