4.1 The terms
In most type theories, one usually makes a syntactic distinction between types and terms. This is not the case for Cic which defines both types and terms in the same syntactical structure. This is because the type-theory itself forces terms and types to be defined in a mutual recursive way and also because similar constructions can be applied to both terms and types and consequently can share the same syntactic structure.For instance the type of functions will have several meanings. Assume nat is the type of natural numbers then nat®nat is the type of functions from nat to nat, nat ® Prop is the type of unary predicates over the natural numbers. For instance [x:nat](x=x) will represent a predicate P, informally written in mathematics P(x)º x=x. If P has type nat ® Prop, (P x) is a proposition, furthermore (x:nat)(P x) will represent the type of functions which associate to each natural number n an object of type (P n) and consequently represent proofs of the formula ``" x.P(x)''.
4.1.1 Sorts
Types are seen as terms of the language and then should belong to another type. The type of a type is always a constant of the language called a sort.The two basic sorts in the language of Cic are Set and Prop.
The sort Prop intends to be the type of logical propositions. If M is a logical proposition then it denotes a class, namely the class of terms representing proofs of M. An object m belonging to M witnesses the fact that M is true. An object of type Prop is called a proposition.
The sort Set intends to be the type of specifications. This includes programs and the usual sets such as booleans, naturals, lists etc.
These sorts themselves can be manipulated as ordinary terms. Consequently sorts also should be given a type. Because assuming simply that Set has type Set leads to an inconsistent theory, we have infinitely many sorts in the language of Cic . These are, in addition to Set and Prop a hierarchy of universes Type(i) for any integer i. We call S the set of sorts which is defined by:
| S | º { | Prop | , | Set | , | Type | (i)| i Î | I N | } |
The user will never mention explicitly the index i when referring to the universe Type(i). One only writes Type. The system itself generates for each instance of Type a new index for the universe and checks that the constraints between these indexes can be solved. From the user point of view we consequently have Type :Type.
We shall make precise in the typing rules the constraints between the indexes.
Remark: The extraction mechanism is not compatible with this universe hierarchy. It is supposed to work only on terms which are explicitly typed in the Calculus of Constructions without universes and with Inductive Definitions at the Set level and only a small elimination. In other cases, extraction may generate a dummy answer and sometimes failed. To avoid failure when developing proofs, an error while extracting the computational contents of a proof will not stop the proof but only give a warning.
4.1.2 Constants
Besides the sorts, the language also contains constants denoting objects in the environment. These constants may denote previously defined objects but also objects related to inductive definitions (either the type itself or one of its constructors or destructors).Remark. In other presentations of Cic, the inductive objects are not seen as external declarations but as first-class terms. Usually the definitions are also completely ignored. This is a nice theoretical point of view but not so practical. An inductive definition is specified by a possibly huge set of declarations, clearly we want to share this specification among the various inductive objects and not to duplicate it. So the specification should exist somewhere and the various objects should refer to it. We choose one more level of indirection where the objects are just represented as constants and the environment gives the information on the kind of object the constant refers to.
Our inductive objects will be manipulated as constants declared in the environment. This roughly corresponds to the way they are actually implemented in the Coq system. It is simple to map this presentation in a theory where inductive objects are represented by terms.
4.1.3 Language
Types.
Roughly speaking types can be separated into atomic and composed types.An atomic type of the Calculus of Inductive Constructions is either a sort or is built from a type variable or an inductive definition applied to some terms.
A composed type will be a product (x:T)U with T and U two types.
Terms.
A term is either a type or a term variable or a term constant of the environment.As usual in l-calculus, we combine objects using abstraction and application.
More precisely the language of the Calculus of Inductive Constructions is built with the following rules:
- the sorts Set, Prop, Type are terms.
- constants of the environment are terms.
- variables are terms.
- if x is a variable and T, U are terms then (x:T)U is a term. If x occurs in U, (x:T)U reads as ``for all x of type T, U''. As U depends on x, one says that (x:T)U is a dependent product. If x doesn't occurs in U then (x:T)U reads as ``if T then U''. A non dependent product can be written: T ® U.
- if x is a variable and T, U are terms then [x:T]U is a term. This is a notation for the l-abstraction of l-calculus[7]. The term [x:T]U is a function which maps elements of T to U.
- if T and U are terms then (T U) is a term. The term (T U) reads as ``T applied to U''.
Notations.
Application associates to the left such that (t t1... tn) represents (... (t t1)... tn). The products and arrows associate to the right such that (x:A)B® C® D represents (x:A)(B® (C® D)). One uses sometimes (x,y:A)B or [x,y:A]B to denote the abstraction or product of several variables of the same type. The equivalent formulation is (x:A)(y:A)B or [x:A][y:A]BFree variables.
The notion of free variables is defined as usual. In the expressions [x:T]U and (x:T)U the occurrences of x in U are bound. They are represented by de Bruijn indexes in the internal structure of terms.Substitution.
The notion of substituting a term T to free occurrences of a variable x in a term U is defined as usual. The resulting term will be written U{x/T}.