Lazi

Quelle récurrence ?

Contexte

Pour prouver la validité de la traduction Lazi.1 vers Lazi.0, il faut prouver que :

  • chaque étape de la traduction retourne une preuve Lazi.1 valide
  • que le nombre d'étape de traduction est finie
  • que la preuve finale est Lazi.0

Pour prouver que le nombre d'étapes est fini, il faut trouver une fonction de mesure qui décroît strictement à chaque étape de la traduction.

Question

Quels sont les étapes et la fonction de mesure adéquate ?

Étude

Traduction en deux passes, par début et par déduction d'ajout

Présentation

Passe 1

Quand on rencontre une déduction d'ajout on parcours le reste de la preuve pour la traduire partout, sous-preuves incluses. Il faut mémoriser les différentes formules qui sont déduites comme égales à l'énoncé premier de la déduction d'ajout, quand on parcourt les sous preuves cette mémoire doit être local à la sous-preuve.

En parcourant la preuve on élimine en même temps les déductions égalité et vérité reliée à l'énoncé premier de la déduction d'ajout.

Remarque: si une autre déduction d'ajout collisionne l'un des énoncés égaux, on élimine des déductions "égalité et vérité" pour cette déduction d'ajout, mais ça ne gêne pas.

Passe 2

On remplace les mots clés Lazi.1 par une valeur fixe quelconque.

Traduction en deux passes, tout en même temps

Présentation

Passe 1

On garde en mémoire les déductions d'ajouts rencontrées ainsi que les énoncés équivalents, cette mémoire est appelée ici le "contexte". On parcours les sous-preuves. On traduit tout ce que l'on rencontre (sauf le remplacement des mots clés dans les déductions restantes). On n'a pas besoin de remplacer la sous-preuve d'un proofT par son contenu.
Pour les sous-preuves, on doit garder une mémoire locale à la sous-preuve du contexte.

Les sous-preuves des déductions d'ajout sont traduites avant que la déduction d'ajout soit ajoutée au contexte. On peut noter que le résultat de cette traduction est en Lazi.0.0 augmenté des variables éventuelles provenant de la déduction d'ajout, sauf pour "imply" (car il manque d'avoir vu la preuve de l'hypothèse).
Pour "imply", la traduction de la preuve est refaite au moment de la traduction de la déduction d'application. Ce ne serait pas pareil de ne faire la traduction de la preuve de imply que lors de remplacement de la déduction d'application, car on pourrait alors créer des boucles (voir exemple "(1b = 1b) ⇒ (1b = 1b)" du bestiaire).

Passe 2

On remplace les mots clés Lazi.1 par une valeur fixe quelconque.

Finitude

Plan de preuve

On remplace/détruit/laisse intacte les déductions , donc si chaque remplacement est fait par une déduction finie, on aboutit à une preuve finie.
Les seuls remplacements qui pourraient aboutir à une preuve infinie sont ceux où l'on remplace la déduction par une preuve. Il nous suffit donc de vérifier que les sous-preuves sont finies après traduction.

Le remplacement d'une déduction par une preuve peut se faire par une preuve copiée telle quelle ou transformée, celle ci peut provenir de la déduction à traduire (comme pour la déduction d'application de "or") une d'une déduction antérieure (comme pour la déduction d'application de "forAll"). Pour la traduction, les différents types de transformations des preuves sont:

  • le remplacement d'une variable (par exemple pour "forAll")
  • la traduction des déductions restant à traduire : cas uniquement pour "imply" où la preuve peut contenir des déductions d'application associées à l'hypothèse.

Si on liste les sous-preuves de la preuve principale, dans l'ordre d'apparition lors du parcours pour la traduction, on peut constater qu'elles sont traduites à partir des preuves précédentes, sauf pour les preuves provenant

Une preuve d'une déduction d'ajout d'une application ne peut avoir qu'une sorte de déduction non traduite: une déduction d'application faisant référence à l'hypothèse. Ces déductions sont en nombre quelconque mais font toute référence à la même phrase mathématique.
Si l'hypothèse n'est pas une implication, alors la traduction de la déduction d'application restant à traduire est faite par soit:

  • une preuve antérieure déjà entièrement traduite
  • pour une hypothèse "or" ou "exists": une preuve interne : par récurrence elle peut être entièrement traduite.
Si l'hypothèse est une implication, alors la traduction de la déduction d'application restant à traduire passe par une preuve partiellement traduite. Si l'hypothèse de récurrence a en paramètre le niveau de profondeur des implications, on peut déduire par récurrence que la traduction ne boucle pas (car on est descendu d'un niveau et donc on peut utiliser la récurrence).

Critère de récurrence

On voit que le critère de récurrence doit avoir en argument un critère de longueur de preuve (à préciser) et un critère de niveau de profondeur des implications.

Essai 2

Le critère est le nombre de déduction dans les preuves et les sous-preuves.

Essai 1

Soit L = Lazi.0.0 avec en plus les mots clés forAll, exists, and, or, imply.
Pour n et m deux entiers naturels, soit H n m = Pour toute preuve Lazi.1 p, tr1 p est une preuve dans L où les listes de déductions des preuves et sous-preuves sont de longueur ≤ n et où les profondeurs d'implication des assertions des déductions d'ajout d'implication est ≤ m.

Preuve

On a H 1 1 car on ne peut avoir de couple déduction ajout/application.

Soit n et m tel que l'on ait H n m.

Montrons H (n+1,m)

Réponse

@todo