natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
logic | category theory | type theory |
---|---|---|
true | terminal object/(-2)-truncated object | h-level 0-type/unit type |
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language
</table>
basic constructions:
strong axioms
further
A pure type system is an explicitly typed lambda calculus using dependent product as the type of lambda expressions: the basic idea is that
implies
In other words a pure type system is
a system of natural deduction;
for dependent types;
and with (only) the dependent product type formation rule specified.
A pure type system is defined by
a set $S$ of sorts, all of which are constants,
a set $A$ of axioms of the form $c : s$ with $c$ a constant and $s$ a sort,
a set $R \hookrightarrow S \times S \times S$ of rules: triples $(s_{1}, s_{2}, s_{3})$ of sorts.
Rules $(s_{1}, s_{2}, s_{2})$ are abbreviated as $(s_{1}, s_{2})$.
These rules will appear in the type formation rule for dependent product types below. They will say that for a type of sort $s_2$ depending on a type of sort $s_1$ its dependent product is a type of sort $s_3$.
In fact all rules $(s_{1}, s_{2}, s_{2})$ appearing in the following have $s_2 = s_3$. So we can just as well regard $R$ as a binary relation $R \hookrightarrow S\times S$ (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 $x$ is a variable and $A$, $B$ are terms. The operators $\lambda$ and $\prod$ bind the variable $x$.
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 $A$ has type $B$. Note that types are also terms.
The order of variable declarations is significant: the declaration $x_{i} : A_{i}$ may depend on declarations to its left.
The natural deduction rules are defined to be the following, for all $s \in S$ and where $x$ ranges over the set of variables.
name | rule | condition |
---|---|---|
(axioms) | $\vdash c : s$ | if $(c : s)$ is an axiom; |
(start) | $\frac{\Gamma \vdash A:s}{\Gamma, x : A \vdash x : A}$ | if $x \notin \Gamma$ |
(weakening) | $\frac{\Gamma \vdash A:B; \quad \Gamma \vdash C:s}{\Gamma, x : C \vdash A : B}$ | if $x \notin \Gamma$ |
(product) | $\frac{\Gamma \vdash A : s_{1}; \quad \Gamma x:A \vdash B : s_{2}}{\Gamma \vdash (\prod x:A . B) : s_{3}}$ | if $(s_{1}, s_{2}. s_{3}) \in R$; |
(application) | $\frac{\Gamma \vdash F : (\prod x:A . B); \quad \Gamma \vdash a : A}{\Gamma \vdash Fa : B [x := a]}$ | |
(abstraction) | $\frac{\Gamma, x:A \vdash b : B; \quad \Gamma \vdash (\prod x:A . B) : s}{\Gamma \vdash (\lambda x:A.b) : (\prod x:A.B)}$ | |
(conversion) | $\frac{\Gamma \vdash A : B; \quad \Gamma \vdash B' : s; \quad B =_{\beta} B'}{\Gamma \vdash A : B'}$ |
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:
symbol | actual value |
---|---|
$S =$ | $\{\ast, \square\}$ |
$A =$ | $\{(\ast : \square)\}$ |
$R =$ | $\{(\ast, \ast), (\ast, \square), (\square, \ast), (\square, \square)\}$ |
(Here $\{\ast, \Box\}$ 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:
name | $(\ast, \ast)$ | $(\ast, \square)$ | $(\square, \ast)$ | $(\square, \square)$ |
---|---|---|---|---|
$\lambda\rightarrow$ simply typed lambda calculus | yes | |||
${\lambda}P$ logical framework | yes | yes | ||
$\lambda2$ system F? | yes | yes | ||
$\lambda\underline{\omega}$ | yes | yes | ||
${\lambda}C$ calculus of constructions | yes | yes | yes | yes |
For instance for the calculus of constructions we have
$* =$ Prop, the type of propositions
$\Box =$ Type, the type of types.
The single axiom $* \colon \Box$ hence says that $Prop \colon Type$, hence that Prop is a type.
The rules express the usual rule for dependent product type:
a dependent product over a generic dependent type is itself some type;
but the dependent product of a dependent proposition is itself a proposition, namely the universal quantification.
The most permissive pure type system:
symbol | actual value |
---|---|
$S =$ | $\{\ast\}$ |
$A =$ | $\{(\ast : \ast)\}$ |
$R =$ | $\{(\ast, \ast)\}$ |
But there is an example with even non-circular system of axioms (System $\mathsf{U}^-$):
symbol | actual value |
---|---|
$S =$ | $\{ \ast, \square, \triangle\}$ |
$A =$ | $\{(\ast : \square), (\square : \triangle)\}$ |
$R =$ | $\{(\ast, \ast), (\square, \ast), (\square, \square), (\triangle, \square)\}$ |
Pure type systems can be augmented with a cumulativity relation between sorts, so that if $s_1 \preceq s_2$, then any type in $s_1$ is also in $s_2$; see Barras-Gregoire.
The calculus of inductive constructions can be formulated as a particular pure type system (with a hierarchy of type of types) augmented by rules for introducing inductive types.
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)
Survey includes
Frade, Calculus of inductive constructions (pdf)
Cody Roux, Pure type systems: Dependents when you need them, talk at Boston Haskell Meetup 2015 (slides,video)
A generalization to cumulativity can be found in
Last revised on May 12, 2018 at 06:13:17. See the history of this page for a list of all contributions to it.