normalisation d'un calcul loose
Contexte
En loose il existe plusieurs manière de désigier un même calcul. Par exemple pour calculer if x y z t r — où x n'est pas un calcul terminé — on peut désigner x mais aussi la formule entière ou encore pour s-loose les formules if x y z ou if x y z t.
Nous allons ici définir des fonctions qui rendent les calculs uniques:
- en n'autorisant pas le calcul directe sur la condition d'une expression if quand on peut le faire sur l'expression if entière.
Donc pour reprendre notre exemple, la normalisation serait ∅l (désigne la formule entière) .
Définition
Normalisation d'un calcul élémentaire loose
Soit s un NFSFP représentant un calcul élémentaire loose sur une formule x. Ce calcul élémentaire normalisé est :
- Si s se termine par $L[0b,0b,1b] et qu'en remplaçant cette terminaison par $L[0b,0b,0b] on désigne l'endroit de x contenant le mot if, alors soit t = s sans ses les 3 derniers éléments. La normalisation du calcul élémentaire représenté par s est la normalisation du calcul élémentaire représenté par t.
- Sinon le calcul élémentaire représenté par s normalisé est lui-même.
Remarque : on doit appliquer le procédé de normalisation récursivement, car on peut avoir des if imbriqué, comme dans if (if x y z) t r.
Normalisation d'un calcul non élémentaire loose
On applique la normalisation à chaque élément du calcul.