Project topics and materials
Get Complete Project Material File(s) Now! »
The Calculus of Congruent Inductive Constructions
The Calculus of Congruent Inductive Constructions is a modi cation of the Calculus of Inductive Constructions which embeds in its conversion the validity entailment of a xed rst-order theory over equality.
This chapter is organized as follow. We rst recall the full de nition of the Calculus of Inductive Construction as described in [48], with the restrictions given in [5]. We then introduce parametric multi-sorted theories. These theories play a crucial role as they will be embeded into the conversion relation of CCIC. Last, we de ne our calculus, and describe in details how theories are built in the conversion relation.
The Calculus of Inductive Constructions
Terms of the calculus
We start our presentation by rst describing the terms algebra of the Calculus of Inductive Constructions.
CIC uses two sorts : (or Prop, or object level universe ) and (or Type, or predicate level universe ). We denote t ; u, the set of CIC sorts, by S.
We use two classes of variables: let X (resp. X ) be a countably in nite set of term variables (resp. predicate variables ) such that X and X are disjoint. We write X for X YX.
Example 3.4
The constructors of nat : IndpX : qtX; X — Xu are clearly all strictly positive. A more complicated example using the de nition of constructor types in all its generality is the one of enumerable ordinals ord : IndpX : qtX; X — X; pnat — Xq — Xu whose constructor types are all strictly positive. See example 3.7 for an example of a non-strictly positive constructor type.
Strong and Weak ¶-reduction
CIC distinguishes two kinds of ¶-elimination: the strong one, when the terms constructed by induction are at predicate level, and the weak one, when they are at object level. (The categorization of terms which de nes these levels is given later) To ensure logical consistency, strong ¶-elimination is restricted to small inductive types, i.e. to inductive types whose constructors do not take a predicate as argument:
Definition 3.8 Small inductive types
A type constructor @pxi : Tiq: X t in X is small if all the xi’s are in X (or equivalently for terms that are typable, if all the Ti’s are of type in their respective environments). If not, it is called a big type constructor. An inductive type is small if all its constructor types are small.
Parametric multi-sorted theories with constructors
We choose to embed into the Calculus of Constructions any rst-order theory expressed by a parametric multi-sorted algebra, with some restrictions for the notion of constructor symbols. These algebras can be easily mapped to the Calculus of Inductive Construction and are expressive enough to describe any theory we want to embed in the calculus and for which a decision procedure exists: linear arithmetic, datatypes, non-interpreted algebras, rings.
Signature
The rst part of this section is taken from the de nition of parametric multi-sorted algebras, with some restrictions for the introduction of constructor symbols.
Example 3.14
Examples of sorts are the sort nat of natural numbers, or listpnatq of lists over natural numbers, nat (resp. list) being a sort constructor of arity 0 (resp. of arity 1).
Definition 3.15
A signature in parametric multi-sorted algebra is a pair p⁄E; §q where i) ⁄E is a set of sorts, ii) § is a nite set, disjoint from all others, of function symbols, and iii) an arity of the form @ # # fi: ¿1 ¿n — ¾ is attached to any symbol f P §, where fi if the set of sort variables occurring in ¿1; : : : ; ¿n; ¾ and all the sort variables occurring in ¾ occur in the ¿i’s.
We distinguish a subset §C of §, called set of constructor symbols, the arity of which must be of the form @fi1; : : : ; fin: ¿1 ¿n — ¾pfi1; : : : ; finq.
Function symbols of § §C are called de ned symbols.
Notation. When x in not free in t, @px :a Tq: t will be written T —a t. The default anno tation, when not speci ed in a product or abstraction, is the unrestricted (u) one.
From now on, let O and O be two arbitrary set of CCIC terms, whose elements are called extractable terms and convertible terms. The set O will be used in the de nition of conversion to restrict the set of extractable equations for a given environment: only equation of the form t 9 u with t and u in O shall be extractable. The set O is used later to restrict the set of terms on which rst-order deduction is applied.
Taking O O O (see De nition 3.34) does not compromise most standard calculus properties but it does compromise decidability of type-checking. For example, if T is the Presburger arithmetic, allowing the extraction of ‚rx : nats: f x 9 ‚rx : nats: f px 9 2q would later require to decide any statement of the form T ( p@x: fpxqfpx 2qq Ò t u, which is well known to be impossible. Our assumptions on O and O will come later, when proving meta-theoretical properties of CCIC and describing the type-checking algorithm.
We also assume a set of CCIC terms P . This set is used later to restrict the types of variables of X .
We now de ne the set of CCIC well-sorted terms. Well-sorted are s.t. fl-reduction always replaces variables of X and X by terms of O and P . Hence, we must forbid pseudo-terms which contain subterms of the form p‚rx :a Us: tq u with x P X and u R O (resp. x P X and u R P ). Since, as in CCN, we do not want terms of the form p‚rx :r Us: tq u and since, we want well-sorted terms to be stable by reduction, we obtain the following de nition:
Definition 3.33 Well-sorted terms
A CCIC pseudo-terms t is well-sorted if:
• t does not contain, on the right of an application or in the branch of a recursor, an unapplied subterm of the form ‚rx :a Us: t with x P X Y x P X or a r.
• If t contains a subterm of the form p‚rx :a Us: tq u, then a u and if x P X (resp. x P X ) then u P O (resp. u P P ).
Moreover, if CpXq @pxi : Uiq: X u is a constructor type, the xi’s and X are not element of X Y X
Definition 3.35 Pseudo-contexts of CCIC
The typing environments of CIC are de ned as ¡; ¢ :: rs | ¡; rx :a Ts s.t. a variable cannot appear twice in the left-hand side of a colon. Moreover, if x P X , then we require T to be in P . We use domp¡q for the domain of ¡ and x¡ for the type associated to x in ¡.
We can now de ne the CCIC typing judgment ¡ $ t : T. The rules de ning ¡ $ t : T are a mix of the ones of CCN (notably for the [App] rule side conditions) and the CIC ones (for inductive types):
Definition 3.36 Typing judgement
The typing judgment ¡ $ t : T is de ned by the rules of Figures 3.5 and 3.6, where fl¶
• −— is a rewriting relation on CCIC, including −—-reduction. Its precise de nition is given later.
• For any typing environment ¡, ¡ is the conversion relation of CCIC under environ ment ¡. As for −—, its precise de nition is given later.
• WT is a set of terms. Again, its precise de nition is given later.
Notation. A term t is well-formed (or well-typed ), denoted by ¡ $ t, if there exists T s.t.
¡ $ t : T. A typing environment is well-formed, denoted by ¡ $, if there exists a term t s.t. ¡ $ t.
Definition 3.37
Among well-typed terms, we distinguish:
• The set Op¡q of well-typed objects under ¡, i.e. the set composed of terms t s.t. ¡ $ t : T and ¡ $ T : for some T.
• The set Pp¡q of well-typed predicates under ¡, i.e. the set of terms T s.t. ¡ $ T : K and ¡ $ K : for some K.
• The set Kp¡q of well-typed predicate types under ¡, i.e. the set of terms T s.t. ¡ $T: .
We now de ne a notion of well-formed substitution. In the Calculus of Constructions, a substitution µ is well-formed from a typing environment ¡ to a typing environment ¢ if for all x P dompµq, ¢ $ xµ : x¡. One can then easily prove ¢ $ tµ : T µ if ¡ $ t : T – a property called stability by substitution.
Assume now that ¡ is a typing environment of the form ¡1; rx :r a 9 bs; ¡2 (a and b being two terms in the set of extractable terms O ). Stability by substitution claims that if we have a derivation of the form ¡ $ t : T, then we can substitute x by a any term P (s.t. ¡ $ P : a 9 b) in the derivation ¡ $ t : T and obtain a proof of ¡1; ¡2µ $ tµ : T µ, where µ tx fi—Pu. However, this is not true in general since the equation a 9 b is then removed from context and not usable in the de nition of ¡1;¡2µ. Hence, aµ ¡1;¡2µ bµ does not hold in general, and ¡1; ¡2µ $ tµ : T µ is not necessarily derivable.
Another problems arise when substituting variables in extractable equations. Suppose now that ¡ $ ‚rp :r a 9 bs: u with a and b in O . Stability by substitution now leads to ¢ $ ‚rp :r aµ 9 bµs: uµ. Again, for this result to hold, we need aµ and bµ to be extractable, i.e. O has to be stable by application of a well-formed substitution.
A substitution µ is well-sorted from ¡ to ¢, written µ : ¡ „— ¢, if
• @x P dompµq, x is not annotated by r in ¡,
• if x is annotated by r is ¡, then x P domp¢q, x is annotated by r in ¢, and x¢x¡ µ.
• @x P dompµq, if x P X then xµ P O ,
• @x P dompµq, if x P X then xµ P P ,
• @x P dompµq: ClasspxqClasspxµq.
• @x P dompµq: xµ is a weak term.
Moreover, if for all x P dompµq, ¢ $ xµ : x¡ µ, then we say that µ is well-formed, written µ : ¡ ˆ ¢. Incorporation of a PMS algebra into CCIC
We start out incorporating of a parametric theory into CCIC. From now on, let ⁄E be a sort signature and § a ⁄E-signature.
Translation of sort constructors and function symbols
We introduce into CCIC two new sets of symbols: a set of type level symbols ⁄ t¾ | ¾ P ⁄u, and a set of object level symbols § tf | f P §u. We then assign for any object (resp. type) level symbol a type level (resp. kind level) CCIC terms denoting the translation of their arities.
Conversion relation
From now on, let —− be a rewriting system, de ned as the union of −— and −— where R is the translation of a §-rewriting system.
We are now left to de ne our conversion relation ¡ . The two main di erences with CCN are the following.
• Our notion of algebraisation now works modulo the expected sort of the resulting rst-order term. This is the aim of the next section.
• A notion of weak terms is introduced in Section 3.3 so that conversion operates only on them – the others being only converted with —−-reductions. This is needed to forbid inconsistencies at object level to be lift up to the type level.
We start with our new notion of algebraisation.
Algebraisation
Algebraisation is the rst part of the hypotheses extraction: it allows transforming a CCIC term into its rst-order counterpart. We illustrate the di culties with examples.
The case for pure algebraic terms is as for CCN. The de nition becomes a little harder for parametric signatures. The theory of lists gives us a simple example. From the definition of conversion of an algebra to CCIC, we know than the app symbol has type @pA : q: list A — list A — list A
Thus, a fully applied, well formed term having the symbol app at head position is necessarily of the form app T l l1 , T being the type of the elements of the list. Algebrai sation of such a term will erase all the type parameters: in our example, Apapp T l l1 q apppAplq; Apl1 qq.
Our conversion being de ned on non well-formed terms, we now come to the case of algebraisation of non-pure algebraic terms or even ill-formed terms. As for CCN, for non-pure algebraic terms, the problem is solved by abstracting non-algebraic subterms with fresh variables. For example, algebraisation of 1 t with t non-algebraic yields 1 xnat where xnat is an abstraction variable of sort nat for t. The problem is harder for:
• parametric symbols : in pcons T t pnil Uqq with t non algebraic, should t be abstracted by a variable of sort nat or listpnatq ?
• ill-formed terms : should pcons T 0 pcons T pnil Uq pnil Tqqq be abstracted as a list of natural numbers or as a list of lists ?
The solution adopted here is to postpone the decision: Aptq is de ned as a function from ⁄E to the terms of T s.t. Aptqp¾q is the algebraisation of t under the condition that t is a CCIC representation of a rst-order term of sort ¾.
We now give the formal de nition of Ap q.
Let tY¾u¾ be a î⁄E-sorted family of pairwise disjoint countable in nite sets of variables of sort ¾. Let Y ¾ Y¾.
For any x P X and sort ¾ P ⁄E, let x¾ be a fresh rst-order variable of sort ¾. We denote by Z ¾ the set tx¾ | x P Xu and by Z the set î Z .
For any equivalence relation R and sort ¾ P ⁄E, we suppose the existence of a function …¾R : CCIC — Y¾ s.t. …¾Rptq …¾Rpuq if and only if t R u (i.e. …¾Rptq is the element of Y¾ representing the class of t modulo R).
Note that, as explained before, the algebraisation does not only depend on the terms being abstracted, but also on the expected sort of the result. This is clearly seen on the example: when abstracting the (heterogeneous and ill-formed) list 0 :: nil :: nil as a list of lists, 0 is seen as an alien and thus abstracted. Conversely, when this list is abstracted as a list of natural numbers, 0 is considered algebraic but the nil element is then seen as an alien and abstracted. Of course, as clear from the last case, if the list is algebraised as a natural number, it gets directly abstracted by a variable.
Table of contents :
1 Introduction
1.1 A brief history of type theory
1.2 Safety of Proof assistants
1.3 Contributions
1.4 Outline of the thesis
2 The Calculus of Presburger Inductive Constructions
2.1 Terms of the calculus
2.2 The conversion relation
2.3 Two simple examples
2.4 Typing rules
2.5 Consistency
3 The Calculus of Congruent Inductive Constructions
3.1 The Calculus of Inductive Constructions
3.2 Parametric multi-sorted theories with constructors
3.3 The calculus
4 Meta-theoretical Properties of CCIC
4.1 Conuence on well-sorted terms
4.2 Monotony of conversion
4.3 Weakening
4.4 Substitutivity
4.5 Product compatibility
4.6 Correctness of types
4.7 Subject reduction
4.8 Type unicity
4.9 Strong normalization
5 Deciding CCIC
5.1 Decidability of conversion relation
5.2 A syntax oriented typing judgment
5.3 Deciding more theories
6 Conclusion and perspectives
6.1 Stability of extractable equations
6.2 Using a typed extraction
6.3 Weak terms
6.4 Extending CCIC to CAC
6.5 Embedding a more powerful logic
Bibliography
