Lazi

Problème de définition de l'égalité par calcul

Contexte

La définition actuelle de =c impose dans le cas de l'application, de calculer l'argument quand il est calculable. Mais on peut alors se trouver dans une boucle infinie. Par exemple:
Soit f et g tq f = if f et g = if \ if 1b g 0b. Si on veut tester if f =c if g :
On aboutit à calculer f et g et on obtient respectivement if f et if \ if 1b g 0b.
On aboutit à calculer f et if 1b g 0b et on obtient respectivement if f et if \ if 1b g 0b.

On voit que l'égalité par calcul n'est pas définit pour certaines valeur (comme l'exemple) puisque la récurrence dans la définition est sans fin.

Question

La définition de =c est-elle quand même celle dont on a besoin ? Sinon par quoi la remplacer ?

Étude

Besoin pour le théorème "Toute vérité se calcule en une égalité"

Il faut que l'égalité sémantique implique "=c". On a éliminé le calcul des sous-expressions incalculables. L'exemple donné ("if f") est entre les deux: on peut le calculer mais il contient quand même un calcul infini.

Pour les sous-expressions incalculables, on ne peut pas le vérifier juste en calculant, donc la définition de =c n'est déjà pas juste un calcul.
Avec le cas exposé dans le contexte, cela montre que =c peut être ni vrai ni faux. Mais comme on a besoin de raisonner que dans certains cas il me semble que ce n'est pas gênant pour ce que l'on a besoin.

Réponse

On peut continuer avec la définition actuelle d' =c .