直観主義型理論

直観型理論（構成型理論、またはマルティン＝レーフ型理論（MLTT）とも呼ばれる）は、型理論であり、数学の代替的な基礎である。直観型理論は、スウェーデンの数学者で哲学者のペル・マルティン＝レーフによって創始され、1972年に初めて発表された。この型理論には複数のバージョンがあり、マルティン＝レーフは理論の内包的および外延的変種を提案し、初期の非述語的バージョンはジラールのパラドックスによって矛盾していることが示され、述語的バージョンに取って代わられた。しかし、すべてのバージョンは、依存型を使用した構成的論理の中核的な設計を維持している。

デザイン

マルティン＝レーフは、数学的構成主義の原理に基づいて型理論を設計した。構成主義では、存在証明には必ず「証拠」が必要である。したがって、「1000より大きい素数が存在する」という証明には、素数でありかつ1000より大きい特定の数を特定する必要がある。直観主義型理論は、BHK解釈を内部化することでこの設計目標を達成した。その結果として、証明は検証、比較、操作が可能な数学的対象となるという利点がある。

直観主義型理論の型コンストラクタは、論理結合子と1対1の対応関係に従うように構築されています。たとえば、含意と呼ばれる論理結合子（ $A\implies B$ ) は関数の型に対応します ( $A\to B$ この対応関係はカリー・ハワード同型性と呼ばれています。以前の型理論もこの同型性に従っていましたが、マルティン・レーフは依存型を導入することで、それを述語論理に拡張した最初の人物でした。

型理論

型理論は、存在する基本的な対象を記述する、一種の数学的存在論、あるいは基礎理論である。標準的な基礎理論である集合論と数理論理学の組み合わせでは、基本的な対象は集合であり、集合は要素を含む容器である。型理論では、基本的な対象は項であり、それぞれの項はただ一つの型に属する。

直観主義型理論には3つの有限型があり、それらは5つの異なる型構成子を用いて合成されます。集合論とは異なり、型理論はフレーゲの論理体系のような論理体系の上に構築されているわけではありません。そのため、型理論の各機能は、数学と論理の両方の機能として二重の役割を果たします。

0型、1型、2型

有限型は3種類あります。0型は項を含みません。1型は1つの標準項を含みます。2型は2つの標準項を含みます。

0型には項が含まれていないため、空型とも呼ばれます。存在し得ないものを表すために使用されます。また、次のように表記されます。 $\bot$ そして、それは証明不可能なもの（つまり、証明が存在し得ないもの）を表す。結果として、否定はそれに対する関数として定義される。 $\neg A:=A\to \bot$ 。

同様に、1型は1つの標準項を含み、存在を表します。これは単位型とも呼ばれます。

最後に、2型には2つの標準項が含まれます。これは2つの値の間の明確な選択を表します。ブール値には使用されますが、命題には使用されません。

命題は、特定の型によって表現される。例えば、真の命題は型1で表現でき、偽の命題は型0で表現できる。しかし、これらが唯一の命題であると断言することはできない。つまり、直観主義型理論における命題には排中律は成り立たない。

Σ型コンストラクタ

Σ型は順序対を含みます。典型的な順序対（または2タプル）型と同様に、Σ型はデカルト積を記述できます。 $A\times B$ 他の2つのタイプでは、 $A$ そして $B$ 論理的には、そのような順序対には証明が含まれるだろう。 $A$ そして証明 $B$ そのため、次のような表記が見られることがあります。 $A\wedge B$ 。

Σ型は、依存型付けのおかげで、一般的な順序対型よりも強力です。順序対では、2番目の項の型は1番目の項の値に依存することがあります。たとえば、ペアの1番目の項が自然数で、2番目の項の型が1番目の項と同じ長さの実数のシーケンスである場合などです。このような型は次のように記述されます。

$\sum _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)$

