Editing Calculus of constructions (section)

==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 [[Typed lambda calculus|simply typed lambda calculus]] with each [[natural deduction|natural-deduction]] proof in [[intuitionistic logic|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:

* <math>\mathbf{T}</math> is a term (also called ''type'');
* <math>\mathbf{P}</math> is a term (also called ''prop'', the type of all propositions);
* Variables (<math>x, y, \ldots</math>) are terms;
* If <math>A</math> and <math>B</math> are terms, then so is <math>(A B)</math>;
* If <math>A</math> and <math>B</math> are terms and <math>x</math> is a variable, then the following are also terms:
** <math>(\lambda x:A. B)</math>,
** <math>(\forall x:A. B)</math>.

In other words, the term syntax, in [[Backus–Naur form]], is then:
:<math>e ::= \mathbf{T} \mid \mathbf{P} \mid x \mid e \, e \mid \lambda x\mathbin{:}e.e\mid \forall x\mathbin{:}e.e</math>

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 (<math>\mathbf{P}</math> is an example of a large type);
# <math>\mathbf{T}</math> itself, which is the type of large types.

=== β-equivalence ===

As with the untyped lambda calculus, the calculus of constructions uses a basic notion of equivalence of terms, known as <math>\beta</math>-equivalence. This captures the meaning of <math>\lambda</math>-abstraction:

* <math>(\lambda x:A . B) N =_\beta B(x := N)</math>

<math>\beta</math>-equivalence is a congruence relation for the calculus of constructions, in the sense that

* If <math>A =_\beta B</math> and <math>M =_\beta N</math>, then <math>A M =_\beta B N</math>.

===Judgments===

The calculus of constructions allows proving '''typing judgments''':

:<math> x_1:A_1, x_2:A_2, \ldots \vdash t:B</math>,

which can be read as the implication

: If variables <math>x_1, x_2, \ldots</math> have, respectively, types <math>A_1, A_2, \ldots</math>, then term <math>t</math> has type <math>B</math>.

The valid judgments for the calculus of constructions are derivable from a set of [[Rule of inference|inference rules]]. In the following, we use <math>\Gamma</math> to mean a sequence of type assignments 
<math> x_1:A_1, x_2:A_2, \ldots </math>; <math>A, B, C, D</math> to mean terms; and <math>K, L</math> to mean either <math>\mathbf{P}</math> or <math>\mathbf{T}</math>. We shall write <math>B[x:=N]</math> to mean the result of substituting the term <math>N</math> for the [[free variable]] <math>x</math> in the term <math>B</math>.

An inference rule is written in the form

:<math>\frac{\Gamma \vdash A:B}{\Gamma' \vdash C:D}</math>,

which means

: if <math> \Gamma \vdash A:B </math> is a valid judgment, then so is <math> \Gamma' \vdash C:D </math>.

===Inference rules for the calculus of constructions===

'''1'''. <math> {{} \over
\Gamma \vdash \mathbf{P} : \mathbf{T}} </math>

'''2'''. <math> {{\Gamma \vdash A : K} \over 
{\Gamma, x:A, \Gamma' \vdash x : A}} </math>

'''3'''. <math> {\Gamma \vdash A : K \qquad\qquad \Gamma, x:A \vdash B : L \over
{\Gamma \vdash (\forall x:A . B) : L}} </math>

'''4'''. <math> {\Gamma \vdash A : K \qquad\qquad \Gamma, x:A \vdash N : B \over 
{\Gamma \vdash (\lambda x:A . N) : (\forall x:A . B)}} </math>

'''5'''. <math> {\Gamma \vdash M : (\forall x:A . B) \qquad\qquad \Gamma \vdash N : A \over 
{\Gamma \vdash M N : B[x := N]}} </math>

'''6'''.   <math> {\Gamma \vdash M : A \qquad \qquad A =_\beta B \qquad \qquad \Gamma \vdash B : K 
\over {\Gamma \vdash M : B}} </math>

===Defining logical operators===

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

: <math>
\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}
</math>

===Defining data types===

The basic data types used in computer science can be defined within the calculus of constructions:

; Booleans : <math>\forall A: \mathbf{P} . A \Rightarrow A \Rightarrow A</math>
; Naturals : <math>\forall A: \mathbf{P} . 
(A \Rightarrow A) \Rightarrow A \Rightarrow A</math>
; Product <math>A \times B</math> : <math>A \wedge B</math>
; Disjoint union <math>A + B</math> : <math>A \vee B</math>

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.<ref name=":0">{{Cite web|title=Standard Library {{!}} The Coq Proof Assistant|url=https://coq.inria.fr/stdlib/Coq.Logic.ClassicalFacts.html|access-date=2020-08-08|website=coq.inria.fr}}</ref>