Lazi

Type des instructions

Contexte

Il semble qu'un moyen simple pour ajouter des instructions à effet de bord soit la manière la plus basique possible (voir Interactions entre les formules lazi et les instructions / Les instructions commes des entités non remplacées). Mais alors se pose la question de la spécification des propriétés (les types) pour les instructions.

Question

Comment spécifier les propriétés sur les instructions ?

Étude

Par un timestamp ?

L'idée est d'ajouter un paramètre pour rendre chaque instruction unique. Cela correspond à la réalité car chaque instruction est unique dans son exécution. De plus ce paramètre, s'il comprend un entier, permet de représenter l'ordre d'éxécution.

Qu'en est-il des boucles ? Par exemple pour une boucle "for" :

  • soit elle est faite en instruction et donc c'est une instruction "for" qui prend en argument l'instruction à répéter.
  • soit elle est faite en lazi, fixe ou dynamique.

Comment inclure le timestamp quand il y a une bifurcation (un if) ? On devrait pouvoir réutiliser les mêmes valeurs mais le problème est que l'on pourrait avoir des doublons. On pourrait utiliser aussi, plutôt qu'un seul integer, un chemin binaire pour distinguer les bifurcations.

Il me semble qu'il n'y a pas de blocague théorique à ajouter un timestamp. Supposons maintenant qu'il n'y ait pas de blocage et voyons comment alors spécifier les types.

Remarquons que même avec un timestamp, une instruction ne retournant pas de valeur peut-elle être vue comme une fonction ? On peut introduire une pseudo valeur "void".

Il est important de distinguer ce qui a un effet de bord. Si on ajoute automatiquement le timestamp, comment distinguer une fonction sans effet de bord d'une fonction utilisant getTime ? Peut-être en ne rendant pas transparent le timestamp, qui serait un argument des fonctions à effet de bord. Il faudrait obligatoirement cet argument, donc la valeur ne pourrait être créée, mais peut-être pourrait-elle (et/ou devrait-elle) être incrémentée ? Ce timeStamp pourrait plutôt être la représentation de l'état de la machine, il pourrait comprendre plus d'information. Il serait donc passé en argument à toutes les fonctions faisant appel directement ou indirectement à une instruction. Il faudrait étudier s'il est possible que le passage de cet arguent soit transparent.

Réponse

@todo