Calculus of constructions


In mathematical logic and computer science, the calculus of constructions is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, the CoC and its variants have been the basis for Rocq and other proof assistants.
Some of its variants include the calculus of inductive constructions, the calculus of inductive constructions, and the predicative calculus of inductive constructions.

General traits

The CoC is a higher-order typed lambda calculus, initially developed by Thierry Coquand. It is well known for being at the top of Barendregt's lambda cube. It is possible within CoC to define functions from terms to terms, terms to types, types to types, and from types to terms.
The CoC is strongly normalizing, and hence consistent.

Usage

The CoC has been developed alongside the Rocq proof assistant. As features were added to the theory, they became available in Rocq.
Variants of the CoC are used in other proof assistants, such as Matita and Lean.

The basics of the calculus of constructions

The calculus of constructions can be considered an extension of the Curry–Howard isomorphism. The Curry–Howard isomorphism associates a term in the simply typed lambda calculus with each natural-deduction proof in intuitionistic propositional logic. The calculus of constructions extends this isomorphism to proofs in the full intuitionistic predicate calculus, which includes proofs of quantified statements.

Terms

A term in the calculus of constructions is constructed using the following rules:
  • is a term ;
  • is a term ;
  • Variables are terms;
  • If and are terms, then so is ;
  • If and are terms and is a variable, then the following are also terms:
  • *,
  • *.
In other words, the term syntax, in Backus–Naur form, is then:
The calculus of constructions has five kinds of objects:
  1. proofs, which are terms whose types are propositions;
  2. propositions, which are also known as small types;
  3. predicates, which are functions that return propositions;
  4. large types, which are the types of predicates ;
  5. itself, which is the type of large types.

    β-equivalence

As with the untyped lambda calculus, the calculus of constructions uses a basic notion of equivalence of terms, known as -equivalence. This captures the meaning of -abstraction:
-equivalence is a congruence relation for the calculus of constructions, in the sense that
  • If and, then.

    Judgments

The calculus of constructions allows proving typing judgments:
which can be read as the implication
The valid judgments for the calculus of constructions are derivable from a set of inference rules. In the following, we use to mean a sequence of type assignments
; to mean terms; and to mean either or. We shall write to mean the result of substituting the term for the free variable in the term.
An inference rule is written in the form
which means

Inference rules for the calculus of constructions

1.
2.
3.
4.
5.
6.

Defining logical operators

The calculus of constructions has very few basic operators: the only logical operator for forming propositions is. However, this one operator is sufficient to define all the other logical operators:

Defining data types

The basic data types used in computer science can be defined within the calculus of constructions:
; Booleans :
; Naturals :
; Product :
; Disjoint union :
Booleans and Naturals are defined in the same way as in Church encoding. However, added problems arise from propositional extensionality and proof irrelevance.