Calculus of constructions

From Wikipedia, the free encyclopedia
  (Redirected from Calculus of Constructions)
Jump to: navigation, search

The Calculus of Constructions (CoC) is a significant 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 derivatives have been the basis for Coq and other proof assistants.

Its derivatives include:

  • Calculus of Inductive Constructions ("CiC") - added inductive types
  • Calculus of (Co)Inductive Constructions ("CciC") - added Coinduction
  • predicative Calculus of Inductive Constructions ("pCiC") - removed some impredicativity

General traits[edit]

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, say, integers to types, types to types as well as functions from integers to integers.

The CoC is strongly normalizing, although, by Gödel's incompleteness theorem, it is impossible to prove this property within the CoC since it implies consistency.

Usage[edit]

The CoC has developed alongside the Coq proof assistant. As features were added (or possible liabilities removed) to the theory, they became available in Coq.

Derivatives of the CoC are used in other proof assistants, such as Matita.

The basics of the calculus of constructions[edit]

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

Terms[edit]

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 are
    • ( A~B )
    • (\mathbf{\lambda}x:A . B)
    • (\forall x:A . B)

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[edit]

The calculus of constructions allows proving typing judgments:

 x_1:A_1, x_2:A_2, \ldots \vdash t:B

Which can be read as the implication

If variables x_1, x_2, \ldots have types A_1, A_2, \ldots, 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, \ldots , and we use K to mean either P or T. We shall write  A : B :C to mean "A has type B, and B has type C". We shall 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

 {\Gamma \vdash A:B} \over {\Gamma' \vdash C:D}

which means

If  \Gamma \vdash A:B is a valid judgment, then so is  \Gamma' \vdash C:D

Inference rules for the calculus of constructions[edit]

1.  {{} \over {} \Gamma \vdash P : T}

2.  {\Gamma \vdash A : K \over 
{\Gamma, x:A \vdash x : A}}

3.  {\Gamma, x:A \vdash t : B : K \over 
{\Gamma \vdash (\lambda x:A . t) : (\forall x:A . B) : K}}

4.  {\Gamma \vdash M : (\forall x:A . B)\qquad\qquad\Gamma
\vdash N : A \over 
{\Gamma \vdash M N : B(x := N)}}

5.  {\Gamma \vdash M : A \qquad \qquad A =_\beta B \qquad \qquad B : K 
\over {\Gamma \vdash M : B}}

Defining logical operators[edit]

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


\begin{matrix}
A \Rightarrow B & \equiv & \forall x:A . B & (x \notin B) \\
A \wedge B      & \equiv & \forall C:P . (A \Rightarrow B \Rightarrow C) \Rightarrow C & \\
A \vee B        & \equiv & \forall C:P . (A \Rightarrow C) \Rightarrow (B \Rightarrow C) \Rightarrow C & \\
\neg A          & \equiv & \forall C:P . (A \Rightarrow C) & \\
\exists x:A.B   & \equiv & \forall C:P . (\forall x:A.(B \Rightarrow C)) \Rightarrow C &
\end{matrix}

Defining data types[edit]

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

Booleans 
\forall A: P . A \Rightarrow A \Rightarrow A
Naturals 
\forall A:P . 
(A \Rightarrow A) \Rightarrow (A \Rightarrow A)
Product A \times B 
A \wedge B
Disjoint union A + B 
A \vee B

Note that Booleans and Naturals are defined in the same way as in Church encoding. However additional problems raise from propositional extensionality and proof irrelevance [1].

See also[edit]

Theorists[edit]

References[edit]