Comment définir un interpréteur

Contexte

Ce que l'on appelle un interpréteur est le processus qui prend en argument une 1-formule et retourne une 1-formule ou rien (si il n'y a rien à interpréter) dite "interprétée", par exemple le calcul élémentaire "univocal" est un interpréteur.

Question

Comment définir un interpréteur ?

Étude

Essai 3

Soit M1 une mathématique Lazi.

Essai 2

C'est une continuation de l'essai 1.

Problème de la généralisation de la liste

On pourrait vouloir s'adapter à toute forme de liste de manière à ne pas nous limiter à une forme de liste et donc pour éviter de ne pas prendre en compte tout un ensemble de calculs.

Mais si on se limite à une seule sorte de liste, comme les formats de liste n'ont pas d'importance dans le calcul et sont en proportions indépendantes du contenu, on ne change pas les proportions des différents calculs en nous limitant une seule forme de liste.
C'est la même chose pour le format "extension de formule", car c'est une encapsulation indépendante du contenu.

Donc on peut limiter les calculs aux liste de formules.

La limitation évite le problème de reconnaissance d'un format liste quelconque, et aussi d'une donnée quelconque. Ce problème ne me semble pas simple car il faut que les fonctions qui permettent d'accéder aux éléments de la liste ne fasse pas elles-même du calcul. On pourrait augmenter les formats de listes reconnues en forçant par exemple la fonction d'extraction de l'élément être une fonction qui applique une liste de binnaires en tant qu'argumentS sur le calcul. Mais ça ne ferait que de repousser le problème car il y a une infinité de liste qui peuvent avoir d'autres formats (certes tordus mais très nombreux. On peut même imaginer un format variable dépendant de l'élément précédent.

Définition d'un calcul

Soit M une mathématique lazi et n un entier naturel ≥ 2. On dit qu'une chose c est un calcul ssi on a la conjonction suivante :

c est une liste inversée potentiellement infinie d'au moins n éléments.
Soit x1,...,xn ces n éléments, alors on a la conjonction :
- x1,...,xn sont des formules de M
- il existe n-1 déduction de calcul de M d1,...,dn-1 tq pour 1 ≤ k ≤ n-1 dk a pour conclusion x_k *=* x_k+1

Comment calculer le coût d'un calcul

Si c est un calcul,

Essai 1

Un interpréteur peut avoir besoin de contexte, par exemple pour un système de calcul qui utilise des références pour unifier le calculs de sous-formules identiques.
Un interpréteur peut devoir avancer par groupe de calculs plus élémentaires, par exemple si il réalise un calcul élémentaire pour chaque sous-formule.
Un interpréteur doit retourner une formule égale à celle en entrée.

On peut voir un interpréteur comme une déduction qui a en argument une formule et retourne une égalité. La déduction suivante se fait à partir du membre droit de l'égalité précédente.

Il faut utiliser une mathématique qui est une extension de lazi.1.0 dans le sens où l'on a pu ajouter des nouveaux types de déduction et de formule.

Comment mesurer la quantité de calcul engendrée par un calcul ?

Pour cela on peut utiliser la quantité de déduction lazi.0.0 nécessaire à ce calcul. Cela n'implique pas de traduire le calcul en preuve lazi.0.0. Théoriquement il me parait logique de devoir ajouter la preuve de la validité de la mathématique utilisée pour le calcul. Mais cette preuve ayant un coût fixe elle ne devrait pas entrer en compte dans les raisonnements basés sur la densité des choses.

Avec une telle définition on ne limite pas le degré d'abstraction utilisé dans les calculs.

Avec cette définition du calcul, peut-on voir notre univers comme un calcul ?

On suppose que le calcul de notre univers peut s'exprimer par le calcul d'une fonction f. On définit une extension des formules qui permet de représenter les différentes étapes du calcul de f. Donc les traductions de ces représentations seront égales à f aux différentes étapes du calcul de f donc à f.

Problème et étude

Avec ce système les calculs sont finis. Est-ce utile de définir les calculs infinis ? Oui.

Donc il faut garder le principe d'utiliser une mathématique quelconque, mais sans pour autant qu'un calcul soit confondu avec une certaine sorte de preuve. La preuve sert aussi à mesurer le coût du calcul par le nombre de déductions utilisées. Ainsi on peut évaluer le coût du calcul suivant les différentes mathématiques, et au final suivant lazi.1.0 (ou lazi.0.0 ?). Comme les preuves se font sur des formules, cela résoud la question de l'effectivité.

On peut définir une liste infinie comme une structure $T[ element, reste de la liste ].

Pour n ≥ 2, c est un calcul de mathématique M et de longueur n ssi :

Soit x₁,...,x_n les n premiers éléments de la liste, alors il existe d₁,...,d_n-1 des déductions de calcul de M tq d_k déduise x_k=x_k+1.

c est un calcul infini de mathématique M ssi pour tout n ≥ 2 c est un calcul de mathématique M et de longueur n.

Comment mesurer le coût du calcul c ? Si on pouvait toujours traduire une preuve déduisant xk *=* xk+1 en preuve lazi.0.0 alors il suffirait de mesurer la longeur de la preuve traduite. Ce n'est pas une bonne solution (voir le lien).
On peut mesurer le coût du calcul de n élément simplement en calculant combien il faut de calculs élémentaires pour calculer les n éléments. Comme les éléments de la liste sont au final des données, on peut calculer toutes les parties par un interpréteur qui calcul l'élément entier puis chaque argument. Remarquons que la fonction qui définit le calcul peut être sophistiquée et par exemple définir des abstractions pour réaliser le calcul de manière optimisé, elle peut par exemple elle même définir un autre formalisme et une autre manière de calculer.

L'extension du type formule permet de supporter toute sortes de représentation de données. Mais est-ce que le fait que ce soit une extension impose une limite gênante ?

Chaque élément d'un calcul doit être une donnée, cela impose que le calcul de toutes les sous-formules doit être fini. Le fait que ces données doivent être d'un type qui est une extension du type formule impose des contraintes. Mais on a déjà des contraintes sur le format de la liste. Peut-on se passer de ces contraintes ? On pourrait imaginer une fonction de traduction qui serait à temps constant par élément : un temps constant pour extraire l'élément suivant (ou trouver qu'il n'y en a pas), et un temps constant pour traduire en une donnée compatible avec une chose de type extension de formule). Il faudrait donc une fonction de traduction tr qui prend en argument la formule représentant le calcule et qui retourne soit nothing (s'il n'y a plus d'élément), soit un couple
$T[suite de la liste, chose compabible avec une extension du type formule]

Réponse

On définit un interpréteur comme une déduction d'une mathématique.

@todo