Lazi

Traduction d'un calcul multi-valeurs

Contexte

On a définiit le calcul multi-valeurs, pour raisonner dessus il est utile de le traduire en un ensemble de calculs (de démultiplexer le calcul).

Question

Quel est l'algorithme pour démultiplexer un calcul ?

Étude

Démultiplexer une formule

Comme il n'y a pas de multiFormulaT dupliqués, il suffit d'utiliser la méthode évidente, on peut même utiliser les règles pour pousser les multiFormulaT vers la racine, et quand il n'y en a plus qu'un on a la liste des formules. Il faut ajouter le développement quand un multiFormulaT est à l'intérieur d'un autre.

Démultiplexer un calcul multi-valeurs

Quand on duplique un multiFormulaT on cré une valeur et des nouvelles formules. Donc on ne peut pas voir un calcul multi-valeurs comme un ensemble de calculs à moins de ne pas créer de nouveau multiFormulaT.

Si on ne cré pas de nouveau multiFormulaT, ou si on en cré temporairement qui seront détruit, alors on peut traduire un calcul. Pour cela on reproduit les calculs élémentaires multi-valeurss sur les formules démulti-valeurses.

Réponse

On a un algorithme (voir la description rapide dans l'étude) que quand on ne cré pas de multiFormulaT ou que l'en en cré qui ne sont pas utilisés (par exemple dans un calcul de l'application d'un argument multiFormulaT dans une fonction où seulement un multiFormulaT restera).