Computer Aided Formal Reasoning Fall, 1995 Lecture notes 15 Judith Underwood

Extended Calculus of Constructions

To counteract the intensely practical nature of the last few lectures, we’ll do a bit of theory today. First, we’ll review (a slightly simplified version of) the Extended Calculus of Constructions, the base theory of Lego. Then, we’ll look at how the Calculus of Constructions can be viewed as an instance of a general framework.

This is a reasonably formal presentation of ECC, from Luo’s book. I’ve left out the Σ types for convenience.

⊢ P rop : T ype_{0}

{Γ ⊢ A : T ype_{j} \atop Γ, x:A ⊢ P rop : T ype_{0}} (x ∉ F V (Γ))

{Γ ⊢ P rop : T ype_{0} \atop Γ ⊢ T ype_{j} : T ype_{j+1}}

{Γ, x:A, Γ′ ⊢ P rop : T ype_{0} \atop Γ, x:A, Γ′ ⊢ x : A}

\begin{matrix}Γ ⊢ M : Πx:A.B & Γ ⊢ N : A \\ Γ ⊢ MN : B[N/x] \end{matrix}

\begin{matrix}Γ ⊢ M : A & Γ ⊢ A′ : T ype_{j} \\ Γ ⊢ M : A′ \end{matrix} (A ⪯ A′)

{Γ, x:A ⊢ P : P rop \atop Γ ⊢ Πx:A.P : P rop}

\begin{matrix}Γ ⊢ A : T ype_{j} & Γ, x:A ⊢ B : T ype_{j} \\ Γ ⊢ Πx:A.B : T ype_{j} \end{matrix}

{Γ, x:A ⊢ M : B \atop Γ ⊢ λx:A.M : Πx:A.B}

F V (Γ) is the set of free variables in Γ, and A ⪯ A′ means essentially that either A is equivalent to A′ under β-conversion, or A is contained in A′ by the universe ordering. When thinking about these rules, keep in mind that there is no real distinction between the variable x and the variable A – by convention we usually choose A as a name for a type, but they are both just variables.

Note that there is no axiom

Γ, x:A ⊢ x : A.

It (and the implicit structural rules which allow reordering of the hypotheses) is replaced by the first four rules as a collection. These rules describe precisely how contexts (the assumptions in Γ) are formed. Assumptions x : A are added to the context using the second rule, after a derivation which shows that A is a type.

Recall that Πx : A.B is {x:A}B in Lego, or A->B if B does not contain x, and λx : A.t is [x:A]t. The last three rules describe the formation of function types and the creation of elements of function types.

A sample derivation in this system is

{⊢ P rop : T ype_{0} \atop A:P rop ⊢ P rop : T ype_{0}} ; A:P rop ⊢ A : P rop ; A:P rop, x:A ⊢ P rop : T ype_{0} ; A:P rop, x:A ⊢ x : A ; A:P rop ⊢ λx:A.x : Πx:A.A

Exercise: Determine which rule is used at each step in this derivation.

Pure Type Systems

Let us now look at the following subsystem of ECC, using just the universes P rop and T ype_{0}.

⊢ P rop : T ype_{0}

{Γ ⊢ A : s \atop Γ, x:A ⊢ P rop : T ype_{0}} (x ∉ F V (Γ))

{Γ, x:A, Γ′ ⊢ P rop : T ype_{0} \atop Γ, x:A, Γ′ ⊢ x : A}

\begin{matrix}Γ ⊢ M : Πx:A.B & Γ ⊢ N : A \\ Γ ⊢ MN : B[N/x] \end{matrix}

\begin{matrix}Γ ⊢ M : A & Γ ⊢ A′ : s \\ Γ ⊢ M : A′ \end{matrix} (A ≅ A′)

\begin{matrix}Γ ⊢ A : s_{1} & Γ, x:A ⊢ B : s_{2} \\ Γ ⊢ Πx:A.B : s_{2} \end{matrix}

