「利用者:I.hidekazu/直観主義型理論」の版間の差分
削除された内容 追加された内容
I.hidekazu (会話 | 投稿記録) 編集の要約なし |
I.hidekazu (会話 | 投稿記録) 編集の要約なし |
||
9行目:
直観主義型理論の型構築子（type constructor）は、論理演算子（logical connective）と一対一で対応するように作られている。例えば、含意と呼ばれる論理演算子（<math>A \implies B</math>）は、関数型（<math>A \to B</math>）に対応する。この対応は[[カリー＝ハワード同型対応]]と呼ばれる。かつての型理論もこの同型対応に従っていたが、現在のマルティン＝レーフの型理論は[[依存型]]（dependent type）を導入することによって述語論理をそのように拡張した最初のものである。
==Type theory==
Intuitionistic type theory has 3 finite types, which are then composed using 5 different type constructors. Unlike set theories, type theories are not built on top of a logic like [[First-order logic|Frege's]]. So, each feature of the type theory does double duty as a feature of both math and logic.
''If you are unfamiliar with type theory and know set theory, a quick summary is: Types contain terms just like sets contain elements. Terms belong to one and only one type. Terms like <math>2+2</math> and <math>2\cdot 2</math> compute ("reduce") down to canonical terms like 4. For more, see the article on [[Type theory]].''
===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 <math>\bot</math> and represents anything unprovable. (That is, a proof of it cannot exist.) As a result, [[negation]] is defined as a function to it: <math>\neg A := A \to \bot</math>.
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 <math>\top</math>.
Finally, the '''2''' type contains 2 canonical terms. It represents a definite choice between two values. It is used for [[Boolean Algebra|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|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]], <math>A \times B</math>, of two other types, <math>A</math> and <math>B</math>. Logically, such an ordered pair would hold a proof of <math>A</math> and a proof of <math>B</math>, so one may see such a type written as <math>A \wedge B</math>.
Σ-types are more powerful than typical ordered pair types because of [[Dependent type|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:
:<math>\sum_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}({\mathbb R}, n)</math>
Using set-theory terminology, this is similar to an indexed [[disjoint union]]s 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 <math>{\mathbb N} \times {\mathbb R}</math> is written:
:<math>\sum_{n \mathbin{:} {\mathbb N}} {\mathbb R}</math>
It is important to note here that the value of the first term, <math>n</math>, is not depended on by the type of the second term, <math>{\mathbb R}</math>.
Obviously, Σ-types can be used to build up longer dependently-typed [[tuple]]s used in mathematics and the [[Record (computer science)|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:
:<math>\sum_{m \mathbin{:} {\mathbb Z}} {\sum_{n \mathbin{:} {\mathbb Z}} ((m < n) = \text{True})}</math>
Dependent typing allows Σ-types to serve the role of [[existential quantifier]]. The statement "there exists an <math>n</math> of type <math>{\mathbb N}</math>, such that <math>P(n)</math> is proven" becomes the type of ordered pairs where the first item is the value <math>n</math> of type <math>{\mathbb N}</math> and the second item is a proof of <math>P(n)</math>. Notice that the type of the second item (proofs of <math>P(n)</math>) depends on the value in the first part of the ordered pair (<math>n</math>). Its type would be:
:<math>\sum_{n \mathbin{:} {\mathbb N}} P(n)</math>
===Π 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 <math>n</math>, returns a vector containing <math>n</math> real numbers is written:
:<math>\prod_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}({\mathbb R}, n)</math>
When the output type does not depend on the input value, the function type is often simply written with a <math>\to</math>. Thus, <math>{\mathbb N} \to {\mathbb R}</math> is the type of functions from natural numbers to real numbers. Such Π-types correspond to logical implication. The logical proposition <math>A \implies B</math> corresponds to the type <math>A \to B</math>, containing functions that take proofs-of-A and return proofs-of-B. This type could be written more consistently as:
:<math>\prod_{a \mathbin{:} A} B</math>
Π-types are also used in logic for [[universal quantification]]. The statement "for every <math>n</math> of type <math>{\mathbb N}</math>, <math>P(n)</math> is proven" becomes a function from <math>n</math> of type <math>{\mathbb N}</math> to proofs of <math>P(n)</math>. Thus, given the value for <math>n</math> the function generates a proof that <math>P()</math> holds for that value. The type would be
:<math>\prod_{n \mathbin{:} {\mathbb N}} P(n)</math>
=== = type constructor ===
<nowiki>=</nowiki>-types are created from two terms. Given two terms like <math>2+2</math> and <math>2 \cdot 2</math>, you can create a new type <math>2+2=2\cdot 2</math>. The terms of that new type represent proofs that the pair reduce to the same canonical term. Thus, since both <math>2+2</math> and <math>2\cdot 2</math> compute to the canonical term <math>4</math>, there will be a term of the type <math>2+2=2\cdot 2</math>. In intuitionistic type theory, there is a single way to make terms of =-types and that is by [[Reflexive relation|reflexivity]]:
:<math>\operatorname{refl} \mathbin{:} \prod_{a \mathbin{:} A} (a = a).</math>
It is possible to create =-types such as <math>1=2</math> 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 <math>1=2</math>, you could create a term of <math>\bot</math>. Putting that into a function would generate a function of type <math>1=2 \to \bot</math>. Since <math>\ldots \to \bot</math> is how intuitionistic type theory defines negation, you would have <math>\neg (1=2)</math> or, finally, <math>1 \neq 2</math>.
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===
{{Main|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 <math>0</math> or the [[Successor function|successor]] of another natural number.
Inductive types define new constants, such as zero <math>0 \mathbin{:} {\mathbb N}</math> and the successor function <math>S \mathbin{:} {\mathbb N} \to {\mathbb N}</math>. Since <math>S</math> does not have a definition and cannot be evaluated using substitution, terms like <math>S 0</math>
and <math>S S S 0</math> become the canonical terms of the natural numbers.
Proofs on inductive types are made possible by [[Structural induction|induction]]. Each new inductive type comes with its own inductive rule. To prove a predicate <math>P()</math> for every natural number, you use the following rule:
:<math>{\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)</math>
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 type]]s 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 <math>\mathcal{U}_0</math> can be mapped to a type created with any combination of <math>0,1,2,\Sigma,\Pi,=,</math> and the inductive type constructor. However, to avoid paradoxes, there is no term in <math>\mathcal{U}_0</math> that maps to <math>\mathcal{U}_0</math>.
To write proofs about all "the small types" and <math>\mathcal{U}_0</math>, you must use <math>\mathcal{U}_1</math>, which does contain a term for <math>\mathcal{U}_0</math>, but not for itself <math>\mathcal{U}_1</math>. Similarly, for <math>\mathcal{U}_2</math>. There is a [[Impredicativity|predicative]] hierarchy of universes, so to quantify a proof over any fixed constant <math>k</math> universes, you can use <math>\mathcal{U}_{k+1}</math>.
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 ==
| |||