Lazi

Calcul et remplacement

Contexte

Nous serons amenés à comparer les calcul d'une formule avec celle-ci où une partie est remplacée par une autre (voir le théorème "1 Mots clés:1.5 Théorèmes de calcul:Toute vérité se calcule en une égalité". Nous allons voir ici que lors d'un calcul une sous-partie ne peut subir que les traitements suivant:

  • duplication et déplacement (par la règle distribute)
  • calcul (argument de if ou position de fonction)
  • comparaison à 1b ou 0b (argument de if)

Ce qui fait que si on remplace une partie d'une formule par une formule de même calculabilité et, si elle est calculable, de même résultat de calcul, alors la calculabilité de la formule globale est inchangée.
Remarquons que la valeur syntaxique du résultat du calcul de la formule globale peut être changée: par exemple si dans equal (if 1b 0b 0b) on remplace if 1b 0b 0b par if 0b 0b 0b, le résultat final passe de equal (if 1b 0b 0b) à equal (if 0b 0b 0b).

Énoncé

Conditions

  • f est une formule lazi.0.0
  • x et y sont deux formules lazi.0.0 telles que x =c y

Conclusion

f +f x =c f +f y

Preuve

Calculons f +f x et f +f y.

Si f n'est pas calculable alors f +f x et f +f y ne sont pas calculables et on a donc par définition f +f x =c f +f y.

Si f est calculable, soit f2 le résultat du calcul de f. Le calcul de f +f x et f +f y revient à calculer f2 +f x et f2 +f y.

Si le calcul de f2 +f x ou f2 +f y est terminé alors les deux sont des calculs terminés et comme f2 =c f2 et x =c y, on a f +f x =c f +f y.

Si le calcul de f2 +f x n'est pas terminé, alors c'est aussi le cas de f2 +f y (voir les règles de →c1).

Si la règle 1 "if 1b" s'applique: alors x ou y est élminé, et donc le résultat est syntaxiquement identique, on a donc f +f x =c f +f y.

Si la règle 2 "if 0b" s'applique: on obtient x et y. Comme on a x =c y, on démontre facilement que f +f x =c f +f y.

Si la règle 4 "if x" s'applique: la règle continue à s'appliquer soit:

  • indéfiniment, et alors
f +f x et f +f y ne sont pas calculables, on a donc f +f x =c f +f y.
  • jusqu'à ce que la règle
"if 1b" ou "if 0b" puisse s'appliquer, et on a déjà traité ce cas
  • la condition du if est calculable mais n'aboutit ni à 0b ni à 1b, le calcul s'arrête avec des valeurs de la forme f3 +f x et f3 +f y. Comme f3 =c f3 et x =c y, on a
f +f x =c f +f y.

La règle 5 "calcul de la fonction" ne peut s'appliquer car f2 est un calcul terminé.

Si la règle 3 "distribute" s'applique: le résultat est de la forme (f2a +f x) +f (f2b +f x) et (f2a +f y) +f (f2b +f y).

Il faudrait élargir les conditions et que l'on ait des fonctions différentes égales par calcul.