利用者:I.hidekazu/直観主義型理論

直観主義型理論（ちょっかんしゅぎかたりろん、英: intuitionistic type theory）とは、数学の代替基盤を目指した型理論を言う。構成的型理論（constructive type theory）、またはマルティン＝レーフの型理論（Martin-Löf's type theory）とも呼ばれる。

1972年、スウェーデンの論理学、哲学者のペール・マルティン＝レーフによって最初のバージョンが発表された。直観主義型理論には複数のバージョンがある。

マルティン＝レーフは当初非可述的な定義が可能な型理論を構築していたが、ジラール（Jean-Yves Girard）によってパラドックスを起こすことが指摘され一時頓挫した（ジラールのパラドックス）。その後、パラドックスを起こさない可述的なバージョンが発表された。ただし、すべてのバージョンは、依存型を使用した構成的論理のコア設計を維持している。

設計方針[編集]

マルティン＝レーフは、この型理論を数学における構成主義の原理に基づいて設計をおこなった。構成主義は、「証拠」を含んだ存在証明を必要とする。すなわち、「１０００より大きい素数が存在する」という証明においては、１０００よりも大きくかつ素数である特定の数を確定しなければならない。直観主義型理論は、BHK解釈（Brouwer–Heyting–Kolmogorov interpretation）を内部化するという設計方針を達成している。興味深い点として、証明（proof）が、調査、比較、そして操作できる数学的対象になるというところがある。

直観主義型理論の型構築子（type constructor）は、論理演算子（logical connective）と一対一で対応するように作られている。例えば、含意と呼ばれる論理演算子（ $A\implies B$ ）は、関数型（ $A\to B$ ）に対応する。この対応はカリー＝ハワード同型対応と呼ばれる。かつての型理論もこの同型対応に従っていたが、現在のマルティン＝レーフの型理論は依存型（dependent type）を導入することによって述語論理をそのように拡張した最初のものである。

型理論[編集]

直観主義型理論は３つの有限型を持つ。その有限型は５つの異なる型構築子（type constructor）を組み合わせたものである。集合論とは異なり、型理論は第一階述語論理のような論理学をベースに構築されてはいない。だから、それぞれの型理論の特徴は、数学と論理学両方の特徴としての役割を果たす。

型理論に親しんでいないが、集合論を知っているという人に対する簡単な要約は次のとおりである。集合が元を含むのと同じように型は項（term）を含む。項は一つそしてただ一つだけの型に属する。 $2+2$ や $2\cdot 2$ のような項は計算（簡約）すると4のようなカノニカルな項（canonical term）になる。さらに知りたい場合は型理論の記事を参照せよ

0 type, 1 type and 2 type[編集]

There are 3 finite types: The 0 type contains 0 terms. The 1 type contains 1 canonical term. And the 2 type contains 2 canonical terms.

Because the 0 type contains 0 terms, it is also called the empty type. It is used to represent anything that cannot exist. It is also written $\bot$ and represents anything unprovable. (That is, a proof of it cannot exist.) As a result, negation is defined as a function to it: $\neg A:=A\to \bot$ .

Likewise, the 1 type contains 1 canonical term and represents existence. It also is called the unit type. It often represents propositions that can be proven and is, therefore, sometimes written $\top$ .

Finally, the 2 type contains 2 canonical terms. It represents a definite choice between two values. It is used for Boolean values but not propositions. Propositions are considered the 1 type and may be proven to never have a proof (the 0 type), or may not be proven either way. (The Law of Excluded Middle does not hold for propositions in intuitionistic type theory.)

Σ type constructor[編集]

Σ-types contain ordered pairs. As with typical ordered pair (or 2-tuple) types, a Σ-type can describe the Cartesian product, $A\times B$ , of two other types, $A$ and $B$ . Logically, such an ordered pair would hold a proof of $A$ and a proof of $B$ , so one may see such a type written as $A\wedge B$ .