集合論の用語を用いると、これはインデックス付きの非交和集合に似ています。通常のデカルト積の場合、第2項の型は第1項の値に依存しません。したがって、デカルト積を記述する型は $\displaystyle {\mathbb {N} }\times {\mathbb {R} }}$ 次のように書かれています。

$\sum _{n{\mathbin {:}}{\mathbb {N} }}{\mathbb {R} }$

最初の項の値、 $n$ は、2番目の項のタイプに依存しない。 ${\mathbb {R} }$ 。

Σ型は、数学で使用されるより長い依存型タプルや、ほとんどのプログラミング言語で使用されるレコードや構造体を構築するために使用できます。依存型3タプルの例としては、2つの整数と、最初の整数が2番目の整数より小さいという証明があり、これは次の型で表されます。

$\sum _{m{\mathbin {:}}{\mathbb {Z} }}{\sum _{n{\mathbin {:}}{\mathbb {Z} }}((m<n)={\text{True}})}$

依存型付けにより、Σ型は存在量化子の役割を果たすことができる。「存在する」という文は、 $n$ タイプの ${\mathbb {N} }$ 、したがって $P(n)$ 「証明されている」は、最初の項目が値である順序対のタイプになります。 $n$ タイプの ${\mathbb {N} }$ そして2番目の項目は証明です $P(n)$ 2 番目の項目のタイプ (証明) に注目してください。 $P(n)$ ) は順序対の最初の部分の値に依存します ( $n$ そのタイプは次のようになります。

$\sum _{n{\mathbin {:}}{\mathbb {N} }}P(n)$

Π型コンストラクタ

Π型は関数を含みます。一般的な関数型と同様に、入力型と出力型で構成されます。ただし、戻り値の型が入力値に依存するという点で、一般的な関数型よりも強力です。型理論における関数は、集合理論における関数とは異なります。集合理論では、引数の値を順序対の集合から検索します。型理論では、引数を項に代入し、その項に対して計算（「還元」）を適用します。

例えば、自然数が与えられた場合に $n$ 、を含むベクトルを返します $n$ 実数は次のように表記されます。

$\prod _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)$

出力型が入力値に依存しない場合、関数型は単に次のように記述されることが多い。 $\to$ 。したがって、 $\displaystyle {\mathbb {N} }\to {\mathbb {R} }}$ これは、自然数から実数への関数のタイプです。このようなΠ型は論理的含意に対応します。論理命題 $A\implies B$ 型に対応します $A\to B$ 、Aの証明を受け取り、Bの証明を返す関数を含む。この型は、より一貫性のある形で次のように記述できる。

$\prod _{a{\mathbin {:}}A}B$

Π型は論理学において全称量化にも用いられる。「すべての $n$ タイプの ${\mathbb {N} }$ 、 $P(n)$ 「証明されている」は関数になります $n$ タイプの ${\mathbb {N} }$ 証明へ $P(n)$ したがって、の値が与えられれば $n$ この関数は、 $P(\,\cdot \,)$ その値に対して保持されます。型は

$\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)$

= 型コンストラクタ

= -型は2つの項から作成されます。 $2+2$ そして $2\cdot 2$ 新しいタイプを作成できます $2+2=2\cdot 2$ この新しいタイプの項は、ペアが同じ標準項に還元されるという証明を表します。したがって、両方とも $2+2$ そして $2\cdot 2$ 標準項を計算する $4$ 次のような項があります $2+2=2\cdot 2$ 直観主義型理論では、=型を導入する方法は反射律によるものだけです。

$\operatorname {refl} {\mathbin {:}}\prod _{a{\mathbin {:}}A}(a=a).$

次のような=型を作成することが可能です。 $1=2$ 用語が同じ標準用語に還元されない場合、その新しいタイプの用語を作成することはできません。実際、用語を作成できたとしても、 $1=2$ 用語を作成できます $\bot$ それを関数に入れると、次の型の関数が生成されます。 $1=2\to \bot$ 。以来 $\ldots \to \bot$ 直観主義型理論では否定をこのように定義します。 $\neg (1=2)$ あるいは、最後に、 $1\neq 2$ 。

