Calculus of constructions

This article needs attention from an expert on the subject. See the talk page for details. WikiProject Computer science or the Computer science Portal may be able to help recruit an expert. (November 2008)

The calculus of constructions (CoC) is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.

1 General traits
2 The basics of the calculus of constructions
3 See also
- 3.1 Theorists
4 References

General traits

The CoC is a higher-order typed lambda calculus, initially developed by Thierry Coquand, where types are first-class values. It is thus possible, within the CoC, to define functions from, say, integers to types, types to types as well as functions from integers to integers. Within Barendregt's lambda cube, it is therefore the richest calculus.

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

The CoC was the basis of the early versions of the Coq proof assistant; later versions were built upon the Calculus of inductive constructions, an extension of CoC with native support for inductive datatypes. In the original CoC, inductive datatypes had to be emulated as their polymorphic destructor function.

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

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

The calculus of constructions has five kinds of objects:

proofs, which are terms whose types are propositions
propositions, which are also known as small types
predicates, which are functions that return propositions
large types, which are the types of predicates. (P is an example of a large type)
T itself, which is the type of large types.

Judgements

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

$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 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 $x_1:A_1, x_2:A_2, \ldots$ , 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

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

which means

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

Inference rules for calculus of constructions

1. ${{} \over {} \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

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

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$

References

Thierry Coquand and Gerard Huet: The Calculus of Constructions. Information and Computation, Vol. 76, Issue 2-3, 1988.
For a source freely accessible online, see Coquand and Huet: The calculus of constructions. Technical Report 530, INRIA, Centre de Rocquencourt, 1986. Note terminology is rather different. For instance, ( $\forall x:A . B$ ) is written [x : A] B.
M. W. Bunder and Jonathan P. Seldin: Variants of the Basic Calculus of Constructions. 2004.

Calculus of constructions

  WikiTude Home

  Celebrity Directory
  Celebrity Pictures
  Celebrity Desktop
  Celebrity Screensavers
  Celebrity Wallpapers
  Celebrity Music Videos
  Song Lyrics
  Celebrity News
  Celebrity Bios
  Celebrity Posters
  Celebrity Movies
  Celebrity Music
  Celebrity Books
  Celebrity Videos
  Latest Celebrity Photos
  Celebrity Candids
  Celebrity Unofficial
  Celebrity Pics
  Celebrity Feet Pics
  Celebrity Video Clips
  Celebrity Articles
  Celebrity Blogs
  Celebrity eBay
  Celebrity Gossip
  Celebrity Photos
  Celebrity YouTube
  Video Celebrity News

  Contact Celebrities
  Celebrity Games
  Celebrity Popularity
  Celebrity
  Celebrity Websites

  Music
  Movies
  Web Portal
  POPped NEWS
  Books
  Games
  Flash Games
  Mortgages
  News Blog
  Quotes
  Travel
  TV Listings
  Tools & Gadgets
  Web Owner Tools

Calculus of constructions