Σ-types are more powerful than typical ordered pair types because of dependent typing. In the ordered pair, the type of the second term can depend on the value of the first term. For example, the first term of the pair might be a natural number and the second term's type might be a vector of length equal to the first term. Such a type would be written:

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

Using set-theory terminology, this is similar to an indexed disjoint unions of sets. In the case of usual ordered pairs, the type of the second term does not depend on the value of the first term. Thus the type describing the cartesian product ${\mathbb {N} }\times {\mathbb {R} }$ is written:

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

It is important to note here that the value of the first term, $n$ , is not depended on by the type of the second term, ${\mathbb {R} }$ .

Obviously, Σ-types can be used to build up longer dependently-typed tuples used in mathematics and the records or structs used in most programming languages. An example of a dependently-typed 3-tuple is two integers and a proof that the first integer is smaller than the second integer, described by the type:

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

Dependent typing allows Σ-types to serve the role of existential quantifier. The statement "there exists an $n$ of type ${\mathbb {N} }$ , such that $P(n)$ is proven" becomes the type of ordered pairs where the first item is the value $n$ of type ${\mathbb {N} }$ and the second item is a proof of $P(n)$ . Notice that the type of the second item (proofs of $P(n)$ ) depends on the value in the first part of the ordered pair ( $n$ ). Its type would be:

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

Π type constructor[編集]

Π-types contain functions. As with typical function types, they consist of an input type and an output type. They are more powerful than typical function types however, in that the return type can depend on the input value. Functions in type theory are different from set theory. In set theory, you look up the argument's value in a set of ordered pairs. In type theory, the argument is substituted into a term and then computation ("reduction") is applied to the term.

As an example, the type of a function that, given a natural number $n$ , returns a vector containing $n$ real numbers is written:

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

When the output type does not depend on the input value, the function type is often simply written with a $\to$ . Thus, ${\mathbb {N} }\to {\mathbb {R} }$ is the type of functions from natural numbers to real numbers. Such Π-types correspond to logical implication. The logical proposition $A\implies B$ corresponds to the type $A\to B$ , containing functions that take proofs-of-A and return proofs-of-B. This type could be written more consistently as:

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

Π-types are also used in logic for universal quantification. The statement "for every $n$ of type ${\mathbb {N} }$ , $P(n)$ is proven" becomes a function from $n$ of type ${\mathbb {N} }$ to proofs of $P(n)$ . Thus, given the value for $n$ the function generates a proof that $P()$ holds for that value. The type would be

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

= type constructor[編集]

=-types are created from two terms. Given two terms like $2+2$ and $2\cdot 2$ , you can create a new type $2+2=2\cdot 2$ . The terms of that new type represent proofs that the pair reduce to the same canonical term. Thus, since both $2+2$ and $2\cdot 2$ compute to the canonical term $4$ , there will be a term of the type $2+2=2\cdot 2$ . In intuitionistic type theory, there is a single way to make terms of =-types and that is by reflexivity:

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

It is possible to create =-types such as $1=2$ where the terms do not reduce to the same canonical term, but you will be unable to create terms of that new type. In fact, if you were able to create a term of $1=2$ , you could create a term of $\bot$ . Putting that into a function would generate a function of type $1=2\to \bot$ . Since $\ldots \to \bot$ is how intuitionistic type theory defines negation, you would have $\neg (1=2)$ or, finally, $1\neq 2$ .

Equality of proofs is an area of active research in proof theory and has led to the development of homotopy type theory and other type theories.

Inductive types[編集]

詳細は「Inductive type」を参照

Inductive types allow the creation of complex, self-referential types. For example, a linked list of natural numbers is either an empty list or a pair of a natural number and another linked list. Inductive types can be used to define unbounded mathematical structures like trees, graphs, etc.. In fact, the natural numbers type may be defined as an inductive type, either being $0$ or the successor of another natural number.

