Lazi

fonction constante par calcul

Contexte

On veut définir, par calcul, ce qu'est une fonction constante. Pour vérifier si f est une fonction constante, on calcul f +f x, où x est un mot qui n'est pas dans le langage de f, jusqu'à ce que x ne se trouve plus dans la formule calculée.

Comme pour beaucoup de propriété du calcul, si f +f x est incalculable cette méthode n'assure par un résultat.

Définition

Pour f une formule, on dit que f est constante par calcul si pour un mot x n'apparaissant pas dans f il existe une formule g telle que f +f x →c g et où x n'apparaît pas dans g.