nLab
pure type system

Idea

A pure type system is an explicitly typed lambda calculus using dependent product as the type of lambda expressions: the basic idea is that

$$\Gamma ,x:A⊢B:C$$\Gamma, x:A \vdash B:C

implies

$$\Gamma ⊢(\lambda x:A.B):(\prod x:A.C).$$\Gamma \vdash (\lambda x:A . B) : (\prod x:A . C).

In other words a pure type system is

1. a system of natural deduction;

2. for dependent types;

3. and with (only) the dependent product type formation rule specified.

Definition

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)$.

Remark

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$.

Remark

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

1. The terms of a pure type system are the following (recursive definition):

   • variables and constants
   • $(\lambda x:A.B)$ (abstraction)
   • $(\prod x:A.B)$ (product)
   • $AB$ (application)

   Here $x$ is a variable and $A$, $B$ are terms. The operators $\lambda$ and $\prod$ bind the variable $x$.

2. The typing of terms is inductively defined by the following rules.

   A typing is of the form

   $$x_1:A_1,\dots ,x_n:A_n⊢A:B$$x_{1} : A_{1}, \dots, x_{n} : A_{n} \vdash A : B

   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 ⊢c:s$	if $(c:s)$ is an axiom;
(start)	$\frac{\Gamma ⊢A:s}{\Gamma ,x:A⊢x:A}$	if $x\notin \Gamma$
(weakening)	$\frac{\Gamma ⊢A:B;\Gamma ⊢C:s}{\Gamma ,x:C⊢A:B}$	if $x\notin \Gamma$
(product)	$\frac{\Gamma ⊢A:s_1;\Gamma x:A⊢B:s_2}{\Gamma ⊢(\prod x:A.B):s_3}$	if $(s_1,s_2.s_3)\in R$;
(application)	$\frac{\Gamma ⊢F:(\prod x:A.B);\Gamma ⊢a:A}{\Gamma ⊢\mathrm{Fa}:B[x:=a]}$
(abstraction)	$\frac{\Gamma ,x:A⊢b:B;\Gamma ⊢(\prod x:A.B):s}{\Gamma ⊢(\lambda x:A:b):(\prod x:A:B)}$
(conversion)	$\frac{\Gamma ⊢A:B;\Gamma ⊢B\prime :s;B{=}_{\beta }B\prime }{\Gamma ⊢A:B\prime }$

Examples

Strongly normalizing systems

Intuitionistic (higher-order) logic

Lambda cube

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=$	$\{*,\square \}$
$A=$	$\{(*:\square )\}$
$R=$	$\{(*,*),(*,\square ),(\square ,*),(\square ,\square )\}$

(Here $\{*,\square \}$ denotes the 2-element set.)

The other systems omit some of the last three relations. Some specific systems are the following:

name	$(*,*)$	$(*,\square )$	$(\square ,*)$	$(\square ,\square )$
$\lambda \to$ simply typed lambda calculus	yes
$\lambda P$ logical framework	yes	yes
$\lambda 2$ system F?	yes		yes
$\lambda \underline{\omega }$	yes			yes
$\lambda C$ calculus of constructions	yes	yes	yes	yes

Calculus of constructions

For instance for the calculus of constructions we have

• $*=$ Prop, the type of propositions

• $\square =$ Type, the type of types.

The single axiom $*:\square$ hence says that $\mathrm{Prop}:\mathrm{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.

Inconsistent systems

The most permissive pure type system:

symbol	actual value
$S=$	$\{*\}$
$A=$	$\{(*:*)\}$
$R=$	$\{(*,*)\}$

But there is an example with even non-circular system of axioms:

symbol	actual value
$S=$	$\{*,\square ,▵\}$
$A=$	$\{(*:\square ),(\square :▵)\}$
$R=$	$\{(*,*),(\square ,*),(\square ,\square ),(▵,\square )\}$

Related concepts

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.

References

• 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

A quick survey is in

• Frade, Calculus of inductive constructions (pdf)