Fact-checked by Grok 2 weeks ago

Calculus of constructions

The Calculus of Constructions (CoC) is a higher-order typed lambda calculus and type theory introduced by Thierry Coquand and Gérard Huet in 1988, designed as a formalism for constructing both proofs and programs in a unified framework based on the Curry-Howard isomorphism, where propositions correspond to types and proofs to typed lambda terms. It integrates impredicative quantification from the polymorphic lambda calculus Fω with the dependent types and universes of Martin-Löf's intuitionistic type theory, enabling complex polymorphism where types can be treated as terms and quantified over universally. CoC operates without primitive types or constructors, instead encoding all data structures—such as natural numbers—through impredicative definitions, though it lacks built-in induction principles, limiting its expressiveness for recursive proofs. The system's syntax includes lambda abstractions, applications, dependent products (denoted [x:M]N for "forall x:M, N"), and two sorts: an impredicative sort for propositions and a predicative universe * for types, with judgments for well-formed contexts and typing ensuring consistency. A key theoretical result is its strong normalization, proving that all reduction sequences terminate, which guarantees the decidability of type checking and the reliability of computations. Positioned at the apex of Barendregt's , allows dependencies across all dimensions—from terms to terms, types to types, and terms to types—making it a pinnacle of pure type systems before extensions. Its impredicativity, where the sort of propositions is closed under general quantification, contrasts with predicative systems by permitting definitions that quantify over the universe itself, enhancing expressiveness for while maintaining constructivity. laid the groundwork for practical proof assistants; it was extended with inductive types by Paulin-Mohring in 1993 to form the Calculus of Inductive Constructions (), which underpins the system for and theorem proving.

Overview

Definition and Core Principles

The Calculus of Constructions (CoC) is a dependently typed lambda calculus that extends the simply typed lambda calculus by incorporating sorts such as Type (denoted *) and Kind (denoted □), which enable types to be expressed as terms and support higher-order dependencies between types.90005-3) This framework allows for the construction of types that depend on terms, facilitating the encoding of mathematical propositions and proofs within a unified system. CoC operates within the paradigm of pure type systems, characterized by an impredicative universe Type where types can be quantified over themselves, and it embodies the Curry-Howard isomorphism, which equates logical proofs with typed programs, thereby supporting both constructive programming and theorem proving.90005-3) The impredicativity of Type permits definitions that refer to the universe itself, enhancing expressiveness for higher-order logic while maintaining consistency through the stratification provided by Kind. A distinguishing trait of CoC is its purity: it begins without built-in constants, with all mathematical objects constructed solely via abstraction and application, which aligns with principles of constructive by emphasizing explicit constructions over classical assumptions. This design enables the formalization of and has established CoC as the foundational for proof assistants like , which extends it with inductive definitions, and , which builds upon a variant with universe hierarchies.

Historical Development

The Calculus of Constructions (CoC) originated in the mid-1980s at INRIA, developed by and Gérard Huet as a higher-order aimed at mechanizing mathematical proofs. It built upon Per Martin-Löf's , which introduced dependent types to encode propositions and proofs uniformly, and Jean-Yves Girard's , which provided impredicative polymorphism through . These influences addressed limitations in earlier systems like Nuprl, which, while based on Martin-Löf's predicative approach, struggled with fully integrating and impredicativity for concise proof representations. CoC's design also drew from foundations and the Automath project by Niklaus de Bruijn, which pioneered the Curry-Howard isomorphism for viewing proofs as programs in a type-theoretic setting. Coquand's PhD thesis, defended on January 31, 1985, presented the initial version of CoC as a higher-order extension of Automath, emphasizing constructive proofs in style. This was followed by the seminal paper "Constructions: A Higher Order Proof System for Mechanizing Mathematics," published in the proceedings of EUROCAL '85, which formalized CoC and introduced dependent types within a framework, enabling the encoding of mathematical structures and proofs as typed terms. The system included sorts for types and propositions, supporting both predicative and impredicative constructions, and included a proof of relative to Martin-Löf's theory. Development accelerated in the late , leading to the Calculus of Inductive Constructions () around 1989, an extension of by Coquand and Christine Paulin that incorporated primitive inductive definitions for defining recursive data types like natural numbers and directly in the . This evolution added an impredicative sort for propositions and allowed inductive types to be used in type definitions, enhancing expressiveness for proof assistants while maintaining strong normalization. The key publication, "Inductively Defined Types" (1990), detailed these rules and properties, bridging 's with Martin-Löf-style induction. By the early 1990s, formed the basis for the proof assistant, with initial implementations in versions 5.6 (1991) and 5.8 (1993), integrating CoC's core into a practical tool for and program extraction. This period marked CoC's transition from theoretical formalism to foundational role in interactive theorem proving, influencing subsequent developments in throughout the decade.