Inductive types define new constants, such as zero $0{\mathbin {:}}{\mathbb {N} }$ and the successor function $S{\mathbin {:}}{\mathbb {N} }\to {\mathbb {N} }$ . Since $S$ does not have a definition and cannot be evaluated using substitution, terms like $S0$ and $SSS0$ become the canonical terms of the natural numbers.

Proofs on inductive types are made possible by induction. Each new inductive type comes with its own inductive rule. To prove a predicate $P()$ for every natural number, you use the following rule:

{\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)

Inductive types in intuitionistic type theory are defined in terms of W-types, the type of well-founded trees. Later work in type theory generated coinductive types, induction-recursion, and induction-induction for working on types with more obscure kinds of self-referentiality. Higher inductive types allow equality to be defined between terms.

Universe types[編集]

The universe types allow proofs to be written about all the types created with the other type constructors. Every term in the universe type ${\mathcal {U}}_{0}$ can be mapped to a type created with any combination of $0,1,2,\Sigma ,\Pi ,=,$ and the inductive type constructor. However, to avoid paradoxes, there is no term in ${\mathcal {U}}_{0}$ that maps to ${\mathcal {U}}_{0}$ .

To write proofs about all "the small types" and ${\mathcal {U}}_{0}$ , you must use ${\mathcal {U}}_{1}$ , which does contain a term for ${\mathcal {U}}_{0}$ , but not for itself ${\mathcal {U}}_{1}$ . Similarly, for ${\mathcal {U}}_{2}$ . There is a predicative hierarchy of universes, so to quantify a proof over any fixed constant $k$ universes, you can use ${\mathcal {U}}_{k+1}$ .

Universe types are a tricky feature of type theories. Martin-Löf's original type theory had to be changed to account for Girard's paradox. Later research covered topics such as "super universes", "Mahlo universes", and impredicative universes.

Extensional versus intensional[編集]

基本的な違いは、外延型理論と内包型理論です。伸長型理論では、定義的（つまり、計算的）等式は、証明を必要とする命題的等式と区別されません。結果として、理論内のプログラムが終了しない可能性があるため、拡張型理論では型チェックが決定不能になります。たとえば、このような理論では、Y-combinatorに型を与えることができます。この詳細な例は、Martin-Löfの型理論のNordstömおよびPeterssonプログラミングにあります。[1]ただし、これは拡張型理論が実用的なツールの基礎になることを妨げるものではありません。たとえば、NuPRLは拡張型理論に基づいています。

対照的に、内包型理論では型チェックは決定可能ですが、内包的推論ではsetoidまたは同様の構造を使用する必要があるため、標準的な数学的概念の表現はやや面倒です。整数、有理数、実数など、操作が難しい、またはこれなしでは表現できない一般的な数学的オブジェクトが多数あります。整数と有理数はsetoidなしで表現できますが、この表現を操作するのは簡単ではありません。コーシー実数はこれなしでは表現できません。[2]

ホモトピー型理論は、この問題の解決に取り組んでいます。これにより、一次コンストラクター（値または点）だけでなく、高次コンストラクター、つまり要素（パス）間の等式、等式（ホモトピー）間の等式、無限大を定義する、より高次の誘導型を定義できます。

A fundamental distinction is extensional vs intensional type theory. In extensional type theory definitional (i.e., computational) equality is not distinguished from propositional equality, which requires proof. As a consequence type checking becomes undecidable in extensional type theory because programs in the theory might not terminate. For example, such a theory allows one to give a type to the Y-combinator, a detailed example of this can be found in Nordstöm and Petersson Programming in Martin-Löf's Type Theory.^[1] However, this doesn't prevent extensional type theory from being a basis for a practical tool, for example, NuPRL is based on extensional type theory.

