|
The calculus of constructions (CoC) is a higher-order typed lambda calculus where types 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. The CoC is strongly normalizing, though, from Gödel's incompleteness theorem, it is impossible to prove this property within the CoC since it implies consistency. The CoC was initially developed by Thierry Coquand. The CoC was the basis of the early versions of the Coq theorem prover; 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.
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: The calculus of constructions has 4 types of objects: Judgements In the calculus of constructions, a judgement is a typing inference: Which can be read as the implication If variables have types , then term has type . The valid judgements 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 If is a valid judgement, then so is Inference rules for calculus of constructions Defining logical operators The calculus of constructions is very parsimonious when it comes to basic operators: the only logical operator for forming propositions is . However, this one operator is sufficient to define all the other logical operators: egin A Rightarrow B & equiv & orall x:A . B & (x otin B) \ A wedge B & equiv & orall C:P . (A Rightarrow B Rightarrow C) Rightarrow C & \ A vee B & equiv & orall C:P . (A Rightarrow C) Rightarrow (B Rightarrow C) Rightarrow C & \ eg A & equiv & orall C:P . (A Rightarrow C) & \ exists x:A.B & equiv & orall C:P . ( orall x:A.(B Rightarrow C)) Rightarrow C & end Defining data types The basic data types used in computer science can be defined within the Calculus of Constructions: Booleans Naturals (A Rightarrow A) Rightarrow (A Rightarrow A) Product Disjoint union Topics | ||||||||
|
| |||||||||
 |
|
| |