Lazi

destin d'un SFP dans un calcul

Contexte

Avec la trace d'un SFP dans un calcul, on s'intéresse à ce qu'il advient à une sous-formule du point de vue de sa position. Ici on s'intéresse à la raison des changements ou non changements. On pourra voir le théorème sur les positionnements possibles entre deux SFP (le NFSFP du calcul et celui de l'endroit que l'on examine) pour mieux comprendre les différents cas.

Définition

destin dans le cas d'un calcul élémentaire

Soit c un calcul élémentaire sur une formule x, soit s une SFP de x.

Le destin de s dans le calcul c sur x est :

  • ignored : ssi s est disjoint du NFSFP du calcul élémentaire. Donc sa trace reste s (par exemple x pour par le calcul loose $L[1b] de x if 0b y z). Remarquons que ce destin est impossible dans un calcul univocal.
  • calculated : ssi on a la disjonction :
    • le calcul porte sur toute ou une sous-partie de s, c'est à dire que le NFSFP du calcul élémentaire est intérieur à s. Donc la sous-formule en s change (probablement) de contenu mais sa trace reste s.
    • s est une fonction de la sous-formule désignée par le calcul élémentaire et la trace de s a un enfant. Par exemple pour le calcul univocal de if 1b x y z t où s est l'endroit de la formule if 1b x y z (s = $L[0b]).
  • argument/n ( pour n∈ℕ ) : ssi s est dans un argument — ou l'argument entier — de la sous-formule désignée par le calcul élémentaire et si la trace de s a n enfants (0,1 ou 2 pour lazi.0.0). Par exemple pour le calcul univocal de if 1b x y z t, s peut désigner 1b, x, y,z ou t et le destin est alors respectivement argument/0 , argument/1, argument/0, argument/1, argument/1.
  • function : ssi s est une fonction de la sous-formule désignée par le calcul élémentaire et si la trace de s n'a pas d'enfant. Par exemple pour le calcul univocal de if 1b x y z t, le destin de if 1b x est function.

destin dans le cas d'un calcul non élémentaire

Soit c un calcul non élémentaire sur x et s un SFP sur un résultat intermédiaire au niveau n du calcul. Le destin de s dans le calcul c à l'étape n sur x est le destin de s dans le n-ième calcul élémentaire de c sur x.