Lazi

É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

Recherche d'une preuve

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.