Lazi

Langage de programmation et mathématique

Contexte

Pour produire un compilateur il faut déjà définir une représentation de ce qu'est un langage de programmation. Ici nous voulons une représentation mathématique.

Question

Comment représenter mathématiquement un langage de programmation ?

Étude

Résumé

Nous allons d'abord montrer comment représenter un programme comportant des entrées/sorties par une déduction de calcul.
Puis nous montrerons comment un langage de programmation peut être représenté par un type de déduction de calcul.
Puis nous exposerons des extensions mathématiques permetant de rendre ce langage pratique et puissant.

Un programme sans effet de bord est une déduction de calcul

Comme il n'y a pas d'effet de bord, il s'agit de calculer une formule f pour aboutir à un résultat r. Hors une déduction de calcul prend en argument une formule p et a pour objet une vérité "p = r". On voit donc que l'on peut représenter un langage informatique sans effet de bord par un type de déduction de calcul.

Si p est un calcul infini, on peut quand même représenter son calcul, pour cela on peut définir une déduction de calcul qui prend en argumet supplémentaire le nombre de déduction maximal à produire.

Représenter les effets de bord

Pour représenter les effets de bord nous allons ajouter un paramètre u qui représentera l'univers du programme. Par exemple si le programme n'a que des effets sur l'affichage alors u pourra ne comporter qu'une représentation de l'affichage. En pratique on ne cherchera pas forcément à calculer une version pleine de u, par exemple si le programme prend des photos de galaxies on ne pourrait évidemment pas calculer notre univers. L'important est d'avoir une représentation mathématique d'un programme, dans certains cas on pourra calculer son univers explicitement, dans d'autres juste déduire des propriétés.

Avec les effets de bord un programme est représenté par un calcul d'une formule p u1 où le résultat est de la forme "p u1 = $T[u2,r]" où u2 est l'univers à la fin du calcul et r le résultat proprement dit du programme.

Gestion du calcul asynchrone de l'univers par p

p n'a besoin de calculer l'univers que lors des entrées/sorties. L'univers peut changer en fonction du temps passé à calculer p entre deux entrées/sorties. Illustrons cela par un exemple : un programme p1 boucle en exécutant :

  1. demander l'heure
  2. calcule factoriel de \ l'heure (en secondes) modulo 100.
  3. afficher le résultat du calcul

On voit que l'univers u qui doit être calculé à chaque lecture de l'heure dépend du temps de calcul du factoriel et donc de l'heure lue précédemment.

Montrons que l'on peut toujours calculer ce temps : pour cela u contient une représentation de p1 ainsi que de l'état d'avancement du calcul. On peut alors calculer le temps passé dans l'univers losque que le calcul de p1 passe entre les deux dernières entrées/sortie puisque toutes les informations du processus sont représentées dans u.

Applications réelles ou virtuelles

Pour calculer p u en pratique, on peut le faire en utilisant — en partie ou totalement — notre univers physique dans le rôle de u. On peut donc dans certain cas utiliser un univers calculé informatiquement ou encore calculer p sur une machine physique où les fonctions d'entrées sorties utiliseront des entrées/sorties réelles.

Langage de programmation en tant que type de déduction de calcul

Pour notre représentation, un langage de programmation est équivalent à un type de déduction de calcul (i.e. une règle de calcul). L'argument de la règle de calcul "source" sera le code source du programme. Il pourra inclure l'expression des types (et plus généralement des propriétés sur le source), ce sera des contraintes supplémentaires qui devront être vérifiées pour que la déduction soit valide.

Les extensions mathématiques

Les déductions de base lazi sont loin d'offrir un langage de programmation aisé (pas de définition, pas de fonction etc). Nous allons définir toute une série d'extension qui rendra au final le langage pratique.

Soit L1 un type de déduction d'une mathématique M1 définissant un langage informatique. Si on étend M1 à M2 par une extention du type des formules, alors on peut remarque que L1 est encore un langage informatique dans M2 si L1 accepte toute formule en argument. Mais pour cela il faut que L1 sache calculer les nouveaux types de formule.

Type de déduction de calcul simple

Il nous faut d'abord éfinire une déduction de calcule, car pour l'instant nous n'en avons pas. C'est à dire qu'il nous faudra générer une preuve f = x à partir d'une formule f.
Pour cela il suffit de calculer f tout en écrivant la preuve correspondante. Par exemple si f est "if 1b 0b 1b" alors on utilise la déduction "if sur 1b" pour déduire "if 1b 0b 1b = 0b".

Extension pour ajouter les définitions

On ajoute une extension pour pouvoir définir des noms globaux (et donc utiliser des "$Def ..."). 07-definition.ext-ev.lazi.

Extension pour ajouter les fonctions

Cela permet la nation $F ... , voir 06-function.ext-nota.lazi

D'autres extensions pour ajouter des notations

Comme :

  • la représentation des mots (voir 08-wordRepr.ext-nota.lazi)
  • utiliser des définitions comportant des boucles récursives (définir x en fonction de y et y en fonction de x)

Extension pour utiliser des variables globales'

On a vue que le calcul du programme inclut l'argument "u" de l'univers. On a alors besoin pour écrire un programme ayant des effets de bords (c'est à dire modifiant "u") à devoir passer u en argument un peu partout dans le programme. On sait déjà que ce genre de code source où il y a une double valeur à retourner (ici "u" et le résultat proproment dit du programme) est pénible.

Il semble alors intéressant de définir une extension pour alléger la production de code source à effet de bord. Pour cela on cherchera à ne plus avoir à gérer le passage de u et à utiliser une "variable globale" que l'on peut lire et écrire.
Voir l'étude sur cette extention.

Réponse

@todo