Lazi

trace d'un SFP dans un calcul

Contexte

Si on regarde les calculs élémentaires (distribute et if) du point de vue des endroits (des SFP), on constate qu'un calcul élémentaire est un ensemble de déplacements, duplications et disparitions. On veut ici représenter le lien entre un endroit de la formule de départ et de la formule résultante pour signifier que ce qui est à cet endroit est resté inchangé pour l'équivalence "égal par calcul".

Par exemple pour if 1b x y →c[loose]1 x, ∅l (l'endroit de la formule entière) est dans la trace de l'endroit de x ($L[0b,1b]) car x devient la formule entière. Aussi ∅l est dans la trace de ∅l car if 1b x y et x sont égaux par calcul.

Voir aussi le destin d'un SFP pour les informations sur la raison des changements.

Définition

Trace pour les calculs élémentaires

Soient

  • l un langage de calcul
  • x une formule
  • s un SFP sur x
  • c un calcul élémentaire en l
  • y le résultat du calcul c sur x
  • t un SFP sur y
On dit que t est dans la trace de s pour le calcul élémentaire c sur x ssi pour toute formule x2 telle que :
  • s est valide sur x2
  • c est valide sur x2
  • c sur x2 fasse appel à la même règle de calcul que c sur x
on a : la sous-formule de x2 en s est égale par calcul élémentaire l à la sous-formule du résultat de c sur x2 en t

Remarques :

  • Pour les calculs lazi.0.0, il peut y avoir de zéro à deux SFP dans la trace d'un SFP.
  • Les traces ne dépendent du calcul élémentaire utilisé, mais pas de la valeur de la formule.

Trace pour les calculs non élémentaires

Soient

  • l un langage de calcul
  • x une formule
  • s un SFP sur x
  • c un calcul en l valide sur x
  • pour n un entier entre 0 et le nombre d'élément de c : xc(n) est le résultat du calcul c tronqué à ses n premiers calculs élémentaires
  • pour n un entier entre 0 et le nombre d'élément de c : ce(n) est le n ième calcul élémentaire de c

La trace de s pour le calcul c sur x est un arbre tq :

  • chaque nœud contient un SFP
  • la racine contient le SFP s
  • si un nœud est à une profondeur n, alors son SFP sera valide sur xc(n)
  • soit t un SFP d'un nœud de profondeur n, le SFP u est un nœud enfant de t ssi u est dans la trace de t pour le calcul élémentaire ce(n) sur xc(n)