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.