Redéfinition de =c

Contexte

Dans l'essai 3 de "Récurrence pour commutativité", on voit que l'on a un problème avec la définition actuelle de =c. D'autre part la définition actuelle est Lazi.1 (elle utilise ∃ et ∨) ce qui complique les choses. Il me semble qu'il serait mieux d'avoir une définition Lazi.0 qui de plus reflète exactement les égalités démontrables par les preuves Lazi.0.

Question

Est-il possible et pratique de définir =c de sorte que:

• la définition soit en Lazi.0
• on ait l'équivalence entre x =c y et il existe une preuve Lazi.0 de x *=* y
• la définition ait un intérêt, c'est à dire qu'elle soit plus simple à calculer que de parcourir toutes les preuves Lazi.0

On cherche une définition de =c qui retourne 1b quand on détecte une égalit, mais on ne cherche pas à détecte une inégalité et donc à retourner 0b.

Étude

Essai 1

On multiplexe les différentes voies explorées, on sait que c'est possible à faire, on verra plus tard de quelle manière.

Si x et y sont calculables

Une des voies explorée est le calcul de x et y, si le calcul s'arrête des deux côté, soit xc et yc les 2 calculs:

• Si l'un est un mot et pas l'autre: on retourne 0b.
• Si les deux sont des mots: on retourne leur comparaison syntaxique.
• Si les deux sont des applications xc1 +f xc2 et yc1 +f yc2: on retourne le résultat du calcul de xc1 =c yc1 ∧b xc2 = yc2.

Si x ou y n'est pas calculable

Il faut envisager en parallèle que le calcul ne s'arrête pas pour x ou y.
Si le calcul d'une formule ne s'arrête pas alors c'est toujours une application.
Si x ou y s'arrête, alors il ne peut y avoir égalité que si l'autre s'arrête.

Bestiaire 1: x et y se calcul différemment au début puis aboutissent à un calcul en boucle tous les 2, mais le calcul est décalé l'un par rapport à l'autre.

Réponse

@todo