Calculus of Constructions

The Calculus of Constructions is a type of lambda calculus. As such, it hard to understand for people who are unfamiliar with lambda calculus (which constitutes the vast majority of our team), and there are not many good resource for learning it. I also believe that at this early stage of our project, it would be overkill to implement it right now; thus, I do not recommend that we adopt the Calculus of Constructions in our application. Nevertheless, I have documented the basics of this system below.

The following is a condensed description of the Calculus of Constructions (Source: https://en.wikipedia.org/wiki/Calculus_of_constructions).

Terms

A term in the calculus of constructions is constructed using the following rules:

• T is a term (also called Type);
• P is a term (also called Prop, the type of all propositions);
• Variables (x, y, ...) are terms;
• If A and B are terms, then so is (A B);
• If A and B are terms and x is a variable, then the following are also terms:
  • (λx:A . B),
  • (∀x:A . B).

Objects 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 (P is an example of a large type);
5. T itself, which is the type of large types.

Judgments The calculus of constructions allows proving typing judgments:

Which can be read as the implication

If variables x_1, x_2 have types A_1, A_2, then term t has type B.

The valid judgments for the calculus of constructions are derivable from a set of inference rules. In the following, we use Gamma to mean a sequence of type assignments x_1: A_1, x_2 : A_2,... and we use K to mean either P or T. We shall write

to mean the result of substituting the term N for the free variable x in the term B.

An inference rule is written in the form

which means

If is a valid judgment, then so is .

Inference Rules

1. 
2. 
3. 
4. 
5. 

Logical Operators

Data Types

Booleans:

Naturals:

Product A x B:

Disjoint union A + B: