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