Lazi

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] ?

Alors on ne peut pas prouver cette vérité en lazi.1.0. Mais il est possible de traduire "a" au préalable.

Donc il faudrait changer le théorème en :

Si M déduit x *=* y alors il existe x2 et y2 des formules lazi.1.0, deux preuves M de x *=* x2 et y *=* y2 et une preuve lazi.1.0 de x2 *=* y2.
Mais cela pose un problème pour la mesure du coût car les preuves de x *=* x2 et y *=* y2 pourraient cacher le coût de la preuve de x *=* y.

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.