Calculus of constructions

<h2 id="general-traits">General traits</h2>
<p>The CoC is a higher-order <a href="/facts/Typed_lambda_calculus/g86GP4uK">typed lambda calculus</a>, initially developed by <a href="/facts/Thierry_Coquand/jG36x5By">Thierry Coquand</a>. It is well known for being at the top of <a href="/facts/Henk_Barendregt/jmvltEQ6">Barendregt</a>'s <a href="/facts/Lambda_cube/tSR2laCs">lambda cube</a>. 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.
</p><p>The CoC is <a href="/facts/Normalization_property_(lambda-calculus)/eV9G3veH">strongly normalizing</a>, and hence <a href="/facts/Consistent/IHkdnA9M">consistent</a>.<a class="footnote-ref" id="fnref:1" href="#fn:1"><sup>1</sup></a>
</p>
<h2 id="usage">Usage</h2>
<p>The CoC has been developed alongside the <a href="/facts/Coq_(software)/7oBXgLCE">Coq</a> <a href="/facts/Proof_assistant/hjFGxLPn">proof assistant</a>. As features were added (or possible liabilities removed) to the theory, they became available in Coq.
</p><p>Variants of the CoC are used in other proof assistants, such as <a href="/facts/Matita/XUWzWMfU">Matita</a> and <a href="/facts/Lean_(proof_assistant)/FbQvTqmg">Lean</a>.
</p>
<h2 id="the-basics-of-the-calculus-of-constructions">The basics of the calculus of constructions</h2>
<p>The calculus of constructions can be considered an extension of the <a href="/facts/Curry%E2%80%93Howard_isomorphism/Q3eVu60u">Curry–Howard isomorphism</a>. The Curry–Howard isomorphism associates a term in the <a href="/facts/Typed_lambda_calculus/g86GP4uK">simply typed lambda calculus</a> with each <a href="/facts/Natural_deduction/PPtgwoaJ">natural-deduction</a> proof in <a href="/facts/Intuitionistic_logic/zI7ulCnM">intuitionistic propositional logic</a>. The calculus of constructions extends this isomorphism to proofs in the full intuitionistic <a href="/facts/Predicate_calculus/lcISqWIg">predicate calculus</a>, which includes proofs of quantified statements (which we will also call "propositions").
</p>
<h3>Terms</h3>
<p>A <i>term</i> in the calculus of constructions is constructed using the following rules:
</p>
<ul><li>
  
    
      
        
          T
        
      
    
    {\displaystyle \mathbf {T} }
  
 is a term (also called <i>type</i>);</li>
<li>
  
    
      
        
          P
        
      
    
    {\displaystyle \mathbf {P} }
  
 is a term (also called <i>prop</i>, the type of all propositions);</li>
<li>Variables (
  
    
      
        x
        ,
        y
        ,
        …
      
    
    {\displaystyle x,y,\ldots }
  
) are terms;</li>
<li>If 
  
    
      
        A
      
    
    {\displaystyle A}
  
 and 
  
    
      
        B
      
    
    {\displaystyle B}
  
 are terms, then so is 
  
    
      
        (
        A
        B
        )
      
    
    {\displaystyle (AB)}
  
;</li>
<li>If 
  
    
      
        A
      
    
    {\displaystyle A}
  
 and 
  
    
      
        B
      
    
    {\displaystyle B}
  
 are terms and 
  
    
      
        x
      
    
    {\displaystyle x}
  
 is a variable, then the following are also terms:
<ul><li>
  
    
      
        (
        λ
        x
        :
        A
        .
        B
        )
      
    
    {\displaystyle (\lambda x:A.B)}
  
,</li>
<li>
  
    
      
        (
        ∀
        x
        :
        A
        .
        B
        )
      
    
    {\displaystyle (\forall x:A.B)}
  
.</li></ul></li></ul>
<p>In other words, the term syntax, in <a href="/facts/Backus%E2%80%93Naur_form/xbMXDntc">Backus–Naur form</a>, is then:
</p>

e
        ::=
        
          T
        
        ∣
        
          P
        
        ∣
        x
        ∣
        e
        
        e
        ∣
        λ
        x
        
          
            :
          
        
        e
        .
        e
        ∣
        ∀
        x
        
          
            :
          
        
        e
        .
        e
      
    
    {\displaystyle e::=\mathbf {T} \mid \mathbf {P} \mid x\mid e\,e\mid \lambda x{\mathbin {:}}e.e\mid \forall x{\mathbin {:}}e.e}

