Égalité par calcul et sous-formules incalculables
Contexte
La notion d'égalité par calcul, du point de vue informatique, correspond à des fonctions (pures) identiques où l'on peut considérer comme égale les différentes boucles infinies. C'est ce que nous démontrons ici.
Nous utiliserons ce résultat pour la démonstration du théorème "Toute vérité se calcule en une égalité".
Énoncé
Définition
Soit va une formule.
Pour x une formule, T x est définie par :
Variables
x,y,va,xv,yv,T
Conditions
- x et y sont des formules.
- va est une formule qui est une variable de nom inutilisée dans x et y.
- T est une fonction définie par :
- Si z est incalculable, T z = va
- Si z est calculable, soit zc son calcul :
- Si zc n'est pas une application on retourne zc.
- Si zc est une application zc1 +f zc2, on retourne T zc1 +f T zc2
Conclusion
x =c y si et seulement si T x = T y
Étude
Preuve
Nous allons prouver le théorème par récurrence sur la profondeur maximale des formules x et y. (à corriger)
Pour une profondeur maximale de 1
Soit x et y des formules de profondeur maximale 1.
Si x =c y :
x et y sont des mots, donc calculables. Soit xc et yc le résultat de leur calcul respectif, on a xc = x et yc = y. Donc d'après la définition de =c on a xc = yc , donc x = y. Comme xv = x et yv = y on a xv = yv.
Si xv = yv :
Comme xv = x et yv = y on a x = y, donc on a x =c y.
Si le théorème est montré pour une profondeur n
Montrons qu'il est alors vrai pour une profondeur n+1.
Soit x et y des formules de profondeur maximale n.
Si x =c y :
Si x ou y n'est pas calculable alors x et y ne sont pas calculable et on a xv = yv.
Sinon x et y sont calculables. Si xc = yc alors par construction on a T x = T y. Sinon xc et yc sont des applications respectivement xc1 +f xc2 et yc1 +f yc2 où xc1 =c yc1 et xc2 =c yc2.
Sinon x et y sont calculables. Si xc = yc alors par construction on a T x = T y. Sinon xc et yc sont des applications respectivement xc1 +f xc2 et yc1 +f yc2 où xc1 =c yc1 et xc2 =c yc2.