Syntax

Terms and Syntax Rules

The calculus of constructions (CoC) defines terms through an abstract syntax that treats types as first-class citizens, allowing for the construction of both proofs and programs within a unified framework. Terms are built from a small set of primitive constructors, encompassing variables, applications, lambda abstractions for dependent functions, and dependent products (which generalize both function types and universal quantification). This syntax enables the encoding of higher-order logic and typed lambda calculus features without relying on built-in constants or axioms in the pure system; all structures are derived compositionally from these primitives. Polymorphism is achieved through dependent products over the universe sort, without separate syntactic constructs for type abstraction. The formal syntax can be specified using a BNF-like notation, where terms t (which include both expressions and types) are defined as follows: 
t ::= x                  (variable)
    | Πx:A.t             (dependent product)
    | λx:A.t             (lambda abstraction)
    | t t                (application)
Here, x and A range over variables. The sort * serves as the special atomic term that anchors the type hierarchy, representing the impredicative universe of types (often denoted \square or s). In the original formulation, * inhabits itself (* : *), enabling impredicativity where types can quantify over themselves, though this leads to logical inconsistencies like Girard's paradox. Variables in terms are either free or bound: a free variable occurs unbound in a term, while bound variables are captured by the nearest enclosing lambda (\lambda x:A.t) or product (\Pi x:A.t) binder. Terms are considered equivalent up to alpha-conversion, meaning that bound variables can be consistently renamed without altering the 's meaning, ensuring capture-avoiding substitutions in further operations. This variable discipline supports the pure syntax's expressiveness while maintaining a concise set of rules for formation.

Sorts and Type Hierarchy

