Type theory

In mathematical logic and theoretical computer science , type theories are formal systems in which every term has a type and operations are restricted to certain types. Some type theories are used as an alternative to axiomatic set theory as the basis for modern mathematics.

Type theories overlap with type systems , which are a feature of programming languages to avoid errors.

Two popular type theories that are used as a mathematical basis are Alonzo Church's typed lambda calculus and Per Martin-Löf's intuitionistic type theory .

history

Between 1902 and 1908, Bertrand Russell proposed various type theories with which Russell's antinomy of the naive set theory of Gottlob Frege should be avoided. His “branched” type theory and the axiom of reducibility played an important role in the Principia Mathematica published between 1910 and 1913 . Whitehead and Russell tried there to avoid Russell's paradox by means of a hierarchy of types, with each mathematical entity being assigned a type. Objects of a certain type can only be made up of objects of a lower type, so that loops are avoided. In the 1920s, Leon Chwistek and Frank P. Ramsey proposed a simpler theory now known as "simple type theory".

Typically, a type theory consists of types and a term rewriting system . A well-known example is the lambda calculus . The logic of a higher level is based on it .

In some areas of constructive mathematics and also for the proof assistant Agda , the intuitionistic type theory is used. In contrast, the evidence assistant Coq is based on the construction calculus CoC. An active area of research is homotopy type theory.

Basic concepts

In type theory, every term has a type and operations are only defined for terms of a certain type. A type judgment says that the term is of type . For example, the type of the natural numbers and are terms of this type. is the judgment that is of the type . ${\ displaystyle M \ colon A}$ ${\ displaystyle M}$ ${\ displaystyle A}$ ${\ displaystyle nat}$ ${\ displaystyle 0,1,2, \ ldots}$ ${\ displaystyle 2 \ colon nat}$ ${\ displaystyle 2}$ ${\ displaystyle nat}$

In type theory, a function is indicated by an arrow . The successor function has the judgment . The call of a function is sometimes written without brackets, i.e. instead of ${\ displaystyle \ to}$ ${\ displaystyle addOne}$ ${\ displaystyle addOne \ colon nat \ to nat}$ ${\ displaystyle addOne2}$ ${\ displaystyle addOne (2).}$

A type theory can also contain term transformation rules. For example, and are syntactically different terms, but the first can be reduced to the second. One writes . ${\ displaystyle 2 + 1}$ ${\ displaystyle 3}$ ${\ displaystyle 2 + 1 \ twoheadrightarrow 3}$

Type theories

Lambda calculus (after Church)

Alonzo Church used the lambda calculus in 1936 to give both a negative answer to the decision problem and to find a foundation for a logical system, such as the Principia Mathematica by Bertrand Russell and Alfred North Whitehead. Using the untyped lambda calculus, it is possible to clearly define what a calculable function is. The question of whether two lambda expressions (see below ) are equivalent cannot generally be decided algorithmically. In its typified form, the calculus can be used to represent higher level logic. The lambda calculus has significantly influenced the development of functional programming languages , research into type systems of programming languages in general and modern sub-disciplines in logic such as type theory.

Intuitionistic type theory (after Martin-Löf)

The intuitionist type theory according to Per Martin-Löf is a type theory based on the principles of constructivism and an alternative foundation of mathematics .

It is based on an analogy between propositions and types: a proposition is identified with the type of its proof. So is z. B. the type of all ordered pairs comparable with logical conjunction : Such an ordered pair can only exist if both types have at least one element. This allows many logical principles to be generalized.

Another very relevant aspect of type theory are inductive definitions. An example of this are the natural numbers : They are explicitly defined as a construction consisting of zero and a successor function. These are not specifically defined as in set theory , but their existence is assumed or permitted by a generalized construction. Together with these constructors there is also an induction scheme that allows the creation of functions using natural numbers or proofs that apply to every natural number.

In general, the intuitionist type theory is often seen as closer to mathematical practice than fundamental set theory, since in this every mathematical object is viewed as a set.

Calculus of Constructions (after Coquand)

The type theory Calculus of Constructions (CoC) according to Thierry Coquand is a higher order lambda calculus, which is the basis for a constructive structure of mathematics as well as for the computerized proof system Coq .

Homotopy type theory

The homotopy type theory ( HoTT ) describes developments of the intensional type theory of Martin-Löf, based on the interpretation of types as objects of the homotopy theory ( Vladimir Voevodsky ). Homotopy type theory can be used as an alternative to set theory as the basis for any mathematics. Current research therefore includes a. the formulation of conventional mathematics based on type theory and the implementation in proof assistants .

In the academic year 2012/2013 a book about the basics of this discipline was created in a joint research project at the Institute for Advanced Study .

Special types

Unit type - void or 0-tuple (English: void type), has only a single value, similar to:
Bottom type - empty type without values (zero or ⊥), see also Top type (has no value)
Top type - the universal type (object or ⊤), see also Top type (all other types are subtypes)

Type constructors

A type constructor can be used to construct new types from existing (simple) types. Examples are setof according to Russell's type hierarchy (also iterates to a base type) and constructors for ordered pairs or n-tuples: If components have different types, a pair representation according to Kuratowski (or similar) is not possible and the existence of a pair type must be axiomatic ( per pair axiom). When used in programming languages, similar constructors are called record or struct , but their components usually have names instead of index numbers as with tuple coordinates. See also monads , lambda calculus §Typed lambda calculus , type constructors in the Haskell programming language .

literature

Bertrand Russell: Mathematical logic as based on the theory of types. (English; PDF; 1.9 MB), in: American Journal of Mathematics. 30, 1908, pp. 222-262 (in the web archive of 23 August 2014).
Álvaro Pelayo, Michael A. Warren: Homotopy type theory and Voevodsky's univalent foundations. (English; PDF), in: Bull. Amer. Math. Soc. (NS). 51, no. 4, 2014, pp. 597-648.

Web links

Type Theory (nLab)
Thierry Coquand: Type Theory. In: Edward N. Zalta (Ed.): Stanford Encyclopedia of Philosophy .
Christoph Benzmüller, Peter Andrews: Church's Type Theory. In: Edward N. Zalta (Ed.): Stanford Encyclopedia of Philosophy .
Peter Dybjer, Erik Palmgren: Intuitionistic Type Theory. In: Edward N. Zalta (Ed.): Stanford Encyclopedia of Philosophy .
http://glossar.hs-augsburg.de/Typentheorie for type theory

Individual evidence

^ Homotopy Type Theory: Univalent Foundations of Mathematics
↑ see PL / PostgreSQL
↑ at least if the basic types are different according to Russell's type hierarchy, with different type levels within the same hierarchy the pair representation can still be modified appropriately
↑ according to a feature logic

[1] Homotopy Type Theory: Univalent Foundations of Mathematics

[2] see PL / PostgreSQL

[3] t least if the basic types are different according to Russell's type hierarchy, with different type levels within the same hierarchy the pair representation can still be modified appropriately

[4] rding to a feature logic