|
|
| (521 intermediate revisions by more than 100 users not shown) |
| Line 1: |
Line 1: |
| '''Intuitionistic type theory''' (also known as '''constructive type theory''', or '''Martin-Löf type theory''') is a [[type theory]] and an alternative [[Foundations of mathematics|foundation of mathematics]] based on the principles of [[mathematical constructivism]]. Intuitionistic type theory was introduced by [[Per Martin-Löf]], a [[Sweden|Swedish]] [[mathematician]] and [[philosopher]], in 1972. Martin-Löf has modified his proposal a few times; his 1971 [[impredicative]] formulation was inconsistent as demonstrated by [[Girard's paradox]]. Later formulations were [[Predicativity|predicative]]. He proposed both [[Intensional logic|intensional]] and [[extensionality|extensional]] variants of the theory. | | This is a preview for the new '''MathML rendering mode''' (with SVG fallback), which is availble in production for registered users. |
|
| |
|
| Intuitionistic type theory is based on a certain analogy or isomorphism between [[proposition]]s and [[Type theory|types]]: a proposition is identified with the type of its proofs. This identification is usually called the [[Curry–Howard isomorphism]], which was originally formulated for [[intuitionistic logic]] and [[simply typed lambda calculus]]. Type theory extends this identification to [[predicate logic]] by introducing [[dependent types]], that is types which contain values.
| | If you would like use the '''MathML''' rendering mode, you need a wikipedia user account that can be registered here [[https://en.wikipedia.org/wiki/Special:UserLogin/signup]] |
| | * Only registered users will be able to execute this rendering mode. |
| | * Note: you need not enter a email address (nor any other private information). Please do not use a password that you use elsewhere. |
|
| |
|
| Type theory internalizes the interpretation of [[intuitionistic logic]] proposed by [[Luitzen Egbertus Jan Brouwer|Brouwer]], [[Arend Heyting|Heyting]] and [[Andrey Kolmogorov|Kolmogorov]], the so-called [[BHK interpretation]]. The types in type theory play a similar role to sets in [[set theory]] but functions definable in type theory are always computable.
| | Registered users will be able to choose between the following three rendering modes: |
|
| |
|
| ==Connectives of type theory== | | '''MathML''' |
| In the context of type theory a [[Logical connective|connective]] is a way of constructing types, possibly using already given types.
| | :<math forcemathmode="mathml">E=mc^2</math> |
| The basic connectives of type theory are:
| |
|
| |
|
| ===Π-types===
| | <!--'''PNG''' (currently default in production) |
| {{main|Dependent type}}
| | :<math forcemathmode="png">E=mc^2</math> |
| Π-types, also called dependent product types, are analogous to the indexed [[Cartesian product|products]] of sets. As such, they generalize the normal [[function space]] to model functions whose result type may vary on their input. E.g. writing <math>\operatorname{Vec}({\mathbb R}, n)</math> for the type of [[tuple|''n''-tuples]] of [[real numbers]] and <math>\mathbb N</math> for the type of [[natural number]]s,
| |
|
| |
|
| :<math>\prod_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}({\mathbb R}, n)</math> | | '''source''' |
| | :<math forcemathmode="source">E=mc^2</math> --> |
|
| |
|
| stands for the type of a function that, given a natural number ''n'', returns an ''n''-tuple of real numbers. The usual function space arises as a special case when the range type does not actually depend on the input, e.g., <math>\prod_{n \mathbin{:} {\mathbb N}} {\mathbb R}</math> is the type of functions from natural numbers to the real numbers, which is also written as <math>{\mathbb N} \to {\mathbb R}</math>.
| | <span style="color: red">Follow this [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering link] to change your Math rendering settings.</span> You can also add a [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering-skin Custom CSS] to force the MathML/SVG rendering or select different font families. See [https://www.mediawiki.org/wiki/Extension:Math#CSS_for_the_MathML_with_SVG_fallback_mode these examples]. |
|
| |
|
| Using the [[Curry–Howard isomorphism]] Π-types also serve to model [[material conditional|implication]] and [[universal quantification]]: e.g., a term inhabiting
| | ==Demos== |
|
| |
|
| <math>\prod_{m, n \mathbin{:} {\mathbb N}} (m + n = n + m)</math>
| | Here are some [https://commons.wikimedia.org/w/index.php?title=Special:ListFiles/Frederic.wang demos]: |
|
| |
|
| is a function which assigns to any pair of natural numbers a proof that addition is [[commutative]] for that pair and hence can be considered as a proof that addition is commutative for all natural numbers. (Here we have used the ''equality type'' (<math>x = y</math>) as explained below.)
| |
|
| |
|
| ===Σ-types===
| | * accessibility: |
| Σ-types, also called dependent sum types, are analogous to the indexed [[disjoint union]]s of sets. As such, they generalize the usual [[Cartesian product]] to model pairs where the type of the second component depends on the first. For example, the type <math>\sum_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}({\mathbb R}, n)</math> stands for the type of pairs of a natural number <math>n</math> and an <math>n</math>-tuple of real numbers, i.e., this type can be used to model sequences of arbitrary but finite length (usually called lists). The conventional [[Cartesian product]] type arises as a special case when the type of the second component doesn't actually depend on the first, e.g., <math>\sum_{n \mathbin{:} {\mathbb N}} {\mathbb R}</math> is the type of pairs of a [[natural number]] and a [[real number]], which is also written as <math>{\mathbb N} \times {\mathbb R}</math>.
| | ** Safari + VoiceOver: [https://commons.wikimedia.org/wiki/File:VoiceOver-Mac-Safari.ogv video only], [[File:Voiceover-mathml-example-1.wav|thumb|Voiceover-mathml-example-1]], [[File:Voiceover-mathml-example-2.wav|thumb|Voiceover-mathml-example-2]], [[File:Voiceover-mathml-example-3.wav|thumb|Voiceover-mathml-example-3]], [[File:Voiceover-mathml-example-4.wav|thumb|Voiceover-mathml-example-4]], [[File:Voiceover-mathml-example-5.wav|thumb|Voiceover-mathml-example-5]], [[File:Voiceover-mathml-example-6.wav|thumb|Voiceover-mathml-example-6]], [[File:Voiceover-mathml-example-7.wav|thumb|Voiceover-mathml-example-7]] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-Audio-Windows7-InternetExplorer.ogg Internet Explorer + MathPlayer (audio)] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-SynchronizedHighlighting-WIndows7-InternetExplorer.png Internet Explorer + MathPlayer (synchronized highlighting)] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-Braille-Windows7-InternetExplorer.png Internet Explorer + MathPlayer (braille)] |
| | ** NVDA+MathPlayer: [[File:Nvda-mathml-example-1.wav|thumb|Nvda-mathml-example-1]], [[File:Nvda-mathml-example-2.wav|thumb|Nvda-mathml-example-2]], [[File:Nvda-mathml-example-3.wav|thumb|Nvda-mathml-example-3]], [[File:Nvda-mathml-example-4.wav|thumb|Nvda-mathml-example-4]], [[File:Nvda-mathml-example-5.wav|thumb|Nvda-mathml-example-5]], [[File:Nvda-mathml-example-6.wav|thumb|Nvda-mathml-example-6]], [[File:Nvda-mathml-example-7.wav|thumb|Nvda-mathml-example-7]]. |
| | ** Orca: There is ongoing work, but no support at all at the moment [[File:Orca-mathml-example-1.wav|thumb|Orca-mathml-example-1]], [[File:Orca-mathml-example-2.wav|thumb|Orca-mathml-example-2]], [[File:Orca-mathml-example-3.wav|thumb|Orca-mathml-example-3]], [[File:Orca-mathml-example-4.wav|thumb|Orca-mathml-example-4]], [[File:Orca-mathml-example-5.wav|thumb|Orca-mathml-example-5]], [[File:Orca-mathml-example-6.wav|thumb|Orca-mathml-example-6]], [[File:Orca-mathml-example-7.wav|thumb|Orca-mathml-example-7]]. |
| | ** From our testing, ChromeVox and JAWS are not able to read the formulas generated by the MathML mode. |
|
| |
|
| Again, using the [[Curry–Howard isomorphism]], Σ-types also serve to model [[Logical conjunction|conjunction]] and [[existential quantification]].
| | ==Test pages == |
|
| |
|
| ===Finite types===
| | To test the '''MathML''', '''PNG''', and '''source''' rendering modes, please go to one of the following test pages: |
| Of special importance are '''0''' or ⊥ (the [[empty type]]), '''1''' or ⊤ (the [[unit type]]) and '''2''' (the type of [[Boolean data type|Booleans]] or classical [[truth value]]s). Invoking the [[Curry–Howard isomorphism]] again, ⊥ stands for ''false'' and ⊤ for ''true''.
| | *[[Displaystyle]] |
| | *[[MathAxisAlignment]] |
| | *[[Styling]] |
| | *[[Linebreaking]] |
| | *[[Unique Ids]] |
| | *[[Help:Formula]] |
|
| |
|
| Using finite types we can define [[negation]] as
| | *[[Inputtypes|Inputtypes (private Wikis only)]] |
| | | *[[Url2Image|Url2Image (private Wikis only)]] |
| <math>\neg A \equiv A \to \bot.</math>
| | ==Bug reporting== |
| | | If you find any bugs, please report them at [https://bugzilla.wikimedia.org/enter_bug.cgi?product=MediaWiki%20extensions&component=Math&version=master&short_desc=Math-preview%20rendering%20problem Bugzilla], or write an email to math_bugs (at) ckurs (dot) de . |
| ===Equality type===
| |
| Given <math>a, b \mathbin{:} A</math>, the expression <math>a = b</math> denotes the type of equality proofs for <math>a</math> is equal to <math>b</math>. That is, if <math>a = b</math> is inhabited, then <math>a</math> is said to be ''equal'' to <math>b</math>. There is only one (canonical) inhabitant of <math>a = a</math> and this is the proof of reflexivity
| |
| | |
| <math>\operatorname{refl} \mathbin{:} \prod_{a \mathbin{:} A} (a = a).</math>
| |
| | |
| Examination of the properties of the equality type, or rather, extending it to a notion of equivalence, lead to [[homotopy type theory]].
| |
| | |
| ===Inductive types===
| |
| A prime example of an [[inductive type]] is the type of [[natural numbers]] <math>\mathbb{N}</math> which is generated by <math>0 \mathbin{:} {\mathbb N}</math> and <math>\operatorname{succ} \mathbin{:} {\mathbb N} \to {\mathbb N}</math>. An important application of the [[propositions as types principle]] is the identification of (dependent) [[primitive recursion]] and [[mathematical induction|induction]] by one elimination constant:
| |
| | |
| <math>{\operatorname{{\mathbb N}-elim}}\, \mathbin{:} P(0)\, \to \left(\prod_{n \mathbin{:} {\mathbb N}} P(n) \to P(\operatorname{succ}(n))\right) \to \prod_{n \mathbin{:} {\mathbb N}} P(n)</math>
| |
| | |
| for any given type <math>P(n)</math> indexed by <math>n \mathbin{:} {\mathbb N}</math>. In general inductive types can be defined in terms of W-types, the type of [[well-founded]] trees.
| |
| | |
| An important class of inductive types are inductive families like the type of vectors <math>\operatorname{Vec}(A, n)</math> mentioned above, which is inductively generated by the constructors <math>\operatorname{vnil} \mathbin{:} \operatorname{Vec}(A, 0)</math> and
| |
| | |
| <math>\operatorname{vcons}\, \mathbin{:}\, A \to \prod_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}(A, n) \to \operatorname{Vec}(A, \operatorname{succ}(n)).</math>
| |
| | |
| Applying the [[Curry–Howard isomorphism]] once more, inductive families correspond to inductively defined relations.
| |
| | |
| ===Universes===
| |
| An example of a universe is <math>\mathcal{U}_0</math>, the universe of all small types, which contains names for all the types introduced so far. To every name <math>a \mathbin{:} \mathcal{U}_0</math> we associate a type <math>\operatorname{El}(a)</math>, its extension or meaning. It is standard to assume a [[Impredicativity|predicative]] hierarchy of universes: <math>\mathcal{U}_n</math> for every natural number <math>n \mathbin{:} {\mathbb N}</math>, where the universe <math>\mathcal{U}_{n+1}</math> contains a code for the previous universe, i.e., we have <math>u_n \mathbin{:} \mathcal{U}_{n+1}</math> with <math>\operatorname{El}(u_n) \equiv \mathcal{U}_n</math>. (A hierarchy with this property is called "cumulative".)
| |
| | |
| Stronger universe principles have been investigated, i.e., super universes and the Mahlo universe. In 1992 Huet and Coquand introduced the [[calculus of constructions]], a type theory with an impredicative universe, thus combining type theory with [[Jean-Yves Girard|Girard]]'s [[System F]]. This extension is not universally accepted by [[Intuitionist]]s since it allows impredicative, i.e., circular, constructions, which are often identified with classical reasoning.
| |
| | |
| ==Formalisation of type theory== | |
| This formalization is based on the discussion in Nordström, Petersson, and Smith.
| |
| | |
| The formal theory works with ''types'' and ''objects''.
| |
| | |
| A type is declared by:
| |
| * <math>A\ \mathsf{Type}</math>
| |
| An object exists and is in a type if:
| |
| * <math>a \mathbin{:} A </math>
| |
| Objects can be equal
| |
| * <math>a = b</math>
| |
| and types can be equal
| |
| * <math>A = B</math>
| |
| A type that depends on an object from another type is declared
| |
| * <math> (x \mathbin{:} A)B</math>
| |
| and removed by substitution
| |
| * <math> B[x / a] </math>, replacing the variable <math>x</math> with the object <math>a</math> in <math>B</math>.
| |
| An object that depends on an object from another type can be done two ways.
| |
| If the object is "abstracted", then it is written | |
| * <math>[x]b</math>
| |
| and removed by substitution
| |
| * <math> b[x / a] </math>, replacing the variable <math>x</math> with the object <math>a</math> in <math>b</math>.
| |
| The object-depending-on-object can also be declared as a constant as part of a recursive type. An example of a recursive type is:
| |
| * <math>0 \mathbin{:} \mathbb{N} </math>
| |
| * <math>\operatorname{succ} \mathbin{:} \mathbb{N} \to \mathbb{N} </math>
| |
| Here, <math>\operatorname{succ}</math> is a constant object-depending-on-object. It is not associated with an abstraction.
| |
| Constants like <math>\operatorname{succ}</math> can be removed by defining equality. Here the relationship with addition is defined using equality and using pattern matching to handle the recursive aspect of <math>\operatorname{succ}</math>:
| |
| : <math>
| |
| \begin{align}
| |
| \operatorname{add} &\mathbin{:}\ (\mathbb{N} \times \mathbb{N}) \to \mathbb{N} \\
| |
| \operatorname{add}(0, b) &= b \\
| |
| \operatorname{add}(\operatorname{succ}(a), b) &= \operatorname{succ}(\operatorname{add}(a, b)))
| |
| \end{align}
| |
| </math>
| |
| <math>\operatorname{succ}</math> is manipulated as an opaque constant - it has no internal structure for substitution.
| |
| | |
| So, objects and types and these relations are used to express formulae in the theory. The following styles of judgements are used to create new objects, types and relations from existing ones:
| |
| | |
| {| class="wikitable"
| |
| |-
| |
| | <math>\Gamma\vdash \sigma\ \mathsf{Type}</math>
| |
| | ''σ'' is a well-formed type in the context Γ.
| |
| |-
| |
| | <math>\Gamma\vdash t \mathbin{:} \sigma</math>
| |
| | ''t'' is a well-formed term of type ''σ'' in context Γ.
| |
| |-
| |
| | <math>\Gamma\vdash \sigma \equiv \tau</math>
| |
| | ''σ'' and ''τ'' are equal types in context Γ.
| |
| |-
| |
| | <math>\Gamma\vdash t \equiv u \mathbin{:} \sigma</math>
| |
| | ''t'' and ''u'' are judgmentally equal terms of type ''σ'' in context Γ.
| |
| |-
| |
| | <math>\vdash \Gamma\ \mathsf{Context}</math>
| |
| | Γ is a well-formed context of typing assumptions.
| |
| |}
| |
| | |
| By convention, there is a type that represents all other types. It is called <math>\mathcal{U}</math> (or <math>\operatorname{Set}</math>). Since <math>\mathcal{U}</math> is a type, the member of it are objects. There is a dependent type <math>\operatorname{El}</math> that maps each object to its corresponding type. ''In most texts <math>\operatorname{El}</math> is never written.'' From the context of the statement, a reader can almost always tell whether <math>A</math> refers to a type, or whether it refers to the object in <math>\mathcal{U}</math> that corresponds to the type.
| |
| | |
| This is the complete foundation of the theory. Everything else is derived.
| |
| | |
| To implement logic, each proposition is given its own type. The objects in those types represent the different possible ways to prove the proposition. Obviously, if there is no proof for the proposition, then the type has no objects in it. Operators like "and" and "or" that work on propositions introduce new types and new objects. So <math>A \times B </math> is a type that depends on the type <math>A</math> and the type <math>B</math>. The objects in that dependent type are defined to exist for every pair of objects in <math>A</math> and <math>B</math>. Obviously, if <math>A</math> or <math>B</math> has no proof and is an empty type, then the new type representing <math> A \times B </math> is also empty.
| |
| | |
| This can be done for other types (booleans, natural numbers, etc.) and their operators.
| |
| | |
| ==Categorical models of type theory==
| |
| Using the language of [[category theory]], [[R.A.G. Seely]] introduced the notion of a [[locally cartesian closed category]] (LCCC) as the basic model of type theory. This has been refined by Hofmann and Dybjer to ''Categories with Families'' or ''Categories with Attributes'' based on earlier work by Cartmell.
| |
| | |
| A category with families is a category ''C'' of contexts (in which the objects are contexts, and
| |
| the context morphisms are substitutions), together with a functor ''T'' : ''C''<sup>op</sup> → ''Fam(Set)''.
| |
| | |
| ''Fam(Set)'' is the [[category of families]] of Sets, in which objects are pairs ''(A,B)'' of an "index set" ''A'' and a function ''B'': ''X'' → ''A'', and morphisms are pairs of functions ''f'' : ''A'' → ''A' '' and ''g'' : ''X'' → ''X' '', such that ''B' '' <sub>°</sub> ''g'' = ''f'' <sub>°</sub> ''B'' - in other words, ''f'' maps ''B<sub>a</sub>'' to ''B'<sub>g(a)</sub>''.
| |
| | |
| The functor ''T'' assigns to a context ''G'' a set ''Ty(G)'' of types, and for each ''A'' : ''Ty(G)'', a set ''Tm(G,A)'' of terms.
| |
| The axioms for a functor require that these play harmoniously with substitution. Substitution is usually
| |
| written in the form ''Af'' or ''af'', where ''A'' is a type in ''Ty(G)'' and ''a'' is a term in ''Tm(G,A)'', and ''f'' is a substitution
| |
| from ''D'' to ''G''. Here ''Af'' : ''Ty(D)'' and ''af'' : ''Tm(D,Af)''.
| |
| | |
| The category ''C'' must contain a terminal object (the empty context), and a final object for a form
| |
| of product called comprehension, or context extension, in which the right element is a type in the context of the left element.
| |
| If ''G'' is a context, and ''A'' : ''Ty(G)'', then there should be an object ''(G,A)'' final among
| |
| contexts ''D'' with mappings ''p'' : ''D → ''G'', ''q'' : ''Tm(D,Ap)''.
| |
| | |
| A logical framework, such as Martin-Löf's takes the form of
| |
| closure conditions on the context dependent sets of types and terms: that there should be a type called
| |
| Set, and for each set a type, that the types should be closed under forms of dependent sum and
| |
| product, and so forth.
| |
| | |
| A theory such as that of predicative set theory expresses closure conditions on the types of sets and
| |
| their elements: that they should be closed under operations that reflect dependent sum and product,
| |
| and under various forms of inductive definition.
| |
| | |
| ==Extensional versus intensional==
| |
| A fundamental distinction is [[Extensional definition|extensional]] vs [[Intensional definition|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 problem|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 [[Fixpoint combinator|Y-Combinator]], a detailed example of this can found in.<ref>Bengt Nordström; Kent Petersson; Jan M. Smith (1990). ''Programming in Martin-Löf's Type Theory''. Oxford University Press p.90</ref> 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. From a practical standpoint there's no difference between a program which doesn't terminate and a program which takes a million years to terminate.
| |
| | |
| In contrast in intensional type theory [[type checking]] is [[Decision problem|decidable]], but the representation of standard mathematical concepts is somewhat more cumbersome, since extensional reasoning requires using [[setoid]]s 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|integer numbers]], [[rational number]]s, and [[real number]]s. Integers and rational numbers can be represented without setoids, but this representation isn't easy to work with. Real numbers can't be represented without this see.<ref>Altenkirch, Thorsten, Thomas Anberrée, and Nuo Li. "Definable Quotients in Type Theory."</ref>
| |
| | |
| [[Homotopy type theory]] works on resolving this problem. It allows one to define [[higher inductive type]]s, which not only define first order constructors ([[value (computer science)|value]]s or [[point (geometry)|point]]s), but higher order constructors, i.e. equalities between elements ([[path (topology)|path]]s), equalities between equalities ([[homotopy|homotopies]]), ''ad infinitum''.
| |
| | |
| ==Implementations of type theory==
| |
| Type theory has been the base of a number of proof assistants, such as [[NuPRL]], [[LEGO (programming)|LEGO]] and [[Coq]]. Recently, [[dependent types]] also featured in the design of [[programming languages]] such as [[ATS (programming language)|ATS]], [[Cayenne (programming language)|Cayenne]], [[Epigram (programming language)|Epigram]], [[Agda (theorem prover)|Agda]], and [[Idris (programming language)|Idris]].
| |
| | |
| ==See also==
| |
| * [[Calculus of constructions]]
| |
| * [[Intuitionistic logic]]
| |
| * [[Per Martin-Löf]]
| |
| * [[Type theory]]
| |
| * [[Typed lambda calculus]]
| |
| | |
| ==References==
| |
| * Per Martin-Löf (1984). ''[http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf Intuitionistic Type Theory]'' Bibliopolis. ISBN 88-7088-105-9.
| |
| | |
| ==Further reading==
| |
| * Bengt Nordström; Kent Petersson; Jan M. Smith (1990). ''Programming in Martin-Löf's Type Theory''. Oxford University Press. The book is out of print, but a free version can be picked up from [http://www.cs.chalmers.se/Cs/Research/Logic/book/ here].
| |
| * Thompson, Simon (1991). ''[http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming]'' Addison-Wesley. ISBN 0-201-41667-0.
| |
| * Granström, Johan G. (2011). ''[http://www.springer.com/philosophy/book/978-94-007-1735-0 Treatise on Intuitionistic Type Theory]'' Springer. ISBN 978-94-007-1735-0.
| |
| | |
| ==External links==
| |
| * [http://www.cs.chalmers.se/Cs/Research/Logic/Types/tutorials.html EU Types Project: Tutorials] - lecture notes and slides from the Types Summer School 2005
| |
| * [http://math.ucr.edu/home/baez/ncat.def.html n-Categories - Sketch of a Definition] - letter from John Baez and James Dolan to Ross Street, November 29, 1995
| |
| | |
| == References ==
| |
| {{Reflist}}
| |
| | |
| {{Non-classical logic}}
| |
| | |
| {{DEFAULTSORT:Intuitionistic Type Theory}}
| |
| [[Category:Dependently typed programming]]
| |
| [[Category:Constructivism (mathematics)]]
| |
| [[Category:Type theory]]
| |
| [[Category:Logic in computer science]]
| |
| [[Category:Intuitionism]]
| |