The employs a of sorts to establish a structure for types, allowing types to be treated as terms while managing potential inconsistencies. In , there is a single impredicative sort *, which serves as the of types and propositions, with the * : *. This impredicativity permits definitions that quantify over the itself, supporting compact encodings of . However, the self-inhabitation * : * allows the construction of paradoxical terms, such as Girard's paradox, rendering the logic inconsistent for full higher-order propositional reasoning. Later extensions address this by distinguishing an impredicative sort for propositions (with products into Prop quantifying over Prop) from a predicative sort Type for types, often with Type : Type initially but refined to avoid paradoxes. In consistent variants, such as those underlying modern proof assistants, the type hierarchy is built upon a cumulative tower of universes denoted Type_i for nonnegative integers i, where each Type_i represents a predicative level of types. The inclusions are axiomatized as Type_i : Type_{i+1} for all i ≥ 0, enabling a term of type Type_i to also inhabit higher universes Type_j for j > i. may be included as Type_0 or separately with impredicativity restricted to it. This setup allows types to be introspected and manipulated at the meta-level, as a type in Type_i is itself a term typed by Type_{i+1}, while preventing self-referential paradoxes by enforcing ascent through the indexed levels. The dependent product type, written as \Pi x : A . B, functions as the primitive for both function spaces and universal quantification, where the codomain B may depend on the value of x : A. Typing rules for the product respect the sort hierarchy: if A : s_1 and, under the assumption x : A, B : s_2, then \Pi x : A . B : s_3 provided (s_1, s_2, s_3) is permitted by the system's axioms, such as in the impredicative case for * or Prop. This mechanism unifies computation and proof, allowing dependent functions to encode predicates and logical implications. CoC is formalized as an instance of a (PTS) with sort S = \{*\} in the core, where the axiom set includes * : *, and the rule set R specifies valid product formations, such as (*, *, *). Impredicativity allows quantification over the entire hierarchy. In extended consistent versions, S = \{\mathsf{Prop}\} \cup \{\mathsf{Type}_i \mid i \in \mathbb{N}\}, with predicative rules (s, s', s) where s is the max level, and special impredicative rules for . In contrast to the simply typed lambda calculus, which relies on a rigid assortment of atomic types without mechanisms for typing types themselves, CoC's sorts permit the universe to inhabit higher levels or itself, fostering impredicative polymorphism that supports advanced encodings of inductive types and higher-order logic within a unified framework.

Semantics

Beta-Equivalence and Reduction

In the calculus of constructions, beta-reduction defines the computational behavior of terms through substitution in applications. The one-step beta-reduction relation, denoted →_β, is the smallest congruence relation generated by two rules: for term-level application, (λx:A.M) N →_β [N/x]M, where substitution replaces free occurrences of x in M with N; and for type-level application, (Λx:A.M) B →_β [B/x]M, where B is a type term. These rules capture the evaluation of lambda abstractions at both term and type levels, enabling the unfolding of definitions in a higher-order setting.90005-3) Multi-step reduction, denoted →_β^, extends one-step reduction transitively, allowing terms to be evaluated to normal forms where no further beta-redexes exist. Various reduction strategies guide the order of applying these rules, such as call-by-name, which evaluates the leftmost outermost redex first, and call-by-value, which reduces arguments to values before substitution. Weak head reduction limits evaluation to the head of a term without descending into subterms, while strong head reduction fully normalizes under the head; these strategies ensure termination in well-typed terms but are defined syntactically here. The system exhibits , meaning that if a term reduces to two different terms via →_β^, there exists a common reduct; this follows from the Church-Rosser theorem, which guarantees unique forms up to equivalence.90005-3) Beta-equivalence, denoted ≡_β, is the reflexive, symmetric, of →_β and its inverse (beta-expansion), or equivalently, M ≡_β N if there exists P such that M →_β^* P and N →_β^* P. This identifies terms that compute to the same result, forming the basis for operational in the . An extension to beta-equivalence incorporates eta-equivalence for : λx:A. (M x) ≡_η M, provided x does not occur free in M, allowing over applications to be collapsed when the variable is unused. This rule is not part of the core but enhances to capture functional extensionality. In the pure calculus of constructions, without definitions or axioms, coincides with beta-equivalence (or beta-eta if extended), serving as the computational notion of equality for terms.90005-3)

Judgments and Typing

The of the Calculus of Constructions () relies on declarative judgments to specify the well-formedness of contexts, the formation of types at specific sorts, and the of terms relative to those types. These judgments form the foundation for ensuring the consistency and habitability of constructions within varying contexts, enabling the expression of dependent types where types themselves may vary based on term values.90005-3) The primary judgments are as follows:
  • Γ ⊢: This asserts that the context Γ is well-formed, meaning it consists of a valid of variable declarations of the form x : A, where each A is a type and variables are distinct.
  • Γ ⊢ A : s: This declares that A is a valid type (or construction) of sort s under context Γ, where sorts classify types hierarchically.
  • Γ ⊢ M : A: This states that the term M inhabits the type A in context Γ, confirming M as a valid proof or relative to A.
Contexts support structured extension while maintaining validity. The empty context \emptyset (or \cdot) is inherently well-formed. Furthermore, if Γ is well-formed and Γ ⊢ A : s for some sort s, then the extended context Γ, x : A is well-formed, provided x does not already appear in Γ. This extension rule ensures that new variables are bound only to properly formed types, preventing malformed declarations.90005-3) CoC features a hierarchy of sorts starting with Type (often denoted *) and Kind (denoted □), which serve as the universe of types and the sort of that universe, respectively. The key sort-level judgment is Γ ⊢ Type : Kind, establishing Type as the predicative sort for all type constructions, while Kind itself lacks a higher sort, forming the top of the . In the pure CoC, these sorts enable the classification of both propositions and types without an explicit impredicative Prop sort, though extensions may introduce it. Dependent typing is integral, allowing types to depend on terms via the dependent product notation Πx : A.B, where B is a type that may refer to the variable x of type A; this judgment Γ ⊢ Πx : A.B : s holds if A and B are appropriately formed under the extended context.90005-3) Contexts in CoC adhere to structural properties that preserve judgment validity across modifications. The weakening principle states that if Γ ⊢ J for some judgment J and Δ is a context extension of Γ (i.e., Δ = Γ, y_1 : B_1, ..., y_n : B_n where the y_i are fresh), then Δ ⊢ J, provided the additional variables do not appear free in J; this ensures irrelevance of unused assumptions. Similarly, the exchange principle guarantees that the order of declarations in a context does not affect the validity of judgments: if Γ = Γ_1, x : A, y : B, Γ_2 ⊢ J and x, y are distinct, then Γ = Γ_1, y : B, x : A, Γ_2 ⊢ J holds equivalently. These principles underpin the robustness of dependent typing by allowing flexible context manipulation without altering typability. Beta-equivalence, arising from reduction, preserves these typing judgments to maintain consistency.90005-3)

