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 xk *=* xk+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 ?
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 ?
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 :
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 ?
$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