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
basic constructions:
strong axioms
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 relations: triples $(s_{1}, s_{2}, s_{3})$ of sorts. Relations $(s_{1}, s_{2}, s_{2})$ are abbreviated as $(s_{1}, s_{2})$.
These relations 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 such triples appearing in the following have $s_2 = s_3$. So we can just as well regard them as binary relations $R \hookrightarrow S\times S$ (rather than ternary ones).
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) | $\Gamma \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 consists of eight systems arranged in a cube. The most expressive is given by the following choice of sorts, axioms and relations:
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.)
The other systems omit some of the last three relations. 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 relations express the usual rule for dependent product type:
a dependent product over a generic dependent type is itself some type;
but if the dependent product is over a proposition then it is in fact itself a proposition, namely the universal quantification of the given definition.
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:
symbol | actual value |
---|---|
$S =$ | $\{ \ast, \square, \triangle\}$ |
$A =$ | $\{(\ast : \square), (\square : \triangle)\}$ |
$R =$ | $\{(\ast, \ast), (\square, \ast), (\square, \square), (\triangle, \square)\}$ |
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 introduing inductive types.
A quick survey is in