Type System

Inference Rules

The Calculus of Constructions (CoC) is formalized as a (PTS), a framework for dependent type theories specified by a set of sorts S, axioms A \subseteq S \times S, and production rules R \subseteq S \times \{\Pi\} \times S. For CoC, the sorts are S = \{\mathsf{Prop}, \mathsf{Type}\}, the axioms include the sort inclusion \mathsf{Prop} : \mathsf{Type}, and the production rules allow dependent products \Pi x : A . B to be formed when A and B are appropriately typed in \mathsf{Prop} or \mathsf{Type}, yielding a type in \mathsf{Prop} or \mathsf{Type}. This specification enables both impredicative quantification over propositions in \mathsf{Prop} and predicative higher-order types in \mathsf{Type}. The core inference rules derive judgments of the form \Gamma \vdash M : A, where \Gamma is a context of variable-type pairs, M is a term, and A is a type. These rules include structural rules for contexts and variables, introduction and elimination rules for applications and abstractions, formation rules for products, and a conversion rule based on \beta-equivalence. CoC extends standard typed \lambda-calculus rules to handle dependent types and type-level computation, using a unified syntax for term-level (\lambda) and type-level abstraction via dependent products (\Pi). The full set comprises approximately 10 rules, covering axioms, variables, sorts, products, applications, abstractions, type abstractions (via \Pi), conversions, and structural properties like weakening and substitution (derived from the core rules). The axiom rules establish the sort hierarchy: \vdash \mathsf{Prop} : \mathsf{Type} This axiom positions \mathsf{Prop} as the impredicative sort for propositions and \mathsf{Type} as the sort for types (allowing impredicativity over Prop and predicativity over Type). The variable rule (start) introduces assumptions from the context: If \Gamma = \Delta, x : A, then \Gamma \vdash x : A. This rule ensures well-formed variables are typed according to their declarations in \Gamma. The application rule eliminates dependent function types: \frac{\Gamma \vdash M : \Pi x : A . B \quad \Gamma \vdash N : A}{\Gamma \vdash M \, N : [N / x] B} Here, [N / x] B denotes of N for x in B, enabling both term application and type application (where N may be a type). The abstraction rule () forms dependent functions and universal quantifiers: \frac{\Gamma, x : A \vdash M : B}{\Gamma \vdash \lambda x : A . M : \Pi x : A . B} This assumes \Gamma, x : A is a valid extension of \Gamma (via the context formation rule: empty context is valid; if \Gamma valid and A typable in \Gamma, then \Gamma, x : A valid if x \notin \Gamma). When A is Type, this supports higher-order polymorphism by abstracting over type variables. The product formation rule constructs dependent products: \frac{\Gamma \vdash A : s \quad \Gamma, x : A \vdash B : t \quad (s, \Pi, t) \in R}{\Gamma \vdash \Pi x : A . B : t} In CoC, R includes ( \mathsf{Prop}, \Pi, \mathsf{Prop} ), ( \mathsf{Type}, \Pi, \mathsf{Prop} ), and ( \mathsf{Type}, \Pi, \mathsf{Type} ). This enables dependent types while respecting the hierarchy, with impredicativity restricted to . The conversion rule ensures typability under equivalence: \frac{\Gamma \vdash M : A \quad \Gamma \vdash A \equiv B}{\Gamma \vdash M : B} Here, A \equiv B holds if A and B are convertible via \beta-reduction steps (and symmetry, transitivity, congruence). This rule is crucial for normalizing types and proofs. Additional derived rules include weakening (adding irrelevant assumptions preserves typability) and (replacing a variable with a well-typed term preserves judgments), ensuring the system's and . These rules collectively define the without primitive logical connectives, relying on encodings via dependent products.

