|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
In other words a pure type system is
a system of natural deduction;
for dependent types;
A pure type system is defined by
a set of sorts, all of which are constants,
a set of axioms of the form with a constant and a sort,
a set of rules: triples of sorts.
Rules are abbreviated as .
In fact all rules appearing in the following have . So we can just as well regard as a binary relation (rather than a ternary one).
From the above input data we derive the following
The terms of a pure type system are the following (recursive definition):
Here is a variable and , are terms. The operators and bind the variable .
The typing of terms is inductively defined by the following rules.
A typing is of the form
meaning that the types of the variables declared on the left induces the term has type . Note that types are also terms.
The order of variable declarations is significant: the declaration may depend on declarations to its left.
The natural deduction rules are defined to be the following, for all and where ranges over the set of variables.
|(axioms)||if is an axiom;|
The lambda cube (Barendregt 91) consists of eight systems arranged in a cube. The most expressive is given by the following choice of sorts, axioms and rules:
(Here denotes the 2-element set, see Barendregt 91, 2.1)
The other systems omit some of the last three rules. Some specific systems are the following:
|simply typed lambda calculus||yes|
|calculus of constructions||yes||yes||yes||yes|
For instance for the calculus of constructions we have
The rules express the usual rule for dependent product type:
a dependent product over a generic dependent type is itself some type;
The most permissive pure type system:
But there is an example with even non-circular system of axioms (System ):
Pure type systems can be augmented with a cumulativity relation between sorts, so that if , then any type in is also in ; see Barras-Gregoire.
Henk Barendregt, Introduction to generalized type systems, J. Funct. Program. 1(2), 1991 (pdf)
Henk Barendregt (Catholic University Nijmegen), Lambda calculi with types?, To appear in Samson Abramsky, D.M. Gabbay and T.S.E. Maibaum (eds.) Handbook of Logic in Computer Science, Volume II, Oxford University Press. (preprint pdf)
Frade, Calculus of inductive constructions (pdf)
A generalization to cumulativity can be found in