{Γ, x:A ⊢ M : B \atop Γ ⊢ λx:A.M : Πx:A.B} (B ≠ T ype_{0})

In these rules, s,s_{1} and s_{2} range over {P rop, T ype_{0}}. Here, A ≅ A′ means that A is equivalent to A′ under β-conversion.

This system differs from ECC above most obviously in the elimination of the universe hierarchy. In particular, there is no X for which we can form the expression T ype_{0} : X. The consequences of this are that we cannot form x : T ype_{0}, i.e. we cannot introduce variables ranging over T ype_{0} – we can only describe elements of it. Furthermore, using ≅ instead of ⪯ means that we cannot lift elements of P rop to elements of T ype_{0}.

This system is the Calculus of Constructions, introduced by Coquand and Huet. Let us reformulate this system in a slightly more abstract way, replacing the names P rop and T ype with ∗ and □. We will also make some slight modifications to the context building rules.

⊢ ∗ : □

{Γ ⊢ A : s \atop Γ, x:A ⊢ x : A} (x ∉ F V (Γ))

\begin{matrix}Γ ⊢ A : B & Γ ⊢ C : s \\ Γ, x:C ⊢ A : B \end{matrix} (x ∉ F V (Γ))

\begin{matrix}Γ ⊢ M : Πx:A.B & Γ ⊢ N : A \\ Γ ⊢ MN : B[N/x] \end{matrix}

\begin{matrix}Γ ⊢ M : A & Γ ⊢ A′ : s \\ Γ ⊢ M : A′ \end{matrix} (A ≅ A′)

\begin{matrix}Γ ⊢ A : s_{1} & Γ, x:A ⊢ B : s_{2} \\ Γ ⊢ Πx:A.B : s_{2} \end{matrix}

\begin{aligned}Γ ⊢ A : s_{1} & Γ, x:A ⊢ M : B & Γ, x:A ⊢ B : s_{2} \\ & Γ ⊢ λx:A.M : Πx:A.B \end{aligned}

In these rules, s, s_{1}, and s_{2} range over {∗, □}. We will rephrase this to say s ranges over {∗, □} and (s_{1}, s_{2}) ranges over {(∗, ∗), (∗, □), (□, ∗), (□, □)}.

We have modified the rules for constructing contexts, though not in a significant way. The first new rule is just a combination of the first two old rules, and the second new rule can be mimicked by appropriate use of the old rules. The advantage in this formulation is that it avoids using P rop : T ype_{0} as a placeholder signifying that the context is well-formed.

Apart from the context rules, the only significant different is in the final rule, where the restriction that B cannot be T ype_{0} is expressed as the requirement that B : s_{2} for some s_{2}. The implicit requirement that A cannot be T ype_{0} is also made explicit.

This is a pure type system description of the calculus of constructions. The advantage in this presentation is that subsystems can be described in a very easy and elegant way.

Subsystems of CC

If we think of ∗ as the “type of terms” and □ as the “type of types”, we can think of the pairs (s_{1}, s_{2}) as describing possible dependencies between terms and types.

For example, the simply typed λ calculus is the above system with (s_{1}, s_{2}) restricted to (∗, ∗). This describes the fact that in λ-calculus, terms can depend on other terms (i.e. λ-terms are functions from terms to terms) but no other dependencies exist. Similarly, adding (∗, □) allows types which depend on terms (dependent Π types) and adding (□, ∗) allows terms which depend on types (polymorphic functions). Adding (□, □) allows types which depend on types (type functions). Given (∗, ∗) as a base, all of the other additions are independent, and the resulting systems form the λ-cube (due to Barendregt).

Credits

The rules for ECC are lifted from Computation and Reasoning, by Zhaohui Luo, as is the specialization to CC. The Pure Type System presentation of CC is from Barendregt, Introduction to Generalised Type Systems in the Journal of Functional Programming. A similar treatment can be found in Barendregt’s article Lambda calculi with types, in the Handbook of Logic in Computer Science (volume 2).