In contrast in intensional type theory type checking is decidable, but the representation of standard mathematical concepts is somewhat more cumbersome, since intensional reasoning requires using setoids or similar constructions. There are many common mathematical objects, which are hard to work with or can't be represented without this, for example, integer numbers, rational numbers, and real numbers. Integers and rational numbers can be represented without setoids, but this representation isn't easy to work with. Cauchy real numbers can't be represented without this.^[2]

Homotopy type theory works on resolving this problem. It allows one to define higher inductive types, which not only define first order constructors (values or points), but higher order constructors, i.e. equalities between elements (paths), equalities between equalities (homotopies), ad infinitum.

型理論のバージョン[編集]

ペール・マルティン＝レーフはいくつもの型理論を構成したが、その発表の時期は、それらが記述された査読前論文が専門家（ジャン＝イヴ・ジラールやGiovanni Sambin）に受理されることになったときよりだいぶ後のさまざまな時期に発表された。以下のリストは、印刷された形態で記述された全ての理論を列挙することを試みたものであり、それらを互いに区別するための重要な特徴を素描している。これら理論の全ては依存積（dependent product）、依存和（dependent sum）、分離和（disjoint union）、有限型、そして自然数を持つ。全ての理論は、依存積に対するη-簡約が追加されたMLTT79を除いて、依存積か依存和のどちらかに対するη-簡約を含まない同じ簡約規則を持つ。

MLTT71: MLTT71 はペール・マルティン＝レーフによって作られた最初の型理論であり、1971年に査読前原稿の中で登場した。それは一つの宇宙（universe）を持っていたが、この宇宙にはそれ自身名前を持っていた。つまり、今日"Type in Type"と呼ばれるものを持つ型理論であった。ジャン＝イヴ・ジラールは、この体系は矛盾していることを示した。そして、この査読前原稿は一度も出版されていない。

MLTT72: MLTT72 は現在公開されている1972年の査読前原稿で発表された^[3]。理論は一つの宇宙（universe）を持つが恒等型（identity type）は持たなかった。その宇宙は、次の意味で"可述的"（predicative）であった。

MLTT72 was presented in a 1972 preprint that has now been published. That theory had one universe V and no identity types . The universe was "predicative" in the sense that the dependent product of a family of objects from V over an object that was not in V such as, for example, V itself, was not assumed to be in V. The universe was à la Russell, i.e., one would write directly "T∈V" and "t∈T" (Martin-Löf uses the sign "∈" instead of modern ":") without the additional constructor such as "El".

MLTT72は、現在公開されている1972年のプレプリントで発表されました。[1]その理論には1つのユニバースVがあり、IDタイプはありませんでした。テンプレート：定義は必要ありません。宇宙は、たとえばV自体など、Vにないオブジェクトに対する、Vからのオブジェクトのファミリーの従属積が、Vにあると想定されなかったという意味で、「述語」でした。宇宙はアラでした。ラッセル、つまり、「El」などの追加のコンストラクターなしで、「T∈V」と「t∈T」（Martin-Löfは現代の「：」の代わりに記号「∈」を使用）を直接記述します。

MLTT73 was the first definition of a type theory that Per Martin-Löf published (it was presented at the Logic Colloquium 73 and published in 1975^[4]). There are identity types which he calls "propositions" but since no real distinction between propositions and the rest of the types is introduced the meaning of this is unclear. There is what later acquires the name of J-eliminator but yet without a name (see pp. 94–95). There is in this theory an infinite sequence of universes V₀, ..., V_n, ... . The universes are predicative, a-la Russell and non-cumulative! In fact, Corollary 3.10 on p. 115 says that if A∈V_m and B∈V_n are such that A and B are convertible then m = n. This means, for example, that it would be difficult to formulate univalence in this theory—there are contractible types in each of the V_i but it is unclear how to declare them to be equal since there are no identity types connecting V_i and V_j for i ≠ j.