<p>The calculus of constructions has five kinds of objects:
</p>
<ol><li><i>proofs</i>, which are terms whose types are <i>propositions</i>;</li>
<li><i>propositions</i>, which are also known as <i>small types</i>;</li>
<li><i>predicates</i>, which are functions that return propositions;</li>
<li><i>large types</i>, which are the types of predicates (
  
    
      
        
          P
        
      
    
    {\displaystyle \mathbf {P} }
  
 is an example of a large type);</li>
<li>
  
    
      
        
          T
        
      
    
    {\displaystyle \mathbf {T} }
  
 itself, which is the type of large types.</li></ol>
<h3>β-equivalence</h3>
<p>As with the untyped lambda calculus, the calculus of constructions uses a basic notion of equivalence of terms, known as 
  
    
      
        β
      
    
    {\displaystyle \beta }
  
-equivalence. This captures the meaning of 
  
    
      
        λ
      
    
    {\displaystyle \lambda }
  
-abstraction:
</p>
<ul><li>
  
    
      
        (
        λ
        x
        :
        A
        .
        B
        )
        N
        
          =
          
            β
          
        
        B
        (
        x
        :=
        N
        )
      
    
    {\displaystyle (\lambda x:A.B)N=_{\beta }B(x:=N)}
  
</li></ul>
<p>
  
    
      
        β
      
    
    {\displaystyle \beta }
  
-equivalence is a congruence relation for the calculus of constructions, in the sense that
</p>
<ul><li>If 
  
    
      
        A
        
          =
          
            β
          
        
        B
      
    
    {\displaystyle A=_{\beta }B}
  
 and 
  
    
      
        M
        
          =
          
            β
          
        
        N
      
    
    {\displaystyle M=_{\beta }N}
  
, then 
  
    
      
        A
        M
        
          =
          
            β
          
        
        B
        N
      
    
    {\displaystyle AM=_{\beta }BN}
  
.</li></ul>
<h3>Judgments</h3>
<p>The calculus of constructions allows proving typing judgments:
</p>

x
          
            1
          
        
        :
        
          A
          
            1
          
        
        ,
        
          x
          
            2
          
        
        :
        
          A
          
            2
          
        
        ,
        …
        ⊢
        t
        :
        B
      
    
    {\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}
  
,
<p>which can be read as the implication
</p>
If variables 
  
    
      
        
          x
          
            1
          
        
        ,
        
          x
          
            2
          
        
        ,
        …
      
    
    {\displaystyle x_{1},x_{2},\ldots }
  
 have, respectively, types 
  
    
      
        
          A
          
            1
          
        
        ,
        
          A
          
            2
          
        
        ,
        …
      
    
    {\displaystyle A_{1},A_{2},\ldots }
  
, then term 
  
    
      
        t
      
    
    {\displaystyle t}
  
 has type 
  
    
      
        B
      
    
    {\displaystyle B}
  
.
<p>The valid judgments for the calculus of constructions are derivable from a set of <a href="/facts/Rule_of_inference/QV5NklQ9">inference rules</a>. In the following, we use 
  
    
      
        Γ
      
    
    {\displaystyle \Gamma }
  
 to mean a sequence of type assignments

x
          
            1
          
        
        :
        
          A
          
            1
          
        
        ,
        
          x
          
            2
          
        
        :
        
          A
          
            2
          
        
        ,
        …
      
    
    {\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots }
  
; 
  
    
      
        A
        ,
        B
        ,
        C
        ,
        D
      
    
    {\displaystyle A,B,C,D}
  
 to mean terms; and 
  
    
      
        K
        ,
        L
      
    
    {\displaystyle K,L}
  
 to mean either 
  
    
      
        
          P
        
      
    
    {\displaystyle \mathbf {P} }
  
 or 
  
    
      
        
          T
        
      
    
    {\displaystyle \mathbf {T} }
  
. We shall write 
  
    
      
        B
        [
        x
        :=
        N
        ]
      
    
    {\displaystyle B[x:=N]}
  
 to mean the result of substituting the term 
  
    
      
        N
      
    
    {\displaystyle N}
  
 for the <a href="/facts/Free_variable/ndWnXXYs">free variable</a> 
  
    
      
        x
      
    
    {\displaystyle x}
  
 in the term 
  
    
      
        B
      
    
    {\displaystyle B}
  
.
</p><p>An inference rule is written in the form
</p>

