Lazi

Compilateur basé sur Lazi

Contexte

La base de lazi est un langage fonctionnel pure sans entrée/sortie.

Question

Comment produire des logiciels en utilisant lazi ?

Étude 3

Pourquoi mathématiser

Les structures des logiciels sont de complexité illimitée. En limitant la syntaxe ou la sémantique d'un système de spécification de logiciels on se heurte forcément à des gênes inutiles. Pour ne pas se limiter il est nécessaire que le système de spécification ait la possibilité d'intégrer toute sortes d'extensions.
Concrètement les compilateurs/interpréteurs actuels ont pour la plupart leur validité d'assurer par des moyens externes (pour la plupart par une relecture du code et la passage de testes). Si l'on veut permettre toute sorte d'évolution il est nécessaire d'assurer l'intégrité par des preuves de propriétés mathématiques. Il est aussi nécessaire que le compilateur/interpréteur soit modulaire de manière à facilité les extensions.

Comment mathématiser

Nous allons montrer qu'un programme, effets de bord inclus, se représente comme une preuve. Nous allons étudier trois composantes du compilateur :

  • le langage de programmation moins le système de typage
  • le système de typage
  • la production du programme effectif (librairies, code exécutable, système d'extensions du compilateur etc).

Étude 2 (abandonnée)

Étude abandonnée car passage à la vision d'un programme comme d'une preuve.

Mathématiser

Les structures des logiciels sont de complexité illimitée. En limitant la syntaxe ou la sémantique d'un système de spécification de logiciels on se heurte forcément à des gênes inutiles. Pour ne pas se limiter il est nécessaire que le système de spécification ait la possibilité d'intégrer toute sortes d'extensions.
Concrètement les compilateurs/interpréteurs actuels ont pour la plupart leur validité d'assurer par des moyens externes (pour la plupart par une relecture du code et la passage de testes). Si l'on veut permettre toute sorte d'évolution il est nécessaire d'assurer l'intégrité par des preuves de propriétés mathématiques. Il est aussi nécessaire que le compilateur/interpréteur soit modulaire de manière à facilité les extensions.

Modèle mathématique de l'exécution d'un programme

On représente l'exécution d'un programmes par trois entités :

  • p : le programme
  • u : l'univers, c'est ce à quoi à accès le programme par l'intermédiaire des entrées / sorties
  • c : la fonction de calcul, elle prend p et u en argument et exécute le calcul du programme p et de l'univers u

Il est clair que suivant le choix de u on ne peut pas calculer pratiquement c p u (par exemple si on inclue un humain dans u). Mais il s'agit ici d'un modèle théorique. Une bonne partie du travail qui va suivre consistera à simplifier c et u. Par exemple on pourra réduire les humains à des réponses prédéfinies, ou encore à un générateur aléatoire (c'est à dire que l'on étudiera les états superposés des entrées possibles).
De ces simplifications naîtra une représentation des programmes qui sera assez simple pour être intégrée dans le langage lazi.

Nous allons donc décrire maintenant une série de simplifications qui seront adoptées.

Simplification par autocentrisme

Comme on ne s'intéresse qu'au programme et à ses interactions avec l'univers, c peut découper le calcul ainsi :

  • Il exécute le calcul du programme sans calculer u tant qu'il n'y a pas d'entrée sortie.
  • Quand il y a une entrée sortie il calcul u jusqu'au point nécessaire à l'exécution de l'entrée sortie, puis il calcul sur u les conséquences de cette entrée sortie.

Exemple : p est le programme qui lit l'heure et affiche le résultat, puis exécute une boucle vide finie et recommence au début. u est le calcul de l'horloge lue par p. Sans autocentrisme c pourrait calculer en parallèle u et p pour qu'ils soient dans le même temps, ainsi quand p lit l'heure il suffit de lire l'heure dans l'horloge de u. Dans le modèle autocentré p est seul calculé jusqu'à l'instruction de lecture de l'heure, alors u est calculé jusqu'au moment correspondant à l'exécution de l'instruction de lecture de l'heure.

On remarquera de l'exemple précédent une difficulté de l'autocentrisme : c'est la resynchronisation des calculs puisqu'ils ne sont plus naturellement effectués en parallèle. Pour cela il faut utiliser les informations de temps de calcul de p et u et ainsi calculer u jusqu'au bon moment. On peut remarquer que, comme le calcul est autocentré il n'y a pas d'effet de bord, et donc la séquence des entrées/sorties est fixe. On peut donc utiliser une version u2 de l'univers u pour calculer les informations de temps de calcul de p entre les différentes entrées/sorties. Remarquons que ces informations sont forcément calculables puisque nous sommes dans un calcul.

Simplification par intégration du calcul de u dans p

Comme l'autocentrisme permet de ne calculer u qu'au moment des instructions d'entrées/sorties, il devient possible de faire calculer u par p. Dans ce modèle le calcul c p u se réalise par un calcul c2 (p2 u) où c2 calcul un programme seul et p2 est l'équivalent de p mais avec l'intégration du calcul de u. L'avantage de cette simplification est que l'on retourne à un calcule pure (sans effet de bord).

Remarquons que la transformation de p en p2 est automatique :

  • Il faut ajouter l'argument u dans toutes les fonctions utilisant des entrées et il faut que toute fonction d'entrée/sortie retourne le u actualisé. Par exemple

t = getTime;
print t;
devient
$T[new_u, t] = getTime u;
new_new_u = print new_u t;

  • Comme dans la simplification précédente on utilise une version modifiée de u pour connaître les temps de calculs entre les entrées/sorties.

Simplification par l'utilisation d'événements

Les événements est une extension mathématique de lazi fournissant un cadre à la "modification" de la mathématique.
Cela nous permetra ici de ne pas avoir à écrire des programmes où l'on doit partout s'occuper de transmettre u en argument et en valeur retournée. Pour cela les événements nous permettent de stocker une variable globale "univers".
Mais en ajoutant des événements au code on ajoute des déductions alors qu'auparavent il n'était constitué que de formules (les définitions sont en soit aussi des événements mais comme elles peuvent être toutes traités avant le calcul, on n'a pas à les mêler à l'exécution).
On ne peut donc plus voir le code comme la définition d'une formule à calculer. Une formule que l'on calcule est une manière de produire automatiquement une preuve d'une égalité. Un événement étant une déduction, il nous faut voir le programme comme représentation permetant de produire une preuve (qui aboutit encore à une égalité puisque le programme avec événements est équivalent à un programme sans).

Comment alors formuler le programme ?

Prenons l'exemple suivant : un programme qui demande un nombre, calcul son factoriel, puis retourne le résultat :
n := readInteger;
print ( fact n);

Dans ce programme nous avons des fonctions qui font appelle à des événements (puisqu'elles utilisent des entrées sorties).

Étude 1 (abandonnée)

Mathématiser

Utiliser le langage mathématique permet de spécifier les propriétés sans limite d'expressivité et de vérifier ces propriétés par des preuves. Cela permet par exemple d'ajouter rapidement des extensions car toutes les vérifications sont faites automatiquement.

Mathématiser le compilateur consiste à utiliser un compilateur qui possède un modèle mathématique de lui-même. Cela permet de le modifier tout en vérifiant sa validité. Il n'y a donc plus de limite dans la souplesse de la programmation.

Le modèle mathématique

Il ne faut pas limiter le compilateur, pour cela on doit partir d'un modèle large : il s'agit de produire un ensemble de fichiers (on peut avoir par exemple à produire des librairies). Puis on utilise différentes représentations comme :

  • celle des fichiers exécutables (par exemple ELF).
  • celle de l'exécution de code

Représenter l'exécution de code au bas niveau

On peut représenter une machine par une fonction f et son état par un argument e. f e est la liste des états de la machine.

Représenter les sorties

On peut représenter les sorties par juste une instruction sans effet, ou bien on peut agrandir la représentation de la machine en incluant le périphérique de sortie (par exemple l'image de l'écran). Dans ce dernier cas une sortie aura un effet sur l'état du périphérique.

Représenter les entrées de données

Une entrée n'est pas un état mais une superposition d'états. Donc il faut intégrer cette notion dans le calcul des machines. On peut avoir des représentations pour les plages de valeurs, par exemple on peut représenter "tous les états superposés entre 0 et 100" quand l'entrée est un entier entre 0 et 100. En utilisant des représentations adaptées on n'a pas d'explosion de la taille du calcul.

Remarquons que certaines entrées sont en rapport avec le temps, comme l'horloge. Ce sont des entrées ordinaires, et comme les autres il faut représenter les contraintes spécifiques.

Une entrée peut être représentée comme une fonction Lazi, simplement la valeur de sortie ne sera une superposition d'états. Mais il faudrait préciser ce qu'est le type "superposition d'état".

Représenter les entrées d'interruption

Une entrée d'interruption ne se produit pas en résultat d'une instruction d'entrée. On peut donc la concevoir comme une superposition d'états dont l'un des états est "pas d'interruption". Il faut donc pour chaque étape du calcul des états vérifier s'il y a eu une interruption. On voit donc que l'on est ogliger d'adopter des représentations particulières pour éviter de faire exploser la taille du calcul.

Les instructions et les formules

Voir l'étude sur les interactions entre les formules lazi et les instructions.

Représenter l'exécution de code à des niveaux intermédiaires

Remarquons qu'un OS peut être vu comme un système de virtualisation car il offre au logiciel une représentation plus simple de l'ordinateur. On peut donc utiliser cette représentation.

Représentation du code à haut niveau

Les données globales non constantes

On étudie le cas ici des données uniquement changer par le programme, pour le reste (comme de la mémoire d'échange) on peut le considérer comme un périphérique.

Étude d'un exemple

On prend l'exemple d'un programme qui demande un nombre entier n entre 1 et 1000 et qui boucle en retournant n×0,n×1,n×2,n×3,...,n×10.

n est une supperposition d'état entre 1 et 1000.

Réponse