証明の等価性は証明論における活発な研究分野であり、ホモトピー型理論やその他の型理論の発展につながっている。

帰納的タイプ

帰納型は、複雑な自己参照型の作成を可能にします。たとえば、自然数の連結リストは、空のリストか、自然数と別の連結リストのペアのいずれかになります。帰納型は、木やグラフなどの無制限の数学的構造を定義するために使用できます。実際、自然数型は帰納型として定義できます。 $0$ または、別の自然数の次の数。

帰納型はゼロなどの新しい定数を定義します $0{\mathbin {:}}{\mathbb {N} }$ そして後継関数 $S{\mathbin {:}}{\mathbb {N} }\to {\mathbb {N} }$ 。以来 $S$ 定義がなく、代入によって評価することもできない用語、例えば $S0$ そして $SSS0$ 自然数の標準項となる。

帰納型に関する証明は帰納法によって可能になります。新しい帰納型にはそれぞれ独自の帰納規則が付属しています。述語を証明するには $P(\,\cdot \,)$ すべての自然数に対して、次の規則を使用します。

$\displaystyle {\operatorname {{\mathbb {N} }-elim} }\,{\mathbin {:}}P(0)\,\to \left(\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)\to P(S(n))\right)\to \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)}$

直観主義型理論における帰納型は、整礎木の型であるW型を用いて定義される。その後の型理論の研究により、より複雑な自己参照性を持つ型を扱うために、共帰納型、帰納再帰、帰納帰納といった概念が生み出された。高次の帰納型では、項間の等価性を定義することができる。

宇宙の種類

宇宙型を使用すると、他の型コンストラクタで作成されたすべての型について証明を記述できます。宇宙型内のすべての項 ${\mathcal {U}}_{0}$ 任意の組み合わせで作成された型にマッピングできます $0,1,2,\Sigma ,\Pi ,=,$ そして帰納型コンストラクタ。ただし、パラドックスを避けるために、項はありません。 ${\mathcal {U}}_{n}$ それは以下に対応する ${\mathcal {U}}_{n}$ いかなる場合でも $\displaystyle {\mathcal {n}}\in \mathbb {N} }$ [ ¹^]

すべての「小さな型」と ${\mathcal {U}}_{0}$ 使用する必要があります ${\mathcal {U}}_{1}$ これには、 ${\mathcal {U}}_{0}$ しかし、それ自体のためではない ${\mathcal {U}}_{1}$ 同様に、 ${\mathcal {U}}_{2}$ 宇宙には述語的階層が存在するので、任意の固定定数に対する証明を定量化するには $k$ 宇宙では、 ${\mathcal {U}}_{k+1}$ 。

宇宙型は型理論における厄介な特徴の一つである。マルティン＝レーフのオリジナルの型理論は、ジラールのパラドックスを説明するために変更を余儀なくされた。その後の研究では、「超宇宙」、「マロー宇宙」、非述語的宇宙といったテーマが取り上げられた。

判決

直観主義型理論の正式な定義は、判断を用いて記述される。例えば、「もし $A$ はタイプであり、 $B$ それはタイプです $\textstyle \sum _{a:A}B$ 「型である」という表現には、「型である」、「かつ」、「もし…ならば…」という判断があります。 $\textstyle \sum _{a:A}B$ これは判断ではなく、定義される種類のことである。

型理論のこの第2レベルは、特に等価性に関しては混乱を招く可能性があります。項の等価性に関する判断があり、それは次のように述べるかもしれません。 $4=2+2$ これは、2 つの項が同じ標準項に還元されるという記述です。また、型の等価性に関する判断もあります。 $A=B$ つまり、 $A$ は、次のタイプの要素です。 $B$ そしてその逆もまた然り。型レベルでは、型が存在する。 $4=2+2$ そして、証明があれば、それは用語を含みます。 $4$ そして $2+2$ 同じ値に減らす。（このタイプの項は項等価性判定を使用して生成されます。）最後に、英語には「four」という単語と記号「 $4$ 正典用語を参照する $SSSS0$ マーティン＝レーフによれば、このような同義語は「定義的に等しい」と表現される。

