Lazi

arbre d'un calcul loose ordonné

Contexte

On représente un calcul par une liste des endroits où un calcul élémentaire doit être effectué. Ici nous allons, pour les calculs ordonnés par niveau, représenter les calculs par un arbre binaire ayant la même forme que la formule résultante et où chaque nœud contient le nombre de calculs élémentaires à effectuer sur l'endroit représenté par le nœud.
À partir d'une telle représentation on peut retrouver le calcul, cela repose sur le fait que pour un calcul ordonné, la forme des arbres représentant les formules résultantes intermédiaires convergent ver la forme du résultat final.

Définition

Soient

  • x une formule
  • c un calcul loose sur x qui est ordonné par les niveaux de NFSFP.
  • c0 la plus longue sous-liste de c où le dernier calcul élémentaire porte sur la formule entière.
  • x0 le résultat du calcul c0 sur x (x0 est un résultat intermédiaire pour le calcul c).
  • cf, c privé de c0 et des calcul élémentaire dont l'endroit est intérieur à la partie argument.
  • ca, c privé de c0 et des calcul élémentaire dont l'endroit est non intérieur à la partie argument.

Alors t est la représentation par arbre de c ssi

  • t est un arbre binaire où chaque nœud contient un entier naturel.
  • Le nombre à la racine est la longeur de c0.
  • Si x0 n'est pas une application alors la racine de t n'a pas d'enfant.
  • Si x0 est une application alors la racine de t a deux enfants :
    • l'enfant de gauche est la représentation par arbre de (cf,x0)
    • l'enfant de droite est la représentation par arbre de (ca,x0)