Intuitionistic type theory

From Wikipedia, the free encyclopedia

Jump to: navigation, search

Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Type Theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher, in 1972. Martin-Löf has modified his proposal a few times; his early, impredicative formulations were inconsistent as demonstrated by Girard's paradox, and later formulations were predicative. He also proposed extensional and then intensional variants of Type Theory.

Intuitionistic type theory is based on a certain analogy or isomorphism between propositions and 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 propositional logic and simply typed lambda calculus. Type Theory extends this identification to predicate logic by introducing dependent types, that is types which contain values. Type Theory internalizes the interpretation of intuitionistic logic proposed by Brouwer, Heyting and Kolmogorov, the so called BHK interpretation. The types of Type Theory play a similar role as sets in set theory but functions definable in Type Theory are always computable.

Contents

[edit] Connectives of Type Theory

In the context of Type Theory a connective is a way of constructing types, possibly using already given types. The basic connectives of Type Theory are:

[edit] Failed to parse (Missing texvc executable; please see math/README to configure.): \Pi -types

Failed to parse (Missing texvc executable; please see math/README to configure.): \Pi -types, also called dependent function types, generalize the normal function space to model functions whose result type may vary on their input. E.g. writing Failed to parse (Missing texvc executable; please see math/README to configure.): \mbox{Vec}({\mathbb R},n)

for Failed to parse (Missing texvc executable; please see math/README to configure.): n

-tuples of real numbers, Failed to parse (Missing texvc executable; please see math/README to configure.): \Pi n:{\mathbb N}.\mbox{Vec}({\mathbb R},n)

stands for the type of functions which given a natural number returns a tuple of real numbers of this size. The usual function space arises as a special case when the range type does not actually depend on the input, e.g. Failed to parse (Missing texvc executable; please see math/README to configure.): \Pi n:{\mathbb N}.{\mathbb R}
is the type of functions from natural numbers to the real numbers, which is also written as Failed to parse (Missing texvc executable; please see math/README to configure.): {\mathbb N}\to{\mathbb R}

. Using the Curry Howard isomorphism Failed to parse (Missing texvc executable; please see math/README to configure.): \Pi -types also serve to model implication and universal quantification: e.g. a term inhabiting Failed to parse (Missing texvc executable; please see math/README to configure.): \Pi m,n:{\mathbb N}.m+n = n+m

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.

[edit] Failed to parse (Missing texvc executable; please see math/README to configure.): \Sigma -types

Failed to parse (Missing texvc executable; please see math/README to configure.): \Sigma -types, also called dependent product types, generalize the usual Cartesian product to model pairs where the type of the 2nd component depends on the first. E.g. the type Failed to parse (Missing texvc executable; please see math/README to configure.): \Sigma n:{\mathbb N}.\mbox{Vec}({\mathbb R},n)

stands for the type of pairs of a natural number and a tuple of real numbers of that size, i.e. this type can be used to model sequences of arbitrary length (usually called lists). The conventional Cartesian product type arises as a special case when the type of the 2nd component doesn't actually depend on the first, e.g. Failed to parse (Missing texvc executable; please see math/README to configure.): \Sigma n:{\mathbb N}.{\mathbb R}
is the type of pairs of a natural number  and a real number, which is also written as Failed to parse (Missing texvc executable; please see math/README to configure.): {\mathbb N}\times{\mathbb R}

. Again, using the Curry Howard isomorphism, Failed to parse (Missing texvc executable; please see math/README to configure.): \Sigma -types also serve to model conjunction and existential quantification.

[edit] Finite types

Of special importance are Failed to parse (Missing texvc executable; please see math/README to configure.): 0

(the empty type), Failed to parse (Missing texvc executable; please see math/README to configure.): 1
(the unit type) and Failed to parse (Missing texvc executable; please see math/README to configure.): 2
(the type of Booleans or classical truth values). Invoking the Curry Howard isomorphism again, Failed to parse (Missing texvc executable; please see math/README to configure.): 0
stands for False and Failed to parse (Missing texvc executable; please see math/README to configure.): 1
for True.

Using finite types we can define negation as Failed to parse (Missing texvc executable; please see math/README to configure.): \neg A = A \to 0 .

[edit] Equality type

Given Failed to parse (Missing texvc executable; please see math/README to configure.): a,b : A

then Failed to parse (Missing texvc executable; please see math/README to configure.): a = b
is the type of equality proofs that Failed to parse (Missing texvc executable; please see math/README to configure.): a
is equal to Failed to parse (Missing texvc executable; please see math/README to configure.): b

. There is only one (canonical) inhabitant of Failed to parse (Missing texvc executable; please see math/README to configure.): a = b

and this is the proof of reflexivity Failed to parse (Missing texvc executable; please see math/README to configure.): \mbox{refl} : \Pi a:A.a = a

.

[edit] Inductive types

