
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 higherorder 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 MartinLöf's Intuitionistic type theory, JeanYves 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) 
Breadthfirst search 
Chaitin's constant 
Algebraic structure 
Linear combination 
Fuzzy logic 
Wiener process 
Ideal class group 
Dijkstra's algorithm 
IEEE 7541985 
Elliptic curve 
Sequence 
Euler characteristic 
Gaussian quadrature 
Euclidean space 
Natural transformation 