Γ
              ⊢
              A
              :
              B
            
            
              
                Γ
                ′
              
              ⊢
              C
              :
              D
            
          
        
      
    
    {\displaystyle {\frac {\Gamma \vdash A:B}{\Gamma '\vdash C:D}}}
  
,
<p>which means
</p>
if 
  
    
      
        Γ
        ⊢
        A
        :
        B
      
    
    {\displaystyle \Gamma \vdash A:B}
  
 is a valid judgment, then so is 
  
    
      
        
          Γ
          ′
        
        ⊢
        C
        :
        D
      
    
    {\displaystyle \Gamma '\vdash C:D}
  
.
<h3>Inference rules for the calculus of constructions</h3>
<p>1.

Γ
              ⊢
              
                P
              
              :
              
                T
              
            
          
        
      
    
    {\displaystyle {{} \over \Gamma \vdash \mathbf {P} :\mathbf {T} }}

</p><p>2. 
  
    
      
        
          
            
              Γ
              ⊢
              A
              :
              K
            
            
              Γ
              ,
              x
              :
              A
              ,
              
                Γ
                ′
              
              ⊢
              x
              :
              A
            
          
        
      
    
    {\displaystyle {{\Gamma \vdash A:K} \over {\Gamma ,x:A,\Gamma '\vdash x:A}}}

</p><p>3. 
  
    
      
        
          
            
              Γ
              ⊢
              A
              :
              K
              
              
              Γ
              ,
              x
              :
              A
              ⊢
              B
              :
              L
            
            
              Γ
              ⊢
              (
              ∀
              x
              :
              A
              .
              B
              )
              :
              L
            
          
        
      
    
    {\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash B:L \over {\Gamma \vdash (\forall x:A.B):L}}}

</p><p>4. 
  
    
      
        
          
            
              Γ
              ⊢
              A
              :
              K
              
              
              Γ
              ,
              x
              :
              A
              ⊢
              N
              :
              B
            
            
              Γ
              ⊢
              (
              λ
              x
              :
              A
              .
              N
              )
              :
              (
              ∀
              x
              :
              A
              .
              B
              )
            
          
        
      
    
    {\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:A.N):(\forall x:A.B)}}}

</p><p>5. 
  
    
      
        
          
            
              Γ
              ⊢
              M
              :
              (
              ∀
              x
              :
              A
              .
              B
              )
              
              
              Γ
              ⊢
              N
              :
              A
            
            
              Γ
              ⊢
              M
              N
              :
              B
              [
              x
              :=
              N
              ]
            
          
        
      
    
    {\displaystyle {\Gamma \vdash M:(\forall x:A.B)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B[x:=N]}}}

</p><p>6.   
  
    
      
        
          
            
              Γ
              ⊢
              M
              :
              A
              
              
              A
              
                =
                
                  β
                
              
              B
              
              
              Γ
              ⊢
              B
              :
              K
            
            
              Γ
              ⊢
              M
              :
              B
            
          
        
      
    
    {\displaystyle {\Gamma \vdash M:A\qquad \qquad A=_{\beta }B\qquad \qquad \Gamma \vdash B:K \over {\Gamma \vdash M:B}}}

</p>
<h3>Defining logical operators</h3>
<p>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:
</p>

A
                ⇒
                B
              
              
                ≡
              
              
                ∀
                x
                :
                A
                .
                B
              
              
                (
                x
                ∉
                B
                )
              
            
            
              
                A
                ∧
                B
              
              
                ≡
              
              
                ∀
                C
                :
                
                  P
                
                .
                (
                A
                ⇒
                B
                ⇒
                C
                )
                ⇒
                C
              
              
            
            
              
                A
                ∨
                B
              
              
                ≡
              
              
                ∀
                C
                :
                
                  P
                
                .
                (
                A
                ⇒
                C
                )
                ⇒
                (
                B
                ⇒
                C
                )
                ⇒
                C
              
              
            
            
              
                ¬
                A
              
              
                ≡
              
              
                ∀
                C
                :
                
                  P
                
                .
                (
                A
                ⇒
                C
                )
              
              
            
            
              
                ∃
                x
                :
                A
                .
                B
              
              
                ≡
              
              
                ∀
                C
                :
                
                  P
                
                .
                (
                ∀
                x
                :
                A
                .
                (
                B
                ⇒
                C
                )
                )
                ⇒
                C
              
              
            
          
        
      
    
    {\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}}}

<h3>Defining data types</h3>
<p>The basic data types used in computer science can be defined within the calculus of constructions:
</p>
Booleans

∀
        A
        :
        
          P
        
        .
        A
        ⇒
        A
        ⇒
        A
      
    
    {\displaystyle \forall A:\mathbf {P} .A\Rightarrow A\Rightarrow A}

Naturals