以下の判決の説明は、Nordström、Petersson、およびSmithの議論に基づいています。

形式理論は型とオブジェクトを扱う。

型は次のように宣言されます。

$A\ {\mathsf {タイプ}}$

オブジェクトが存在し、かつ型に属している条件は以下のとおりです。

$a{\mathbin {:}}A$

物体は等しい

$a=b$

型は等しい

$A=B$

別の型のオブジェクトに依存する型は宣言されます

$(x{\mathbin {:}}A)B$

代用により削除

$B[x/a]$ 変数を置き換える $x$ 対象物と共に $a$ で $B$ 。

別の型のオブジェクトに依存するオブジェクトは、2 つの方法で作成できます。オブジェクトが「抽象化」されている場合は、次のように記述します。

$[x]b$

代用により削除

$b[x/a]$ 変数を置き換える $x$ 対象物と共に $a$ で $b$ 。

オブジェクトに依存するオブジェクトは、再帰型の一部として定数として宣言することもできます。再帰型の例は次のとおりです。

$0{\mathbin {:}}\mathbb {N}$
$S{\mathbin {:}}\mathbb {N} \to \mathbb {N}$

ここ、 $S$ は、オブジェクトに依存する定数です。抽象化とは関連付けられていません。 $S$ 等価性を定義することで削除できます。ここでは、加算との関係は等価性を使用して定義され、パターンマッチングを使用して再帰的な側面を処理します。 $S$ :

{\begin{aligned}\operatorname {add} &{\mathbin {:}}\ (\mathbb {N} \times \mathbb {N} )\to \mathbb {N} \\\operatorname {add} (0,b)&=b\\\operatorname {add} (S(a),b)&=S(\operatorname {add} (a,b)))\end{aligned}}

$S$ 不透明な定数として扱われるため、置換のための内部構造は持ちません。

つまり、理論においては、対象、型、そしてこれらの関係を用いて数式を表現する。既存の対象、型、関係から新たな対象、型、関係を生み出すために、以下の判断様式が用いられる。

慣例として、他のすべての型を表す型があります。それは ${\mathcal {U}}$ （または $\operatorname {Set}$ ）。以来 ${\mathcal {U}}$ これは型であり、そのメンバーはオブジェクトです。依存型があります。 $\operatorname {El}$ 各オブジェクトを対応する型にマッピングします。ほとんどのテキストでは $\operatorname {El}$ は決して書かれません。文の文脈から、読者はほぼ常に、 $A$ 型を参照しているか、またはオブジェクトを参照しているか ${\mathcal {U}}$ そのタイプに対応するもの。

これが理論の完全な基礎であり、その他すべてはそこから派生したものである。

論理を実装するために、各命題には独自の型が割り当てられます。これらの型のオブジェクトは、命題を証明するさまざまな方法を表します。命題の証明がない場合、その型にはオブジェクトがありません。命題に対して作用する「and」や「or」などの演算子は、新しい型と新しいオブジェクトを導入します。したがって $A\times B$ 型によって異なる型です $A$ そしてその種類 $B$ その依存型のオブジェクトは、すべてのオブジェクトのペアに対して存在すると定義されています。 $A$ そして $B$ どちらか $A$ または $B$ 証明がなく、空の型である場合、新しい型は $A\times B$ これも空です。

これは、他の型（ブール値、自然数など）とその演算子についても同様に行うことができます。

型理論のカテゴリーモデル

圏論の言語を用いて、RAG Seely は型理論の基本モデルとして局所的にデカルト閉圏(LCCC)の概念を導入した。これは、Cartmell の以前の研究に基づいて、Hofmann と Dybjer によって「族を持つ圏」または「属性を持つ圏」へと改良された。^{[ 2 ]}

外延的対内在的

