Calculus of constructions
Encyclopedia
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
.
, initially developed by Thierry Coquand
, where type
s 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.
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").
The calculus of constructions has five kinds of objects:
Which can be read as the implication
The valid judgments 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
, and we use K to mean either P or T. We will write 
to mean "
has type
, and 
has type 
". We will write 
to mean the result of substituting the term
for the variable 
in
the term
.
An inference rule is written in the form
which means
2.
3.
4.
5.
. However, this one operator is sufficient to define all the other logical operators:
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq
Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
proof assistant, which implements the derivative calculus of inductive constructions
Calculus of inductive constructions
The calculus of inductive constructions is the underlying core language of the Coq Proof Assistant. It is based on the calculus of constructions extended by inductive definitions as they are known from intuitionistic type theory....
.
General traits
The CoC is a higher-order typed lambda calculusTyped lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
, initially developed by Thierry Coquand
Thierry Coquand
Thierry Coquand is a professor in computer science at the University of Gothenburg, Sweden. He is known for his work in constructive mathematics, especially the calculus of constructions. He received his Ph.D. under the supervision of Gérard Huet.- External links :*...
, where type
Data type
In computer programming, a data type is a classification identifying one of various types of data, such as floating-point, integer, or Boolean, that determines the possible values for that type; the operations that can be done on values of that type; the meaning of the data; and the way values of...
s 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
Henk Barendregt
Hendrik Pieter Barendregt is a Dutch logician, known for his work in lambda calculus and type theory.Barendregt studied mathematical logic at Utrecht University, obtaining his Masters in 1968 and his Ph.D. in 1971, both cum laude, under Dirk van Dalen and Georg Kreisel...
's lambda cube
Lambda cube
In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions as its diametrically opposite...
, it is therefore the richest calculus.
The CoC is strongly normalizing
Normalization property (lambda-calculus)
In mathematical logic and theoretical computer science, a rewrite system has the strong normalization property if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates to a term in normal form...
, 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
Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
proof assistant; later versions were built upon the calculus of inductive constructions
Calculus of inductive constructions
The calculus of inductive constructions is the underlying core language of the Coq Proof Assistant. It is based on the calculus of constructions extended by inductive definitions as they are known from intuitionistic type theory....
, 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 calculusTyped lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
with each natural-deduction proof in intuitionistic propositional logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
. 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
and 
are terms, then so are
-
- (
) - (
)
-
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.
Judgments
The calculus of constructions allows proving typing judgments:Which can be read as the implication
- If variables
have types 
, then term 
has type 
.
The valid judgments 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, and we use K to mean either P or T. We will write to mean " has type, and has type ". We will write to mean the result of substituting the term for the variable inthe term
.An inference rule is written in the form
which means
- If
is a valid judgment, then so is 
Inference rules for the calculus of constructions
1.2.
3.
4.
5.
Defining logical operators
The calculus of constructions has very few basic operators: the only logical operator for forming propositions is. However, this one operator is sufficient to define all the other logical operators:-
Defining data types
The basic data types used in computer science can be defined
within the Calculus of Constructions:
Booleans :
Naturals :
Product
: 
Disjoint union
: 
Note that Booleans and Naturals are defined in the same way that in Church encodingChurch encodingIn mathematics, Church encoding is a means of embedding data and operators into the lambda calculus, the most familiar form being the Church numerals, a representation of the natural numbers using lambda notation...
. However additional problems raise from propositional extensionality and proof irrelevance http://coq.inria.fr/stdlib/Coq.Logic.ClassicalFacts.html.
See also
- Curry–Howard isomorphism
- Intuitionistic logicIntuitionistic logicIntuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
- Intuitionistic type theoryIntuitionistic type theoryIntuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
- Lambda calculusLambda calculusIn mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
- Lambda cubeLambda cubeIn mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions as its diametrically opposite...
- System FSystem FSystem F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
- Typed lambda calculusTyped lambda calculusA typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...