É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 a₁ < a₂ ... < a_n < a₁, cela implique que l'on peut écrire a₁ de la forme a₁ = f a₁ et donc que a₁ est un argument ignoré (sinon a₁ 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 :

Si a différent de b alors a est strictement utilisé dans le calcul de b et b est strictement utilisé dans le calcul de a, donc a est strictement utilisé dans le calcul de a. Cela implique qu'à l'intérieur du calcul de a on passe par le calcul de a. On a donc un calcul récursif infinie, et donc a n'est pas calculable, ce qui est absurde. Comme l'énoncé "a = b" est booléen, on déduit que a = b.

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.