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 terms to terms, as well as terms to types, types to types, and types to terms.
The CoC is strongly normalizing, although it is impossible to prove this property within the CoC since it implies consistency, which by Gödel's incompleteness theorem is impossible to prove from within the system itself.
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:
\( \mathbf {T} \) is a term (also called Type);
\( \ \mathbf {P} \) is a term (also called Prop, the type of all propositions);
Variables ( \( \ {\displaystyle x,y,\ldots } \) ) are terms;
If A A and B are terms, then so is \( \ {\displaystyle (AB)} \);
If A {\displaystyle A} A and B are terms and x is a variable, then the following are also terms:
\( \{\displaystyle (\lambda x:A.B)} \) ,
\( \ {\displaystyle (\forall x:A.B)} \) .
In other words, the term syntax, in BNF, is then:
\( \ {\displaystyle e::=\mathbf {T} \mid \mathbf {P} \mid x\mid e\,e\mid \lambda x{\mathbin {:}}e.e\mid \forall x{\mathbin {:}}e.e} \)
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 ( \( \ \mathbf {P} \) is an example of a large type);
\( \ \mathbf {T} \) itself, which is the type of large types.
Judgments
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 \) ; A,B,C,D to mean terms; and \( {\displaystyle K,L}\) to mean either \( \ \mathbf {P} \) or \( \ \mathbf {T} \). We shall write \( \ {\displaystyle B[x:=N]} \) to mean the result of substituting the term N for the free 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
1. \( \ {\displaystyle {{} \over \Gamma \vdash \mathbf {P} :\mathbf {T} }} \)
2. \( \ {\displaystyle {{} \over {\Gamma ,x:A,\Gamma '\vdash x:A}}} \)
3. \( \{\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash B:L \over {\Gamma \vdash (\forall x:A.B):L}}} \)
4. \( \ {\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:A.N):(\forall x:A.B)}}} \)
5. \( \ {\displaystyle {\Gamma \vdash M:(\forall x:A.B)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B[x:=N]}}} \)
6. Γ \( \ {\displaystyle {\Gamma \vdash M:A\qquad \qquad A=_{\beta }B\qquad \qquad \Gamma \vdash 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:
\( \ {\displaystyle {\begin{array}{ccll}A\Rightarrow B&\equiv &\forall x:A.B&(x\notin B)\\A\wedge B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow B\Rightarrow C)\Rightarrow C&\\A\vee B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C&\\\neg A&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)&\\\exists x:A.B&\equiv &\forall C:\mathbf {P} .(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{array}}} \)
Defining data types
The basic data types used in computer science can be defined within the Calculus of Constructions:
Booleans
\( \ {\displaystyle \forall A:\mathbf {P} .A\Rightarrow A\Rightarrow A} \)
Naturals
\( \ {\displaystyle \forall A:\mathbf {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 arise from propositional extensionality and proof irrelevance.[2]
See also
Pure type system
Lambda cube
System F
Dependent type
Intuitionistic type theory
Homotopy type theory
References
Calculus of Inductive Constructions, and basic standard libraries : Datatypes and Logic.
"Standard Library | The Coq Proof Assistant". coq.inria.fr. Retrieved 2020-08-08.
Coquand, Thierry; Huet, Gérard (1988). "The Calculus of Constructions" (PDF). Information and Computation. 76 (2–3): 95–120. doi:10.1016/0890-5401(88)90005-3.
Also available freely accessible online: Coquand, Thierry; Huet, Gérard (1986). The calculus of constructions (Technical report). INRIA, Centre de Rocquencourt. 530.
Note terminology is rather different. For instance, ( \(\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" (PDF). Archived from the original (talk) on 2014-05-29. Retrieved 2013-03-03.
Huet, Gérard (1988). "Induction Principles Formalized in the Calculus of Constructions" (PDF). In Fuchi, K.; Nivat, M. (eds.). Programming of Future Generation Computers. North-Holland. pp. 205–216. ISBN 0444704108. — An application of the CoC
Undergraduate Texts in Mathematics
Graduate Studies in Mathematics
Hellenica World - Scientific Library
Retrieved from "http://en.wikipedia.org/"
All text is available under the terms of the GNU Free Documentation License
