Lazi

calcul passant par

Contexte

Le calcul de x passe par y signifie que pour calculer x il est nécessaire de calculer y. C'est donc une notion fondamentale pour le calcul des formules. La définition est calquée sur les règles de calcul.

Définition

Soit a, b deux formules. Le calcul de a passe par b ssi on a la disjonction suivante :

  • si a est de la forme $F[ if 1b ] +f x +f y : b = x ou le calcul de x passe par b
  • si a est de la forme $F[ if 0b ] +f x +f y : b = y ou le calcul de y passe par b
  • si a est de la forme $F[distribute] +f x +f y +f z : b = (x +f z) +f (y +f z) ou le calcul de (x +f z) +f (y +f z) passe par b.
  • si a est de la forme $F[if] +f x +f y +f z où x →c1 t : b = x ou le calcul de $F[if] +f t +f y +f z passe par b.
  • si a est de la forme x +f y où x →c1 z : b = z ou le calcul de z +f y passe par b.