∀
        A
        :
        
          P
        
        .
        (
        A
        ⇒
        A
        )
        ⇒
        A
        ⇒
        A
      
    
    {\displaystyle \forall A:\mathbf {P} .(A\Rightarrow A)\Rightarrow A\Rightarrow A}

Product 
  
    
      
        A
        ×
        B
      
    
    {\displaystyle A\times B}

A
        ∧
        B
      
    
    {\displaystyle A\wedge B}

Disjoint union 
  
    
      
        A
        +
        B
      
    
    {\displaystyle A+B}

A
        ∨
        B
      
    
    {\displaystyle A\vee B}

<p>Note that Booleans and Naturals are defined in the same way as in <a href="/facts/Church_encoding/IlLPzswH">Church encoding</a>. However, additional problems arise from propositional extensionality and proof irrelevance.<a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a>
</p>
<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Pure_type_system/045wJpGU">Pure type system</a></li>
<li><a href="/facts/Lambda_cube/tSR2laCs">Lambda cube</a></li>
<li><a href="/facts/System_F/odpwVpAG">System F</a></li>
<li><a href="/facts/Dependent_type/wCeQI7ds">Dependent type</a></li>
<li><a href="/facts/Intuitionistic_type_theory/qwkrpKlP">Intuitionistic type theory</a></li>
<li><a href="/facts/Homotopy_type_theory/C2vTAVnJ">Homotopy type theory</a></li></ul>

<h2 id="sources">Sources</h2>

<ul><li><a href="/facts/Thierry_Coquand/jG36x5By">Coquand, Thierry</a>; <a href="/facts/G%C3%A9rard_Huet/127arH1z">Huet, Gérard</a> (1988). <a href="http://hal.archives-ouvertes.fr/docs/00/07/60/24/PDF/RR-0530.pdf">"The Calculus of Constructions"</a> (PDF). <i><a href="/facts/Information_and_Computation/4gdF7pR6">Information and Computation</a></i>. 76 (2–3): 95–120. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2F0890-5401%2888%2990005-3">10.1016/0890-5401(88)90005-3</a>.
<ul><li>Also available freely accessible online: Coquand, Thierry; Huet, Gérard (1986). <a href="http://hal.inria.fr/inria-00076024/en/"><i>The calculus of constructions</i></a> (Technical report). <a href="/facts/INRIA/ruIkcapf">INRIA</a>, Centre de Rocquencourt. 530.  Note terminology is rather different. For instance, (
  
    
      
        ∀
        x
        :
        A
        .
        B
      
    
    {\displaystyle \forall x:A.B}
  
) is written [<i>x</i> : <i>A</i>] <i>B</i>.</li></ul></li>
<li>Bunder, M. W.; Seldin, Jonathan P. (2004). <a href="https://citeseerx.ist.psu.edu/doc/10.1.1.88.9497">"Variants of the Basic Calculus of Constructions"</a>. <a href="/facts/CiteSeerX_(identifier)/SceDmd3c">CiteSeerX</a> <a href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.88.9497">10.1.1.88.9497</a>.</li>
<li>Frade, Maria João (2009). <a href="https://web.archive.org/web/20140529103535/http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf">"Calculus of Inductive Constructions"</a> (PDF). Archived from <a href="http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf">the original</a> (talk) on 2014-05-29. Retrieved 2013-03-03.</li>
<li>Huet, Gérard (1988). <a href="https://web.archive.org/web/20150701130220/http://yquem.inria.fr/~huet/PUBLIC/induction.pdf">"Induction Principles Formalized in the Calculus of Constructions"</a> (PDF). In Fuchi, K.; <a href="/facts/Maurice_Nivat/l5GtJaYb">Nivat, M.</a> (eds.). <i>Programming of Future Generation Computers</i>. North-Holland. pp. 205–216. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 0444704108. Archived from <a href="http://yquem.inria.fr/~huet/PUBLIC/induction.pdf">the original</a> (PDF) on 2015-07-01. — An application of the CoC</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>Coquand, Thierry; Gallier, Jean H. (July 1990). "A Proof of Strong Normalization for the Theory of Constructions Using a Kripke-Like Interpretation". Technical Reports (Cis) (568): 14. <a href="https://repository.upenn.edu/cis_reports/568/" target="_blank">https://repository.upenn.edu/cis_reports/568/</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>"Standard Library | The Coq Proof Assistant". coq.inria.fr. Retrieved 2020-08-08. <a href="https://coq.inria.fr/stdlib/Coq.Logic.ClassicalFacts.html" target="_blank">https://coq.inria.fr/stdlib/Coq.Logic.ClassicalFacts.html</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
</ol>

Calculus of constructions open-in-new

Calculus of constructions