Lazi

Interactions entre les formules lazi et les instructions

Contexte

Pour représenter un langage informatique basé sur lazi il faut utiliser la notion d'instructions, mais celles-ci utilisent des formules lazi. Il faut donc représenter les interactios entre lazi et les instructions.

Question

Comment représenter les interactions entre lazi et les instructions ?

Étude

Les instructions intégrables dans les formules ?

L'intérêt d'intégrer les instructions directement dans les formules (plutôt que d'utiliser des représentations) est que l'on peut utiliser directement des formules lazi dans les arguments des instructions et pour les instructions retournant une valeur on peut directement les voir comme des valeurs. Ce serait donc agréable et simple d'étendre les formules lazi aux instructions.

Les instructions qui ne retournent pas de valeur peuvent peut-être être vues comme des formules. Mais comme la valeur retournée est dépendantes de facteurs externent, si on n'utilise pas de dispositif particulier alors on obtiendrait des contradictions car on pourrait déduire "instruction = 1b" et "instruction = 0b".
On peut utiliser divers dispositifs pour éviter cela, comme :

  • L'instruction retourne une valeur fixe : dans ce cas il est inutile de l'éxécuter. Elle peut retourner l'ensemble des valeurs possibles. Cela peut servir par exemple à étudiers tous les états possibles lors de l'éxécution d'un programme. Mais il faut tenir compte aussi que voir la valeur retournée par une instruction à
  • On réduit les règles de déductions pour les instructions pour ne pas pouvoir aboutir à une contradiction. Donc cela revient à dire que l'instruction n'est pas réellement une formule lazi.
  • On ajoute un argument "temps" qui fait que l'éxécution de chaque instruction est spéciale, mais alors comment ajouter cet argument ?
  • Du point de vue mathmatique, considérer les instructions commes des entités non remplacées.

Par réduction des règles ?

Si i est une instruction, on ne peut déduire i = i, toute formule contenant une instruction serait "contaminée".

Peut être que : Ce n'est pas très gênant car les formules contenant des instructions sont petites car en lazi les instructions sont des représentations, par exemple une fonction contenant de instruction est une fonction lazi normale, mais retournant une représentation.

Quelles seraient les règles à enlever pour les instructions ?
Suffit-il de garder un lien quand on calcul un distribute ?

Par l'ajout d'un timestamp ?

Pour que cela ait un sens il faut que l'argument rendant chaque instruction unique soit là dès le début. Si on avait un argument "getTime" qui soit aussi une instruction, ça ne ferait que déplacer le problème. Donc ce n'est pas un timeStamp mais un marquage d'unicité. Ce marquage peut éventuellement suivre l'ordre d'éxécution des instructions, mais ce n'est pas souvent possible. Mais il faudrait que l'instruction ne soit éxécuter qu'une fois ou que la duplication change l'argument de marquage. Cela me parait trop tordu.

Par des valeurs retournées fixes ?

Ce cas ne répond pas au besoin d'exécution des instructions. Reste à savoir si c'est utile pour déterminer les états possibles. Le problème est que les valeurs retournées peuvent devoir vérifier des constraintes entres elles. Par exemple on peut imaginer une instruction qui retourne au valeur quelconque la première fois puis l'incrémentation de la valeur précédente. Donc d'un côté il faudrait représenter ces constraintes et de l'autre il faut retourner strictement la même chose à chaque calcul d'une instruction (on y incorpore ses arguments). Cela est incompatible. Donc même les valeurs fixes ne sont pas une bonne solution.

Les instructions commes des entités non remplacées

Du point de vue mathématique on ne voit pas les remplacements. Donc il n'y a pas d'incohérence. Pour les instructions ayant leur valeur de retour inutilisées on peut utiliser le mot clé "InstructionPair i j" qui représente l'éxécution de x puis celle de y. Ainsi on peut représenter des listes non vides d'instructions.

Si une formule lazi sert à produire des instructions, alors on peut calculer la formule avec les règles habituelles, on doit donc arriver sur une instruction ou sur "instructionPair" (que l'on peut voir comme une instruction). On peut alors calculer récursivement les arguments et sous-arguments des instructions car les instructions utilisent et retournent des données. Une fois fait, si le programme est statique — dans le sens où le résultat d'une instruction ne sert pas à déterminer la suite des instructions — alors le programme peut être compilé. Sinon il doit avoir des parties interprétées.

Reste à savoir comment voir les instructions du point de vue de la spécification des propriétés sur le code. Il faut spécifier d'une manière ou d'une autre les propriétés sur les arguments et l'éventuelle valeur retournée. Il faut prendre en compte la séquence entre les instructions : par exemple si une instruction getTime retourne une certaine valeur, on peut vouloir spécifier que la fois suivante la valeur de getTime sera ≥ à la valeur précédente.

@todo

Intégrer les formules dans les instructions ?

Pour interpréter une instruction (mélangée à des formules lazi) on peut ajouter au calcul habituel des règles pour éxécuter les instructions.

Pour une mathématique lazi M de type de forumes F, soit I le type des formules où l'on ajoute des instructions.

Ainsi pour une formule I (qui n'a pas de mathématique associée, voir pourquoi plus haut), on peut calculer sa valeur ce qui peut impliquer l'éxécution des instructions incluses.

Mais avec ce système on ne résoud pas la question de l'éxécution des instruction sans valeur de retour. De plus il est intéressant de distinguer les suites d'instructions qui sont constantes car alors on peut coder l'exécution en dur plutôt que d'interpréter du code lazi pour calculer les instructions à éxécuter.

Donc intégrer les formules dans les instructions peut être interessant comme manière de formuler mais n'est pas utile comme modèle global.

Fournir une liste d'instructions optionnellement dynamique

On entend par dynamique le fait que la suite de la liste peut dépendre des valeurs retournées par les instructions précédentes.

Un programme p est un Maybe $T[i,arg,f] où, si il n'est pas vide alors i est la première instruction à exécuter et si x est le résultat de l'instruction i alors si arg=0b f est la suite du programme et si arg=1b alors f x est la suite du programme.

Remarquons qu'avec ce système on peut compiler en dur le début de liste tant que l'argument pour déterminer la suite du programme n'est pas utilisé. Si on veut intégrer un détermination dynamique des instructions (c'est à dire dépendant d'une valeur retournée précédante) suivie d'une statique, il faut alors que la partie dynamique ainsi que l'instruction retournant la valeur soit encaptulée dans une instruction. On a donc un système souple qui à la fois supporte la compilation en dur, l'interprétation et un mix des deux.

On peut ajouter n'importe quelle forme d'abstraction, par exemple celle consistant à intégrer des formules dans les instructions (voir ci-dessus), il suffit pour cela d'ajouter un nouveau type d'instruction.

Les instructions et les fonctions

A-t-on besoin de créer un nouveau type de fonction quand une fonction contient des instructions ?
Non, on peut voir la fonction comme une fonction normale qui retourne des instructions.

Les instructions et les variables locales

Comment traduire : Let a = read STDIN; print a;

Réponse

@todo