Lazi

Théorème du calcul trié

Contexte

Pour raisonner sur les calculs, on cherche à les reformuler sous une forme comparable. Pour cela on trie les calculs élémentaires par leur niveau.

Énoncé

Définitions

Définition des entiers naturels associés au NFSFP

Un NFSFP est représenté par une liste binaire se terminant par un 1b. Exceptionnelement ici le nombre binaire associé est dans l'ordre inverse : le bit le plus fort est en queue (cet un choix pour abréger la définition).

Définition d'un ordre total sur les NFSFP

Nous allons définir un ordre total sur les NFSFP.
Soient x et y deux SFP, on a x ≥ y ssi on a la disjonction :

  • si le nombre de 1b dans la liste du x est strictement supérieur au nombre de 1b dans la liste de y.
  • si le nombre de 1b est égal et que le nombre binaire représenté par la liste x est supérieur ou égal à celui d'y.

Remarque: le nombre de 1b est appelé le niveau du NFSFP ou du calcul élémentaire.

Cet ordre est total car les listes binaires des NFSFP se terminent par 1b, donc tous les bits sont pris en compte dans la comparaison, cela repose donc sur l'ordre total des entiers naturels.

Conclusion

Il existe une fonction orderedCalc sur les calculs tq pour toute formule x et tout calcul loose c compatible avec x, on a:
orderedCalc c est équivalent à c sur x

  • Les calculs élémentaires de orderedCalc c sont en ordre croissant par l'ordre défini ci-dessus
  • Les calculs sur les conditions des if sont exprimés en tant que calcul sur l'expression contenant le if correspondant (voir la remarque ci-dessous).

Remarque : en calcul loose on peut calculer la condition d'un if en donnant directement l'adresse de l'argument ou en donnant l'adresse de la sous-formule entière contenant le if, la dernière condition empêche cette double représentation de ce calcul.

Preuve

Définition de la fonction d'inversion "norm"

La fonction norm est la fonction de normalisation du calcul loose déjà définie.

Définition de la fonction d'inversion "inv"

Nous allons définir une fonction "inv" qui :

  • Prend en argument un calcul constitué de deux calculs élémentaires. Le premier est dénomé "précédent" et le deuxième "principal" (car il est d'un niveau moindre).
  • Retourne, suivant l'ordre défini ci-dessus sur les NFSFP :
    • Ordre inverse (le plus petit en deuxième) : Retourne un calcul équivalent où le premier calcul élémentaire est le calcul principal et où les éventuels calculs élémentaires suivant sont inférieurs au calcul principal.
    • Ordonné : l'argument inchangé

Si les NFSFP des deux calculs élémentaires sont disjoints

Voir SFP disjoints.
Dans ce cas les deux calculs ne s'impactent pas l'un l'autre.
→ On a juste à inverser les deux calculs élémentaires.

Si le niveau de calcul principal est 0 et que le calcul précédent porte sur l'intérieur du calcul principal

On se place dans ce cas pour simplifier, on généralisera ces cas plus tard.

Nous divisons les cas suivant la forme de la formule sur laquelle porte le calcul principal :

"f a1 a2 ... an" où le calcul précédent porte sur ou à l'intérieur d'un argument ak où k>3.

Comme l'argument calculé dans le calcul précédent ne concerne pas la partie de formule modifiée, et que l'adresse de l'argument reste inchangé par le calcul principal :
→ On a juste à inverser les deux calculs élémentaires.
Remarque: le résultat du calcul élémentaire sur f a1 a2 a3 peut être "if", et le calcul précédent peut être un calcul élémentaire de a4, dans ce cas le calcul précédent sera normaliser par la suite par "norm" (voir ci-dessous).

"if a1 a2 ... an" où a1 est 0b ou 1b et où le calcul précédent porte sur ou à l'intérieur de l'argument (a2 ou a3) abandonné.

Comme l'argument sur calcul précédent n'a pas de conséquence :
→ On détruit le calcul préçédant.

"if a1 a2 ... an" où a1 est 0b ou 1b et où le calcul précédent porte sur ou à l'intérieur de l'argument retourné (a2 ou a3).

On peut inverser les deux calculs, il faut juste tenir compte du changement de SPF.
→ On inverse les deux calculs en relativisant le NFSFP du calcul préçédant pour l'adapter au nouvel endroit.

"if a1 a2 ... an" où a1 n'est ni 0b ni 1b et si le calcul précédent porte sur la condition du if.

C'est donc la condition du if qui est calculée. Le calcul préçédent étant de niveau supérieur, il porte sur l'intérieur de la condition. On se retrouve donc dans le même cas qu'une inversion de calcul où la formule générale est la condition. On peut donc appliquer les mêmes règles.
→ On relativise les deux calculs élémentaires comme si la condition était la formule générale, on applique les règles d'inversion, puis on relativise le résultat pour qu'il porte sur la condition.

"if a1 a2 ... an" où a1 n'est ni 0b ni 1b et si le calcul précédent porte sur autre chose que la condition du if.

Les calculs sont indépendants, on peut donc les inverser sans les modifier.
→ On a juste à inverser les deux calculs élémentaires.

"distribute a1 a2 ... an" où le calcul précédent porte sur ou à l'intérieur d'un argument ak où 1 ≥ k ≥ 3.

La sous-formule calculée par le calcul précédent n'est pas modifiée par le calcul "distribute", mais seulement déplacée et éventuellement dupliqué pour a3. On pourra donc inverser en s'adaptant au déplacement et à l'éventuelle duplication.
→ On inverse les deux calculs. On adapte le calcul précédant à la nouvelle place de l'argument. On duplique le calcul précédent s'il portait sur l'argument a3 où chacun des calculs dupliqué portera sur l'une des duplication.

Si le niveau de calcul principal est >0 et que le calcul précédent porte sur l'intérieur du calcul principal

On peut appliquer les règles où le calcul principal est de niveau 0, en relativisant à la sous-formule concernée.

Propriété de "inv"

Il nous faut montrer que inv retourne un calcul équivalent où le premier calcul élémentaire est le calcul principal et où les éventuels calculs élémentaires suivant sont d'un niveau inférieur.

La preuve est simple et longue, elle consiste à prouver la propriété pour les différents cas de la définition. C'est pourquoi nous ne la détaillons pas là.

Définition de la fonction "normInv"

C'est la composition norm ∘ inv ∘ norm

Définition de la fonction d'inversion "orderedCalc"

La fonction orderedCalc prend en argument un calcul et retourne un calcul équivalent trié par "normInv". Il nous faut choisir une des nombreuses manières de trier, on utilisera ici le trie à bulle. Remarquons qu'il faut l'adapter à la variabilité du la taille du calcul au cours du trie.

Propriété de "orderedCalc"

Nous devons prouver que la valeur retournée par "orderedCalc" vérifie les conclusions. Comme nous avons déjà que "normInv" ordonne les cacluls élémentaires deux à deux, il reste à prouver que le trie ordonne l'ensemble du calcul. Comme les algorithmes de trie sont simples et classiques, nous passerons aussi cette preuve.

@theorem