Download Preuves Constructives

21 janvier 2005
et pour le
k -ème
37
constructeur :
Constr(k, Ind(nom : A){C1 ; . . . ; Cp })
nom
peut être vu comme un lieur dans la déclaration de l'inductif ce qui permet d'identier des
déclarations inductives isomorphes (même arité, même nombre de constructeurs avec les mêmes
types d'argument).
Dans cette approche, si toutes les occurrences de
nom
dans les types d'arguments sont appli-
z1 , . . . , zp alors les paramètres peuvent être vus comme des abstractions. On
Ck0 en remplaçant dans chaque type de constructeur
(nom z1 . . . zp ) par le nouvel identicateur nom' et on retrouve la dénition inductive
quées aux paramètres
construit de nouveaux types de constructeur
Ck
le terme
générale à l'aide des dénitions suivantes.
nom := λ(z1 : P1 ) . . . (zk : Pk ) ⇒ Ind(nom' : A){C10 ; . . . ; Cp0 }
cok := λ(z1 : P1 ) . . . (zk : Pk ) ⇒ Constr(k, Ind(nom' : A){C10 ; . . . ; Cp0 })
Une déclaration inductive avec paramètres peut se voir comme une famille de dénitions inductives.
3.2 Les déclarations non-récursives
Beaucoup des dicultés concernant les dénitions inductives apparaissent déjà au niveau
des dénitions non-récursives que nous étudions en premier. Dans un premier temps, nous ne
précisons pas la sorte de déclaration de la dénition inductive. Nous considérons également des
dénitions inductives sans paramètres car ceux-ci ne jouent pas de rôle essentiel.
3.2.1 Les déclarations de base
Les dénitions de base non récursives sont :
Zero (arité s, pas de constructeur)
Un (arité s, un constructeur de type Un)
Les types sommes (aussi appelés Σ-type) Σx : A.B (arité s, un constructeur de type
∀(x : A), B → Σx : A.B )
Les sommes disjointes A+B : (arité s, deux constructeurs de type A → A+B et B → A+B )
Égalité x =A y : (un paramètre x : A, arité A → s, un constructeur de type x =A x)
Si on suppose que l'on a un Σ-type : Σx : A.B avec deux projections : π1 : Σx : A.B → A et
π2 : (p : Σx : A.B)B{x := (π1 p)} alors il est aisé de dénir une somme n-aire :
La déclaration vide
La déclaration unitaire
Σ(x1 : A1 ; . . . ; xn : An )
∀(x1 : A1 ) . . . (xn : An ), Σ(x1 : A1 ; . . . ; xn : An ) et n projections πk :
∀p : Σ(x1 : A1 ; . . . ; xn : An ), (Ak {x1 , . . . , xk−1 := (π1 p), . . . , (πk−1 p)}. On notera (a1 , . . . , an )
l'élément de Σ(x1 : A1 ; . . . ; xn : An ) déni à l'aide du constructeur. Cette somme se dénit par
récurrence sur n. On pose Σ() ≡ Un, Σ(x : A) ≡ A, et Σ(x : A; x1 : A1 ; . . . ; xn : An ) ≡ Σx :
A.Σ(x1 : A1 ; . . . ; xn : An ).
De même on peut dénir une disjonction n-aire A1 + · · · + An comme étant Zero si n = 0,
A1 si n = 1 et dans le cas n > 1 A + A1 + · · · An ≡ A + (A1 + · · · An ).
avec un constructeur de type
À partir de ces constructions de base, on peut trouver un équivalent à toute dénition inductive non récursive. En reprenant les notations données en 3.1.1 et en introduisant la notation
pour
ΣA
Σ(a1 : A1 ; . . . ; an : An ) avec A ≡ ∀(a1 : A1 ) . . . (an : An ), s l'arité de la dénition inductive :
nom := λ(a1 : A1 ) . . . (al : Al ) ⇒
Σ(x1 : C11 ; . . . ; xn1 : C1n1 ; (a1 , . . . , al ) =ΣA (t11 , . . . , tl1 ))
+...+
n
Σ(x1 : Cp1 ; . . . ; xnp : Cp p ; (a1 , . . . , al ) =ΣA (t1p , . . . , tlp ))