MLTT73は、PerMartin-Löfが発表した型理論の最初の定義でした（Logic Colloquium 73で発表され、1975年に発表されました[2]）。彼が「命題」と呼ぶアイデンティティタイプがありますが、命題と他のタイプの実際の区別が導入されていないため、これの意味は不明です。後にJ-eliminatorの名前を取得するものがありますが、名前はありません（94〜95ページを参照）。この理論には、宇宙V0、...、Vn、...の無限のシーケンスがあります。宇宙は述語的で、ラッセルであり、非累積的です！実際、p。の結果3.10。 115は、A∈VmとB∈VnがAとBが変換可能であるようなものである場合、m = nであると述べています。これは、たとえば、この理論で一価性を定式化するのが難しいことを意味します。各Viには可縮型がありますが、iのViとVjを接続するアイデンティティ型がないため、それらが等しいと宣言する方法は不明です。 ≠j。

MLTT79: MLTT79 は1979年に発表され、1982年に出版された^[5]。この論文において、マルティン＝レーフは依存的型理論のための４つの判断の基本型を導入した。依存的型理論はメタ理論のような体系の研究における基本的なものとなった。彼はまたその中において分離された概念として文脈（context）を導入した（see p.161）。J-除去（これはMLTT73に登場していたがこの名称はこのバージョンからである）規則を持つだけでなく理論を"拡大"（extensional）させるための規則も持つ（p.169）恒等型を持つ。また、W型を持つ。"累積的"（cumulative）で可述的（predicative）な無限列も持つ。

Bibliopolis: there is a discussion of a type theory in the Bibliopolis book from 1984^[6] but it is somewhat open-ended and does not seem to represent a particular set of choices and so there is no specific type theory associated with it.

ビブリオポリス：1984年のビブリオポリスの本[4]に型理論の議論がありますが、それはやや自由形式であり、特定の選択肢のセットを表していないようであり、それに関連する特定の型理論はありません。

脚注[編集]

^ Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in Martin-Löf's Type Theory. Oxford University Press, p. 90.
^ Altenkirch, Thorsten, Thomas Anberrée, and Nuo Li. "Definable Quotients in Type Theory."
^ Per Martin-Löf, An intuitionistic theory of types, Twenty-five years of constructive type theory (Venice,1995), Oxford Logic Guides, v. 36, pp. 127--172, Oxford Univ. Press, New York, 1998
^ Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium '73 (Bristol, 1973), 73--118. Studies in Logic and the Foundations of Mathematics, Vol. 80, North-Holland, Amsterdam,1975
^ Per Martin-Löf, Constructive mathematics and computer programming, Logic, methodology and philosophy of science, VI (Hannover, 1979), Stud. Logic Found. Math., v. 104, pp. 153--175, North-Holland, Amsterdam, 1982
^ Per Martin-Löf, Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, v. 1, Notes by Giovanni Sambin, pp. iv+91, 1984

参考文献　[編集]

外部リンク[編集]

EU Types Project: Tutorials – 型についての夏の学校2005の講義録及びスライド
n-Categories - Sketch of a Definition – 1995年11月２９日付のジョン・バエズとJames Dolanからロス・ストリートへの手紙

[1] Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in Martin-Löf's Type Theory. Oxford University Press, p. 90.

[2] Altenkirch, Thorsten, Thomas Anberrée, and Nuo Li. "Definable Quotients in Type Theory."

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

[4] Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium '73 (Bristol, 1973), 73--118. Studies in Logic and the Foundations of Mathematics, Vol. 80, North-Holland, Amsterdam,1975

[5] Per Martin-Löf, Constructive mathematics and computer programming, Logic, methodology and philosophy of science, VI (Hannover, 1979), Stud. Logic Found. Math., v. 104, pp. 153--175, North-Holland, Amsterdam, 1982

[MartinLöf1984-6] Per Martin-Löf, Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, v. 1, Notes by Giovanni Sambin, pp. iv+91, 1984

[1]

[2]

[3]

[4]

[5]

[6]