Download Preuves Constructives

21 janvier 2005
49
l'utilisateur de concevoir un schéma adapté et de le démontrer à l'aide de l'élimination récursive
et des constructions par point xe que nous allons maintenant introduire.
3.3.4 Condition de garde
Le schéma d'élimination récursive était proposé par P. Martin-Löf comme la construction
d'élimination de base des dénitions inductives. Il permet de capturer la notion de fonctionnelle
dénie de manière primitive récursive ainsi que la notion de preuve par récurrence structurelle.
Cependant, Th. Coquand a suggéré une approche alternative, où comme dans les langages
de programmation fonctionnelle, les notions primitives sont l'élimination non récursive (qui correspond à l'analyse par cas) et les dénitions par point xe. Évidemment, on ne peut autoriser
n'importe quel point xe sous peine de construire des termes non normalisables et d'aboutir à
une incohérence. Une condition syntaxique de garde permet d'accepter les dénitions qui suivent
un schéma primitif récursif et de préserver la terminaison.
Pour cela, une fonction
f
peut être dénie par point xe si un de ses arguments
type une dénition inductive et si dans le corps de
place de
x
un terme
t
f
tous les appels récursifs à
Case
sur
x
et d'être l'un des sous-termes de
x.
x
x
a pour
se font avec en
que l'on reconnaît syntaxiquement comme étant plus petit que
La règle principale pour être structurellement plus petit que
branche d'un
f
x.
est d'apparaître dans une
Mais cette dénition peut être
Case est reconnu plus petit que x si chacune de ses branches est plus
x (en particulier s'il n'y a aucune branche dans le cas de l'élimination d'une condition
étendue. Par exemple un
petite que
absurde). De même être plus petit est une opération transitive.
Les points xes de
Coq
sont représentés de manière anonyme par un terme :
Fix(f /n : T := t)
dans lequel
f
est une variable liée et
Γ, f : T ` t : T
f
n
est un entier positif ou nul. La règle de typage est :
t par le n + 1ème
Γ ` Fix(f /n : T := t) : T
est gardée dans
argument
La règle de réduction de point xe est :
an+1 commence par un constructeur alors :
(Fix(f /n : T := t) a1 . . . an+1 ) −→ι (t{f := Fix(f /n : T := t)} a1 . . . an+1 )
si
La règle de réduction est également gardée par la condition que l'argument de décroissance
commence par un constructeur. Ceci permet d'éviter de poursuivre la réduction du point xe à
l'intérieur du terme ce qui violerait la terminaison forte.
On dénit aisément à l'aide du point xe la fonction qui calcule le minimum de deux entiers :
Fix(min/0 : nat → nat → nat := [n, m]Case(nat, n, 0, [n0 ]Case(nat, m, 0, [m0 ](S (min n0 m0 )))))
Par contre la fonction d'Ackermann spéciée par les équations :
(ack 0 m) = (S m)
(ack (S n0 ) 0) = (ack n0 (S 0)) (ack (S n0 ) (S m0 )) = (ack n0 (ack (S n0 ) m0 )
nécessite l'utilisation de deux points xe imbriqués :
Fix(ack/0 : nat → nat → nat :=
[n]Case(nat, n,
S,
[n0 ]Fix(ackn/0 : nat → nat :=
[m]Case(nat, m, (ack n0 (S 0)), [m0 ](ack n0 (ackn m0 ))))
))