Type theory

related topics
{math, number, function}
{theory, work, human}
{rate, high, increase}
{law, state, case}
{group, member, jewish}
{son, year, death}

In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general. In programming language theory, a branch of computer science, type theory can refer to the design, analysis and study of type systems, although some computer scientists limit the term's meaning to the study of abstract formalisms such as typed λ-calculi.

Bertrand Russell invented the first type theory in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox. This theory of types features prominently in Whitehead and Russell's Principia Mathematica. It avoids Russell's paradox by first creating a hierarchy of types, then assigning each mathematical (and possibly other) entity to a type. Objects of a given type are built exclusively from objects of preceding types (those lower in the hierarchy), thus preventing loops.

Alonzo Church, inventor of the lambda calculus, developed a higher-order logic commonly called Church's Theory of Types,[1] in order to avoid the Kleene–Rosser paradox afflicting the original pure lambda calculus. Church's type theory is a variant of the lambda calculus in which expressions (also called formulas or λ-terms) are classified into types, and the types of expressions restrict the ways in which they can be combined. In other words, it is a typed lambda calculus. Today many other such calculi are in use, including Per Martin-Löf's Intuitionistic type theory, Jean-Yves Girard's System F and the Calculus of Constructions. In typed lambda calculi, types play a role similar to that of sets in set theory.

Contents

Full article ▸

related documents
Factorization
Linear independence
Glossary of topology
Euclidean algorithm
Heine–Borel theorem
Axiom schema of replacement
Pushdown automaton
Presentation of a group
Probability density function
Binary relation
Abstract interpretation
Homology (mathematics)
Random variable
Goldbach's conjecture
E (mathematical constant)
Breadth-first search
Chaitin's constant
Algebraic structure
Linear combination
Fuzzy logic
Wiener process
Ideal class group
Dijkstra's algorithm
IEEE 754-1985
Elliptic curve
Sequence
Euler characteristic
Gaussian quadrature
Euclidean space
Natural transformation