Lazi

x→c[l]... y (notations de calcul)

Contexte

Nous avons défini la fonction "calculate". À partir de cette fonction nous allons définir une notation signifiant "il existe un calcul qui calcul x en y suivant le langage de calcul l". Suivant une option, ce sera un calcul élémentaire ou non.

Définition

Pour x et y deux formules et a un langage de calcul, x →c[a] y :

  • signifie : il existe un calcul c en a tq calculate a c x = y et c est de longueur ≥ 1
  • se lit : x se a-calcule en y ou encore y est une étape du a-calcul de x.

On peut ajouter des lettres après le "]" pour préciser des propriétés :

  • 1 : c est de longeur 1, se lit : x se 1-a-calcule en y.
  • = : la condition "c est de longueur ≥ 1" est enlevée, se lit x se égal-a-calcule en y.
  • t : y est un calcul terminé, se lit x se a-calcule complètement en y

Par exemple : x →c[a]=t y signifie qu'il existe un calcul c en a tq calculate a c x = y et le calcul de y est terminé, et se lit : x se égal-a-calcule complètement en y.