根本的な違いは、外延型理論と内包型理論です。外延型理論では、定義的（つまり計算的）等価性と命題的等価性は区別されず、命題的等価性には証明が必要です。結果として、外延型理論では、理論内のプログラムが終了しない可能性があるため、型チェックは決定不能になります。たとえば、このような理論では、 Yコンビネータに型を与えることができます。この詳細な例は、NordstömとPeterssonの「Martin-Löfの型理論におけるプログラミング」^{[ 3 ]}に記載されています。しかし、これは外延型理論が実用的なツールの基盤となることを妨げるものではありません。たとえば、Nuprlは外延型理論に基づいています。

対照的に、内包型理論では型チェックは決定可能ですが、内包推論では集合または同様の構成を使用する必要があるため、標準的な数学的概念の表現はやや扱いにくくなります。整数、有理数、実数など、これなしでは扱いにくい、または表現できない一般的な数学的対象が多数あります。整数と有理数は集合なしでも表現できますが、この表現は扱いにくいです。コーシー実数はこれなしでは表現できません。^{[ 4 ]}

ホモトピー型理論はこの問題を解決するために用いられます。この理論では、より高次の帰納型を定義することができ、それによって一階コンストラクタ（値や点）だけでなく、より高次のコンストラクタ、すなわち要素間の等式（パス）、等式間の等式（ホモトピー）などを無限に定義することができます。

型理論の実装

さまざまな形式の型理論が、多くの証明支援システムの基盤となる形式システムとして実装されています。その多くはPer Martin-Löfのアイデアに基づいていますが、多くのシステムには機能の追加、公理の増加、または異なる哲学的背景があります。たとえば、Nuprlシステムは計算型理論^{[ 5 ]}に基づいており、Rocqは（共）帰納的構成の計算に基づいています。依存型は、 ATS、Cayenne、Epigram、Agda ^[⁶^]、Idris ^[⁷^]などのプログラミング言語の設計にも使用されています。

マルティン＝レーフ型理論

Per Martin-Löf は、さまざまな時期に発表されたいくつかの型理論を構築しました。その中には、その説明が記載されたプレプリントが専門家 ( Jean-Yves Girardや Giovanni Sambin など) に入手可能になった時期よりもずっと後に発表されたものもありました。以下のリストは、印刷された形で説明されたすべての理論を列挙し、それらを区別する主要な特徴を概説しようとするものです。これらの理論はすべて、依存積、依存和、非交和、有限型、自然数を持っていました。依存積または依存和の η 還元を含まない同じ還元規則を持っていましたが、依存積の η 還元が追加されている MLTT79 だけは例外です。

MLTT71は、ペル・マルティン＝レーフによって最初に作成された型理論である。1971年にプレプリントとして発表された。この理論は1つの宇宙を持っていたが、その宇宙自体に名前がついており、つまり、今日でいうところの「型の中に型がある」型理論であった。ジャン＝イヴ・ジラールはこのシステムに矛盾があることを示し、プレプリントは出版されることはなかった。

MLTT72 は1972 年のプレプリントで発表され、現在は出版されている。^{[ 8 ]}この理論は、1 つの宇宙 V と、同一性型(=-型)を持たないものを持っていた。宇宙は、V に含まれるオブジェクトの族と、V に含まれないオブジェクト (例えば V 自体) との従属積が、V に含まれるとは想定されないという意味で、「述語的」であった。宇宙は、ラッセルのプリンキピア・マテマティカに倣ったもので、つまり、「 T∈V」と「t∈T」を直接記述し (Martin-Löf は現代の「:」の代わりに「∈」記号を使用)、「El」などの追加のコンストラクタは不要であった。