Dependent Types and Functions

In the Calculus of Constructions (), dependent types allow the type of a to depend on the itself, enabling more expressive specifications than non-dependent type systems. The core construct for this is the dependent product type, denoted \Pi x : A . B, which forms the type of functions whose codomain B may depend on the of the argument x of type A. This generalizes both simple function types (where B is independent of x) and universal quantification in . For example, a length-dependent type \mathsf{Vec}(n, A) can be conceptualized as \Pi n : \mathsf{[nat](/page/Nat)} . \Pi A : \mathsf{Type} . \tau(n, A), where \tau(n, A) encodes a structure whose properties vary with n, though \mathsf{nat} and inductive definitions are extensions beyond the pure . The typing rules for dependent functions in CoC ensure that abstractions and applications respect this dependency. For abstraction, if \Gamma, x : A \vdash M : B(x), then \Gamma \vdash \lambda x : A . M : \Pi x : A . B(x), where B(x) may refer to x. Application then substitutes the argument into the dependent codomain: if \Gamma \vdash f : \Pi x : A . B(x) and \Gamma \vdash a : A, then \Gamma \vdash f \, a : [a/x] B(x), with substitution [a/x] B(x) replacing free occurrences of x in B(x) by a. These rules, based on the type hierarchy of CoC with Prop and Type, allow types to be computed based on values, facilitating precise specifications. Under the Curry-Howard correspondence, the dependent product \Pi x : A . B serves dual roles as a function space in the computational interpretation and as a universal quantifier \forall x : A . B in the logical one, where types represent propositions and terms represent proofs. This isomorphism embeds higher-order intuitionistic logic into CoC, with \Pi-types enabling polymorphic proofs that quantify over types or values. For instance, the polymorphic identity function is defined as \mathsf{id} = \lambda A : \mathsf{Type} . \lambda x : A . x, which inhabits the type \Pi A : \mathsf{Type} . \Pi x : A . A; here, the outer \Pi quantifies over types A, while the inner depends on the value x of that type, distinguishing it from non-dependent products like simple arrows A \to B. Unlike non-dependent systems such as the simply typed lambda calculus, CoC's dependent \Pi-types provide greater expressiveness for formalizing parameterized theorems as types, allowing proofs to be constructed as terms that carry computational content specific to those parameters.

Extensions and Applications

Defining Logical Connectives

In the Calculus of Constructions (), the Curry-Howard correspondence establishes a deep connection between logical proofs and typed terms, allowing logical connectives to be encoded directly as types within the impredicative sort , where propositions are interpreted as types and proofs as their inhabitants. This encoding leverages dependent product types (Π-types) to represent intuitionistic logical operators, enabling the construction of proof terms via abstractions without primitive logical constants. Logical A \to B, where A and B are propositions (i.e., types in ), is encoded as the non-dependent Π-type \Pi x : A . B. A proof for this implication is a \lambda x : A . M, where M : B, corresponding to the introduction rule for implication in . The application of such a term to a proof N : A yields (\lambda x : A . M) N : B, mirroring the elimination rule. The universal quantifier \forall x : A . B, with A : Type and B : Prop potentially depending on x, is identically encoded as the dependent product \Pi x : A . B. Proof terms are again lambda abstractions \lambda x : A . M(x), where M(x) : B for arbitrary x : A, providing a uniform treatment with implication under the Curry-Howard isomorphism. Conjunction A \land B is encoded in pure CoC using the higher-order type \Pi P : Prop . (A \to (B \to P)) \to P, which captures the universal property of the product: a proof of conjunction allows deriving any proposition P from a joint implication assuming both A and B. Given proofs a : A and b : B, the introduction term is \lambda P : Prop . \lambda f : A \to B \to P . f \, a \, b : A \land B. In extensions of CoC incorporating dependent sum types (Σ-types), conjunction can be directly represented as \Sigma x : A . B, with pair introduction \langle a, b \rangle and projections. Negation \neg A is defined as A \to \bot, where the false proposition \bot is encoded as the uninhabited type \Pi P : Prop . P, simulating an empty inductive type whose lack of constructors ensures no terms inhabit it in a consistent system. A proof of negation would thus require deriving an arbitrary proposition from A, which is impossible unless A itself leads to absurdity; in extensions with inductive types, \bot is explicitly defined as an empty inductive type. Equality between terms x, y : A is captured by the Leibniz type eq(A, x, y) := \Pi P : A \to [Prop](/page/Prop) . P \, x \to P \, y, stating that any P true of x is true of y. The reflexivity proof is refl := \lambda P : A \to [Prop](/page/Prop) . \lambda p : P \, x . p : eq(A, x, x), a that preserves any proof p under the . This encoding relies on the impredicativity of to ensure propositional behaves as expected in .

