Calculus of constructions: Encyclopedia II - Calculus of constructions - The basics of the calculus of constructions

Calculus of constructions - 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 (which we will also call "propositions").

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)
• If A and B are terms, then so are
  • ()
  • ()

The calculus of constructions has 4 types 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.

Calculus of constructions - Judgements

In the calculus of constructions, a judgement is a typing inference:

Which can be read as the implication

The valid judgements 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 , and we use K to mean either P or T. We will write A:B:C to mean "A has type B, and B has type C". We will write B(x: = N) to mean the result of substituting the term N for the variable x in the term B.

An inference rule is written in the form

which means

Calculus of constructions - Inference rules for calculus of constructions

Calculus of constructions - Defining logical operators

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

Calculus of constructions - Defining data types

The basic data types used in computer science can be defined within the Calculus of Constructions:

Adapted from the Wikipedia article "The basics of the calculus of constructions", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki