mjhjmtu

In mathematical logic and computer science, the calculus of constructions (CoC) is a 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 variants have been the basis for Coq and other proof assistants.

Some of its variants include the calculus of inductive constructions^[1] (which adds inductive types),
the calculus of (co)inductive constructions (which adds coinduction),
and the predicative calculus of inductive constructions (which removes some impredicativity).

General traits

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 integers to integers, as well as integers to types, types to types, and types 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 inconsistency.

Usage

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

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

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);


• 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 following are also terms:
  
  • (λx:A . B),
  
  
  • (∀x:A . B).
  
  

In other words, the term syntax, in BNF, is then:

e::=T∣P∣x∣ee∣λx:e.e∣∀x:e.edisplaystyle e::=mathbf T mid mathbf P mid xmid e,emid lambda xmathbin :e.emid forall xmathbin :e.e

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:

x1:A1,x2:A2,…⊢t:Bdisplaystyle x_1:A_1,x_2:A_2,ldots vdash t:B

Which can be read as the implication

If variables x1,x2,…displaystyle x_1,x_2,ldots have types A1,A2,…displaystyle A_1,A_2,ldots , then term tdisplaystyle t has type Bdisplaystyle B.

The valid judgments for the calculus of constructions are derivable from a set of inference rules. In the following, we use Γdisplaystyle Gamma to mean a sequence of type assignments
x1:A1,x2:A2,…displaystyle x_1:A_1,x_2:A_2,ldots , and we use K to mean either P or T. We shall write B[x:=N]displaystyle B[x:=N] to mean the result of substituting the term
Ndisplaystyle N for the free variable xdisplaystyle x in
the term Bdisplaystyle B.

An inference rule is written in the form

Γ⊢A:BΓ′⊢C:Ddisplaystyle Gamma vdash A:B over Gamma 'vdash C:D

which means

If Γ⊢A:Bdisplaystyle Gamma vdash A:B is a valid judgment, then so is Γ′⊢C:Ddisplaystyle Gamma 'vdash C:D

Inference rules for the calculus of constructions

1. Γ⊢P:Tdisplaystyle over Gamma vdash P:T

2. Γ⊢A:KΓ,x:A⊢x:Adisplaystyle Gamma vdash A:K over Gamma ,x:Avdash x:AGamma, x:A vdash x : A "/>

3. Γ,x:A⊢B:KΓ,x:A⊢N:BΓ⊢(λx:A.N):(∀x:A.B):Kdisplaystyle Gamma ,x:Avdash B:Kqquad qquad Gamma ,x:Avdash N:B over Gamma vdash (lambda x:A.N):(forall x:A.B):K

4. Γ⊢M:(∀x:A.B)Γ⊢N:AΓ⊢MN:B[x:=N]displaystyle Gamma vdash M:(forall x:A.B)qquad qquad Gamma vdash N:A over Gamma vdash MN:B[x:=N]

5. Γ⊢M:AA=βBB:KΓ⊢M:Bdisplaystyle Gamma vdash M:Aqquad qquad A=_beta Bqquad qquad B:K over Gamma vdash M:Bover Gamma vdash M : B "/>

Defining logical operators

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

A⇒B≡∀x:A.B(x∉B)A∧B≡∀C:P.(A⇒B⇒C)⇒CA∨B≡∀C:P.(A⇒C)⇒(B⇒C)⇒C¬A≡∀C:P.(A⇒C)∃x:A.B≡∀C:P.(∀x:A.(B⇒C))⇒Cdisplaystyle beginarrayccllARightarrow B&equiv &forall x:A.B&(xnotin B)\Awedge B&equiv &forall C:P.(ARightarrow BRightarrow C)Rightarrow C&\Avee B&equiv &forall C:P.(ARightarrow C)Rightarrow (BRightarrow C)Rightarrow C&\neg A&equiv &forall C:P.(ARightarrow C)&\exists x:A.B&equiv &forall C:P.(forall x:A.(BRightarrow C))Rightarrow C&endarray

Defining data types

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

Booleans 

∀A:P.A⇒A⇒Adisplaystyle forall A:P.ARightarrow ARightarrow A

Naturals 

∀A:P.(A⇒A)⇒(A⇒A)displaystyle forall A:P.(ARightarrow A)Rightarrow (ARightarrow A)(A Rightarrow A) Rightarrow (A Rightarrow A)"/>

Product A×Bdisplaystyle Atimes B 

A∧Bdisplaystyle Awedge B

Disjoint union A+Bdisplaystyle A+B 

A∨Bdisplaystyle Avee B

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

See also

• Pure type system


• Lambda cube


• System F


• Dependent type


• Intuitionistic type theory


• Homotopy type theory

References

• 
  Coquand, Thierry; Huet, Gérard (1988). "The Calculus of Constructions". Information and Computation. 76 (2–3): 95–120. doi:10.1016/0890-5401(88)90005-3..mw-parser-output cite.citationfont-style:inherit.mw-parser-output .citation qquotes:"""""""'""'".mw-parser-output .citation .cs1-lock-free abackground:url("//upload.wikimedia.org/wikipedia/commons/thumb/6/65/Lock-green.svg/9px-Lock-green.svg.png")no-repeat;background-position:right .1em center.mw-parser-output .citation .cs1-lock-limited a,.mw-parser-output .citation .cs1-lock-registration abackground:url("//upload.wikimedia.org/wikipedia/commons/thumb/d/d6/Lock-gray-alt-2.svg/9px-Lock-gray-alt-2.svg.png")no-repeat;background-position:right .1em center.mw-parser-output .citation .cs1-lock-subscription abackground:url("//upload.wikimedia.org/wikipedia/commons/thumb/a/aa/Lock-red-alt-2.svg/9px-Lock-red-alt-2.svg.png")no-repeat;background-position:right .1em center.mw-parser-output .cs1-subscription,.mw-parser-output .cs1-registrationcolor:#555.mw-parser-output .cs1-subscription span,.mw-parser-output .cs1-registration spanborder-bottom:1px dotted;cursor:help.mw-parser-output .cs1-ws-icon abackground:url("//upload.wikimedia.org/wikipedia/commons/thumb/4/4c/Wikisource-logo.svg/12px-Wikisource-logo.svg.png")no-repeat;background-position:right .1em center.mw-parser-output code.cs1-codecolor:inherit;background:inherit;border:inherit;padding:inherit.mw-parser-output .cs1-hidden-errordisplay:none;font-size:100%.mw-parser-output .cs1-visible-errorfont-size:100%.mw-parser-output .cs1-maintdisplay:none;color:#33aa33;margin-left:0.3em.mw-parser-output .cs1-subscription,.mw-parser-output .cs1-registration,.mw-parser-output .cs1-formatfont-size:95%.mw-parser-output .cs1-kern-left,.mw-parser-output .cs1-kern-wl-leftpadding-left:0.2em.mw-parser-output .cs1-kern-right,.mw-parser-output .cs1-kern-wl-rightpadding-right:0.2em
  


• Also available freely accessible online: Coquand, Thierry; Huet, Gérard (1986). "The calculus of constructions". Technical Report 530. INRIA, Centre de Rocquencourt. Note terminology is rather different. For instance, (∀x:A.Bdisplaystyle forall x:A.B) is written [x : A] B.


• 
  Bunder, M. W.; Seldin, Jonathan P. (2004). "Variants of the Basic Calculus of Constructions". CiteSeerX 10.1.1.88.9497.
  


• 
  Frade, Maria João (2009). "Calculus of Inductive Constructions" (talk).
  


• 
  Gérard Huet (1988). K. Fuchi and M. Nivat, ed. Induction Principles Formalized in the Calculus of Constructions (PDF). North-Holland. pp. 205–216. — An application of the CoC