Traduction des égalités
Contexte
Pour mesurer les coûts des calculs (voir comment définir un interpréteur) il est pratique de se baser sur le nombre de déductions de la preuve de l'égalité, mais pour cela on a besoin d'une mesure commune. Ce qui me semble logique est de traduire la preuve de l'égalité en M en preuve en lazi.0.0.
Question
Est-ce que toute déduction dans une mathématique M d'une égalité x *=* y peut se traduire en une déduction lazi.1.0 où l'on a étendu le type de formule mais sans étendre les déductions.
Étude
Si M ajoute un mots a et une déduction prouvant a *=* $F[1b] ?
Donc il faudrait changer le théorème en :
En plus d'être complexe, le coût de la preuve peut être beaucoup plus grand que le coût du calcul. Donc ce n'est pas une bonne idée de mesurer le coût par la preuve.
Réponse
Ce n'est pas une bonne idée de mesurer le coût par la preuve.