Inductive Types and Data Structures

The , an extension of the pure , incorporates inductive types to enable the definition of recursive data structures and primitive , addressing limitations in expressing natural numbers and similar constructs directly in pure CoC. In CIC, inductive types are introduced via a formation rule that specifies the type's sort (typically Set for computational content), parameters, and constructors, ensuring the type is the least fixed point closed under those constructors. This primitive support for contrasts with pure CoC, where natural numbers must be encoded impredicatively, such as via the Church-style encoding \mathsf{[nat](/page/Nat)} \equiv \forall \alpha : \mathsf{Set}, (\alpha \to \alpha) \to \alpha \to \alpha, which supports but leads to less efficient and due to the absence of dedicated . A canonical example is the natural numbers type, defined as \mathsf{Inductive}\ \mathsf{nat} : \mathsf{Set}\ :=\ |\ \mathsf{O} : \mathsf{nat}\ |\ \mathsf{S} : \mathsf{nat} \to \mathsf{nat}, where \mathsf{O} introduces zero and \mathsf{S} the . The formation rule for such an I with constructors c_i : Q_i requires that I appears only positively in each Q_i, a strict positivity condition that guarantees the well-foundedness of the inductive definition and prevents paradoxes like non-terminating recursions. This condition is verified during type checking: for instance, in \mathsf{nat}, \mathsf{nat} occurs positively in the type of \mathsf{S}. Universes in , such as the cumulative hierarchy \mathsf{Type}_i, allow inductive types to be large enough for proofs (in \mathsf{Prop} = \mathsf{Type}_0) while restricting impredicativity to small types, enabling efficient impredicative definitions of logical connectives over small inductive proofs. Elimination principles, or recursors, provide the means to define functions by primitive recursion over inductive types. For natural numbers, the recursor \mathsf{rect}_\mathsf{nat} has type \forall P : \mathsf{nat} \to \mathsf{Prop}, P\ \mathsf{O} \to (\forall n : \mathsf{nat}, P\ n \to P\ (\mathsf{S}\ n)) \to \forall n : \mathsf{nat}, P\ n, allowing proofs by ; for computational purposes in Set, a similar iterator or recursor enables definitions like : \mathsf{add}\ m\ n \equiv \mathsf{rect}_\mathsf{nat}\ (\lambda \_.\ \mathsf{nat})\ m\ (\lambda n\ p,\ \mathsf{S}\ p)\ n. These eliminators are accompanied by reduction rules that unfold recursions at constructor-headed terms, ensuring strong normalization. Inductive types also support more complex data structures, such as parameterized s: \mathsf{Inductive}\ \mathsf{list}\ A : \mathsf{Set}\ :=\ |\ \mathsf{nil} : \mathsf{list}\ A\ |\ \mathsf{cons} : A \to \mathsf{list}\ A \to \mathsf{list}\ A, with an eliminator for case analysis and like \mathsf{list}_\mathsf{rect}. Dependent inductive types extend this to indexed families, as in vectors of fixed length: \mathsf{Inductive}\ \mathsf{vector}\ A : \mathsf{nat} \to \mathsf{Set}\ :=\ |\ \mathsf{vnil} : \mathsf{vector}\ A\ 0\ |\ \mathsf{vcons} : \forall n : \mathsf{nat}, A \to \mathsf{vector}\ A\ n \to \mathsf{vector}\ A\ (\mathsf{S}\ n), where the index \mathsf{nat} depends on the structure itself, leveraging dependent types for length-indexed operations. This primitive in CIC facilitates efficient implementations in proof assistants like , filling the completeness gap of pure CoC by natively supporting without cumbersome encodings.