Étude : Récurrence sur les sous-formules utilisées d'un calcul
Contexte
Pour raisonner par récurrence sur les calculs, il me semble bon de pouvoir ordonner les formules de sorte qu'une sous-formule y du calcul terminal d'une formule x soit plus petite que x.
Question
Existe-t-il un ordre sur les formules de sorte qu'une sous-formule y d'un calcul d'une formule x soit plus petite x ?
Étude
Les arguments ignorés
Supposons que :
- le calcul terminal de la formule a soit f b
- le calcul terminal de b soit g a
On devrait alors avoir b < a et a < b, ce qui est contradictoire.
Remarquons que l'on a a = f b = f \ g a , donc l'argument a est ignoré sinon la formule globale a ne serait pas calculable.
Si on avait une boucle a1 < a2 ... < an < a1, cela implique que l'on peut écrire a1 de la forme a1 = f a1 et donc que a1 est un argument ignoré (sinon a1 ne serait pas calculable).
Pour prouver l'existence d'un ordre à partir de l'argument ci-dessus, il faudrait développer la notion d'argument ignoré ou calculé.
L'ordre "est utilisé dans le calcul"
Soit x une formule calculable, Soit P la relation définie sur les formules utilisées dans le calcul de x définie par :
P a b ssi b est utilisé dans le calcul de a.
Nous allons prouver que P est une relation d'ordre:
- réflexivité : car la relation "est utilisé" est réflexive
- transitivité: oui car si c est utilisé dans le calcul de b qui est utilisé dans le calcul de a alors c est utilisé dans le calcul de a (car "y est utilisé dans le calcul de x" signifie que le calcul de x nécessite le calcul de y).
- antisymétrie : si a est utilisé dans le calcul de b qui est utilisé dans le calcul de a :
En général le calcul d'une formule comprend des sous-calculs indépendants (par exemple dans if a b c le calcul de a et b ou c est indépendant). De ce fait P n'est pas une relation d'ordre totale. Comme P a un domaine fini (P dépend de x), on peut étendre la relation d'ordre à une relation d'ordre totale.
Limitation aux formules utilisées dans le calcul
Une formule calculable peut contenir des sous formules non calculées (par exemple dans if 0b a b, a n'est pas calculé). Une sous-formule non calculée peut contenir des calculs récursifs. Donc on ne peut pas toujours trouver un ordre total sur toutes les sous-formules d'une formule calculable.
Et même plus, on peut avoir une formule calculable a vérifiant : a = if 0b (if 1b a a) b, et dans ce cas on voit que if 1b a a est une sous-formule de a qui contient a, donc on aurait a supérieur ou égal à if 1b a a qui est supérieur ou égal à a, on devrait donc en déduire a = if 1b a a, ce qui est faut (égalité syntaxique).
Donc on ne peut pas étendre le théorème a toutes sous-formules.