Calculus Of Constructions

The CoC was initially developed by Thierry Coquand .

The CoC was the basis of the early versions of the Coq theorem prover; later versions were built upon the Calculus Of Inductive Constructions an extension of CoC with native support for inductive Datatype s. 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$ )

--- ( $orall x:A . B$ )

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

\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 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 dash A:B} \over {\Gamma' dash C:D}

which means

: If

\Gamma dash A:B

is a valid judgement, then so is

\Gamma' dash C:D

Inference rules for calculus of constructions

{\Gamma, x:A dash t : B : K \over 
{\Gamma dash (\lambda x:A . t) : (orall x:A . B) : K}}

{\Gamma dash M : (orall x:A . B)\qquad\qquad\Gamma
dash N : A \over 
{\Gamma dash M N : B(x := N)}}

Defining logical operators

The calculus of constructions is very parsimonious when it comes to basic operators: the only logical operator for forming propositions is

orall

. However, this one operator is sufficient to define all the other logical operators:

:

A \Rightarrow B\qquad\equiv\qquad orall x:A . B

(if

x 
otin B

)
:

A \wedge B\qquad\equiv\qquad orall C:P . 
(A \Rightarrow B \Rightarrow C) \Rightarrow C

A ee B\qquad\equiv\qquad orall C:P . 
(A \Rightarrow C) \Rightarrow (B \Rightarrow C) \Rightarrow C

eg A \qquad\equiv\qquad orall C:P . 
(A \Rightarrow C)

\exists x:A.B \qquad\equiv\qquad orall C:P . 
(orall x:A.(B \Rightarrow C)) \Rightarrow C

Defining data types

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

; Booleans :

orall A: P . A \Rightarrow A \Rightarrow A

; Naturals :

orall A:P . 
(A \Rightarrow A) \Rightarrow (A \Rightarrow A)

; Product

A 	imes B

A \wedge B

; Disjoint union

A + B

A ee B

	APPAREL
	BABY
	BEAUTY
	BOOKS
	CAR TOYS
	CELL PHONES
	DVD'S
	ELECTRONICS
	GOURMET FOOD
	GROCERIES
	HEALTH & PERSONAL
	HOME & GARDEN
	JEWELRY
	MUSIC
	MUSIC INSTRUMENTS
	OFFICE PRODUCTS
	SOFTWARE
	SPORTING GOODS
	TOOLS & HARDWARE
	TOYS
	VIDEO GAMES
	SHOPPING HOME

	MORE SHOPPING...

	CATEGORIES ABOUT CALCULUS OF CONSTRUCTIONS

	lambda calculus

	type theory

Information About

Calculus Of Constructions