Lazi

normalisation d'un calcul s-loose

Contexte

L'intérêt de s-loose est de représenter la partie sur laquelle le calcul est réellement effectué. La normalisation consistera donc à réduire au maximum la zone désigné par le calcul élémentaire. Notamment les caculs sur les conditions des if seront réduite au calcul directement sur la sous-formule condition.

Nous allons ici définir des fonctions qui rendent les calculs uniques:

  • en n'autorisant pas le calcul le calcul de la condition d'un if par le calcul du if.
  • en réduisant le SFP au minimum.

Définition

Normalisation d'un calcul élémentaire s-loose

Soit s un NFSFP représentant un calcul élémentaire s-loose sur une formule x. Ce calcul élémentaire normalisé est l'application composée des deux sous-fonction de normalisation suivante :

  • si la fonction minimale désigné par s est le mot if, alors retourne la normalisation du calcul élémentaire représenté par le SFP du la condition de l'expression "if".
  • ajoute à s autant de 0b que possible tant que cela ne change pas le calcul.

Normalisation d'un calcul non élémentaire s-loose

On applique la normalisation à chaque élément du calcul.