A prime example of an inductive type is the type of natural numbers Failed to parse (Missing texvc executable; please see math/README to configure.): \mathbb N

which is generated by Failed to parse (Missing texvc executable; please see math/README to configure.): 0 : {\mathbb N}
and Failed to parse (Missing texvc executable; please see math/README to configure.): \mbox{succ} :{\mathbb N} \to {\mathbb N}

. An important application of the propositions as types principle is the identification of (dependent) primitive recursion and induction by one elimination constant: Failed to parse (Missing texvc executable; please see math/README to configure.): {\mathbb N}-\mbox{elim} : P(0) \to (\Pi n:{\mathbb N}.P(n)\to P(\mbox{succ}(n)))\to\Pi n:{\mathbb N}.P(n)

for any given type Failed to parse (Missing texvc executable; please see math/README to configure.): P(n)
indexed by Failed to parse (Missing texvc executable; please see math/README to configure.): n:{\mathbb N}

. 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 Failed to parse (Missing texvc executable; please see math/README to configure.): \mbox{Vec}(A,n)

mentioned above, which is inductively generated by the constructors Failed to parse (Missing texvc executable; please see math/README to configure.): \mbox{vnil}:\mbox{Vec}(A,0)
and Failed to parse (Missing texvc executable; please see math/README to configure.): \mbox{vcons}:A\to\Pi n:{\mathbb N}.\mbox{Vec}(A,n)\to\mbox{Vec}(A,\mbox{succ}(n))

. Applying the Curry Howard isomorphism once more, inductive families correspond to inductively defined relations.

[edit] Universes

An example of a universe is Failed to parse (Missing texvc executable; please see math/README to configure.): U_0 , the universe of all small types, which contains names for all the types introduced so far. To every name Failed to parse (Missing texvc executable; please see math/README to configure.): a:U_0

we associate a type Failed to parse (Missing texvc executable; please see math/README to configure.): El(a)

, its extension or meaning. It is standard to assume a predicative hierarchy of universes: Failed to parse (Missing texvc executable; please see math/README to configure.): U_n

for every natural number Failed to parse (Missing texvc executable; please see math/README to configure.): n:{\mathbb N}

, where the universe Failed to parse (Missing texvc executable; please see math/README to configure.): U_{n+1}

contains a code for the previous universe, i.e. we have Failed to parse (Missing texvc executable; please see math/README to configure.): u_n:U_{n+1}
with Failed to parse (Missing texvc executable; please see math/README to configure.): El(u_n)=U_n

. This hierarchy is often assumed to be cumulative, that is the codes from Failed to parse (Missing texvc executable; please see math/README to configure.): U_n

are embedded in Failed to parse (Missing texvc executable; please see math/README to configure.): U_{n+1}

.

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 Girard's System F. This extension is not universally accepted by Intuitionists since it allows impredicative, i.e. circular, constructions, which are often identified with classical reasoning.

[edit] Formalisation of Type Theory

Type Theory is usually presented as a dependently typed lambda calculus, using the judgements:

  • Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash \Gamma\, \mbox{Context}

, Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma

is a well-formed context of typing assumptions.
  • Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma\vdash \sigma\, \mbox{Type}

, Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma

is a well-formed type in context Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma

.

  • Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma\vdash t : \sigma

, Failed to parse (Missing texvc executable; please see math/README to configure.): t

is a well-formed term of type Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma
in context Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma

.

  • Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma\vdash \sigma\equiv\tau

, Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma

and Failed to parse (Missing texvc executable; please see math/README to configure.): \tau
are equal types in context Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma

.

  • Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma\vdash t \equiv u: \sigma

, Failed to parse (Missing texvc executable; please see math/README to configure.): t

and Failed to parse (Missing texvc executable; please see math/README to configure.): u
are equal terms of type Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma
in context Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma

. Of special importance is the conversion rule, which says that given Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma\vdash t : \sigma

and Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma\vdash \sigma\equiv\tau
then Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma\vdash t : \tau

.

[edit] Categorical models of Type Theory

Using the language of category theory, 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^op -> 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' ° f = f ° B - in plain words, for each elements of the index set A ga maps Ba to B'f(a).

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.

[edit] Extensional versus intensional

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 contrast in intensional Type Theory type checking is decidable, but the representation of many mathematical concepts is non-standard due to a lack of extensional reasoning. It is a subject of current discussion whether this tradeoff is unavoidable and whether the lack of extensional principles in intensional Type Theory is a feature or a bug.

[edit] Implementations of Type Theory

Type Theory has been the base of a number of proof assistants, such as NuPRL, LEGO, Coq, and Agda. Recently, dependent types also featured in the design of programming languages such as Dependent ML, Cayenne and Epigram.

[edit] See also

[edit] External links

  • 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 here.
Retrieved from "http://en.wikilib.com/wiki/Intuitionistic_type_theory"
Personal tools