MLTT73 はPer Martin-Löf が発表した最初の型理論の定義です (Logic Colloquium '73 で発表され、1975 年に出版されました^{[ 9 ]} )。彼はこれを「命題」と説明していますが、命題と他の型との間に明確な区別が導入されていないため、その意味は不明です。後に J 消去法と呼ばれるようになるものがありますが、まだ名前がありません ( 94-95 ページを参照)。この理論には、無限の宇宙列 V ₀、 ...、 V _n、 ...があります。宇宙は Russell のように述語的で、非累積的です。実際、 115 ページの系 3.10 では、A∈V _mと B∈V _nが A と B が変換可能であるならば、 m = nであると述べられています。

MLTT79 は1979 年に発表され、1982 年に出版されました。^{[ 10 ]}この論文で、マルティン・レーフは、依存型理論の 4 つの基本的な判断タイプを紹介しました。これは、その後、このようなシステムのメタ理論の研究において基礎的なものとなりました。彼はまた、文脈を独立した概念として導入しました (p. 161 を参照)。J 除去子 (MLTT73 にすでに登場しましたが、この名前はありませんでした) を持つ同一型があり、理論を「外延的」にする規則も存在します (p. 169)。W タイプがあります。累積的な 述語宇宙の無限のシーケンスがあります。

ビブリオポリス：1984年のビブリオポリスの本^{[ 11 ]}には型理論についての議論があるが、それはやや漠然としており、特定の選択肢のセットを表しているようには見えないため、それに関連付けられた特定の型理論はない。

注記

↑ Bertot, Yves; Castéran, Pierre (2004). Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions . Texts in theoretical computer science. Berlin Heidelberg: Springer. ISBN 978-3-540-20854-9。
↑ Clairambault, Pierre; Dybjer, Peter (2014). "局所的にデカルト閉圏と Martin-Löf 型理論の双同値性" . Mathematical Structures in Computer Science . 24 (6). arXiv : 1112.3456 . doi : 10.1017/S0960129513000881 . ISSN 0960-1295 . S2CID 416274 .
↑ベングト・ノードストローム。ケント・ピーターソン。ジャン・M・スミス (1990)。 Martin-Löf の型理論におけるプログラミング。オックスフォード大学出版局、p. 90.
↑ Altenkirch, Thorsten; Anberrée, Thomas; Li, Nuo.型理論における定義可能な商(PDF) (レポート)。 2024年4月19日にオリジナル(PDF)からアーカイブされました。
↑ Allen, SF; Bickford, M.; Constable, RL; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E. (2006). "Innovations in computational type theory using Nuprl" . Journal of Applied Logic . 4 (4): 428– 469. doi : 10.1016/j.jal.2005.10.005 .
↑ Norell, Ulf (2009). "Agdaにおける依存型プログラミング".第4回言語設計と実装における型に関する国際ワークショップ議事録. TLDI '09. ニューヨーク州ニューヨーク、米国: ACM. pp. 1–2 . CiteSeerX 10.1.1.163.7149 . doi : 10.1145/1481861.1481862 . ISBN 9781605584201. S2CID 1777213 .
↑ Brady, Edwin (2013). "Idris、汎用依存型プログラミング言語：設計と実装" . Journal of Functional Programming . 23 (5): 552– 593. doi : 10.1017/S095679681300018X . ISSN 0956-7968 . S2CID 19895964 .
↑ Martin-Löf, Per (1998). An intuitionistic theory of types, Twenty-five years of constructive type theory (Venice,1995) . Oxford Logic Guides. Vol. 36. New York: Oxford University Press. pp. 127–172 .
↑ Martin-Löf, Per (1975). 「直観主義的型の理論：述語部分」. Studies in Logic and the Foundations of Mathematics . Logic Colloquium '73 (Bristol, 1973). Vol. 80. Amsterdam: North-Holland. pp. 73–118 .
↑ Martin-Löf, Per (1982). 「構成的数学とコンピュータプログラミング」.論理学と数学の基礎に関する研究. 論理学、方法論、科学哲学、VI (ハノーバー、1979)。第104巻。アムステルダム：North-Holland。pp. 153–175。
↑ Martin-Löf, Per (1984).直観主義型理論、証明理論研究（Giovanni Sambin による講義ノート）。第1 巻。Bibliopolis。pp. iv, 91。

参考文献

Martin-Löf, ペル州;サンビン、ジョバンニ (1984)。直観主義的タイプ理論(PDF)。ナポリ：ビブリオポリス。ISBN 978-8870881059. OCLC 12731401 .

さらに読む

Martin-Löf のノートによると、Giovanni Sambin が記録 (1980 年)
ノードストローム、ベングト。ケント州ピーターソン。スミス、ヤン・M. (1990)。Martin-Löf の型理論におけるプログラミング。オックスフォード大学出版局。ISBN 9780198538141。
トンプソン、サイモン（1991）。型理論と関数型プログラミング。アディソン・ウェスリー。ISBN 0-201-41667-0。
グランストロム、ヨハン G. (2011)。直観主義的型理論に関する論文。スプリンガー。ISBN 978-94-007-1735-0。

外部リンク

EU型プロジェクト：チュートリアル– 2005年型サマースクールの講義ノートとスライド
n-カテゴリ - 定義の概略-ジョン・バエズとジェームズ・ドーランからロス・ストリートへの手紙、1995年11月29日

[1] Bertot, Yves; Castéran, Pierre (2004). Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions . Texts in theoretical computer science. Berlin Heidelberg: Springer. ISBN 978-3-540-20854-9。

[2] Clairambault, Pierre; Dybjer, Peter (2014). "局所的にデカルト閉圏と Martin-Löf 型理論の双同値性" . Mathematical Structures in Computer Science . 24 (6). arXiv : 1112.3456 . doi : 10.1017/S0960129513000881 . ISSN 0960-1295 . S2CID 416274 .

[3] ベングト・ノードストローム。ケント・ピーターソン。ジャン・M・スミス (1990)。 Martin-Löf の型理論におけるプログラミング。オックスフォード大学出版局、p. 90.

[4] Altenkirch, Thorsten; Anberrée, Thomas; Li, Nuo.型理論における定義可能な商(PDF) (レポート)。 2024年4月19日にオリジナル(PDF)からアーカイブされました。

[5] Allen, SF; Bickford, M.; Constable, RL; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E. (2006). "Innovations in computational type theory using Nuprl" . Journal of Applied Logic . 4 (4): 428– 469. doi : 10.1016/j.jal.2005.10.005 .

[6] Norell, Ulf (2009). "Agdaにおける依存型プログラミング".第4回言語設計と実装における型に関する国際ワークショップ議事録. TLDI '09. ニューヨーク州ニューヨーク、米国: ACM. pp. 1–2 . CiteSeerX 10.1.1.163.7149 . doi : 10.1145/1481861.1481862 . ISBN 9781605584201. S2CID 1777213 .

[7] Brady, Edwin (2013). "Idris、汎用依存型プログラミング言語：設計と実装" . Journal of Functional Programming . 23 (5): 552– 593. doi : 10.1017/S095679681300018X . ISSN 0956-7968 . S2CID 19895964 .

[8] Martin-Löf, Per (1998). An intuitionistic theory of types, Twenty-five years of constructive type theory (Venice,1995) . Oxford Logic Guides. Vol. 36. New York: Oxford University Press. pp. 127–172 .

[9] Martin-Löf, Per (1975). 「直観主義的型の理論：述語部分」. Studies in Logic and the Foundations of Mathematics . Logic Colloquium '73 (Bristol, 1973). Vol. 80. Amsterdam: North-Holland. pp. 73–118 .

[10] Martin-Löf, Per (1982). 「構成的数学とコンピュータプログラミング」.論理学と数学の基礎に関する研究. 論理学、方法論、科学哲学、VI (ハノーバー、1979)。第104巻。アムステルダム：North-Holland。pp. 153–175。

[MartinLöf1984-11] Martin-Löf, Per (1984).直観主義型理論、証明理論研究（Giovanni Sambin による講義ノート）。第1 巻。Bibliopolis。pp. iv, 91。

1

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[

[

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]