Skel et les sémantiques squelettiques 

Télécharger le fichier pdf d’un mémoire de fin d’études

Machine abstraite

Pour éviter le problème d’avoir à reconstruire des termes, on peut utiliser une machine abs-traite. Une machine abstraite est une méthode d’évaluation où on sélectionne la partie du terme à évaluer, et on garde le contexte en mémoire pour plus tard. Ainsi, une configuration d’évaluation est généralement constituée d’un état, d’un terme à évaluer, et d’un contexte. On donne toutes les règles de la sémantique à machine abstraite de IMP en figure 1.7.

Langages de description de sémantiques

Le rôle de cette thèse est de présenter un langage de description de sémantiques, Skel, et l’écosystème Necro qui permet de le manipuler. Plusieurs langages de description de sémantiques existent déjà, et l’auteur de cette thèse ni son directeur de thèse n’ont l’hybris de prétendre que leur langage est meilleur ou mieux pensé. Nous expliquerons cependant pourquoi l’usage que nous envisageons d’un langage de spécification rend Skel et Necro plus pertinents que les précédents outils. Pour présenter les outils, nous utiliserons le λ-calcul en appel par valeur. IMP étant un langage assez gros, cet exemple est plus minimal et fonctionnel.

Attendus

Pour être utilisable et maintenable, on attend plusieurs choses d’un langage de spécification. Tout d’abord, le plus évident et le plus nécessaire, est qu’il doit permettre de spécifier une sémantique de manière lisible, compréhensible, et maintenable.
On attend également que le langage soit simple et ait une sémantique claire et bien définie. Enfin, on attend que le langage dispose d’un ensemble d’outils pour l’exécuter ou l’injecter dans des assistants de preuves. Il faut idéalement qu’il ait une interface suffisamment simple pour pouvoir facilement programmer d’autres outils.
Un bon langage de spécification peut cependant avoir une méta-sémantique configurable, de manière à pouvoir donner des sens différents à une même sémantique écrite dans ce langage. On attend alors que les différentes interprétations possibles soient clairement documentées.
Certains langages de spécifications proposent également une gestion de types natifs, ou une gestion native des lieurs pour simplifier l’écriture de sémantiques. Ces ajouts peuvent néanmoins complexifier la manipulation des sémantiques, et il faut donc choisir entre simplicité d’écriture et simplicité de manipulation.
Enfin, la possibilité de sous-spécification est utile, car elle permet de décrire une sémantique de manière incrémentale, et elle permet de laisser certaines décisions libres suivant les choix d’implémentation.

Skel et Necro

D’abord introduit par Bodin et al. [5], le langage Skel et l’outil Necro valident toutes ces pro-priétés, comme on le montrera dans cette thèse. En particulier, sa minimalité permet à n’importe qui de programmer très simplement un nouvel outil pour exploiter les sémantiques écrites dans ce langage.
Le but de cette section étant de parler des langages et outils préexistants à Skel, nous allons nous concentrer sur ces derniers.

Plongement dans un langage existant

La première méthode et sans doute la plus simple, que l’on utilise souvent pour des langages très simples comme le λ-calcul, est d’utiliser un langage existant comme OCaml ou Haskell, qu’on appelle alors le langage hôte, pour définir la sémantique du nouveau langage. On peut alors utiliser les fonctionnalités du langages hôte pour modéliser les fonctionnalités du langage cible, dans le cadre d’un plongement superficiel, mais on peut aussi les utiliser pour donner de la modularité ou de la flexibilité au langage dans le cadre d’un plongement profond.
Les travaux réalisés par Liang et al. [14] montrent comment l’utilisation de transformateurs de monades en Haskell permettent de définir la sémantique d’un langage en utilisant Haskell comme langage hôte, de manière modulaire. De même, Wadler [28] montre comment l’utilisation de monades pour un interpréteur permet de rajouter des fonctionnalités sans avoir à altérer la totalité de l’interpréteur à chaque fois.
On peut aussi décrire une sémantique dans un assistant de preuve, comme JSCert [3], qui a été plongée directement dans l’assistant de preuve Coq. Cela permet d’avoir une sémantique utilisable pour faire directement des preuves formelles, et le mécanisme d’extraction de Coq permet ensuite d’avoir une sémantique OCaml exécutable.
Cependant, il peut être difficile de manipuler une telle formalisation, puisque l’AST de ces langages hôtes n’a pas été conçu dans cette optique. De plus, le coût est élevé pour modifier des choix de conception, comme passer d’un plongement superficiel à un plongement profond.
Skel permet également l’usage de monades, comme nous le montrerons dans la section 2.5. Ces monades assurent en effet une grande flexibilité, notamment dans l’ajout incrémental de fonctionnalités, comme cela a pu être expérimenté dans le cadre de JSkel [12].

Écosystèmes complets

Plusieurs systèmes existent qui fournissent à la fois un langage et un ensemble d’outils pour manipuler ce langage, comme nous le faisons avec Skel et Necro. Cependant, dans les langages que nous présentons ci-dessous, même si la liste d’outils et d’extraction possible est longue, elle est généralement difficile à augmenter. Si l’on souhaite extraire du Lem vers quelque chose qui n’est pas prévu, il y aura un travail non négligeable pour créer un outil. Et en général, l’écosystème n’est pas fait pour être étendu, il faut donc par exemple forker l’outil existant.
Lem
Lem [17, 22] est un langage de spécification qui permet des extractions vers de nombreux outils, notamment un interpréteur OCaml et une formalisation dans les assistants de preuve Isa-belle/HOL et Coq. Il ne se réduit pas exclusivement aux langages de programmation, puisqu’il a été utilisé notamment pour spécifier des protocoles de communications, ou un modèle de mémoire faible par exemple.
Lem gère de manière native les ensembles, l’inférence de type et les modules imbriqués. Si cela semble pratique, cela a cependant l’inconvénient de rendre le langage plus lourd et donc plus difficile à manipuler pour créer un nouveau back-end. Il y a notamment dans Lem 4 types d’entiers définis par défaut.
De plus, lors de l’extraction vers Coq, les fonctions sont compilées par des fonctions et les relations par des relations. Cela diffère de notre outil qui ne fait pas la distinction et considère tout comme des relations. Encore une fois, on peut trouver cela utile, mais cela signifie qu’il faut prouver la terminaison des fonctions. Une partie est prouvée automatiquement, mais des preuves de terminaison peuvent être déférées.
Ensuite, Lem a fait le choix de confondre Prop et bool, et donc de travailler en logique classique dans Coq, donc de perdre en calculabilité. L’argumentation soutenue dans [17] est la suivante : The admission of classical axioms to collapse Prop into bool is a matter of taste. Some large Coq developments happily assume classical axioms, others stay firmly within the existing constructive logic provided by Coq. We feel, however, that not restricting the Lem source language to accommodate every nuance exhibited by the backends is worth the admission of these axioms, though to what extent they affect the computational behaviour and automation and proof search tactics of Coq will require further experimentation to fully resolve.
Lem propose également une libraire standard assez complète et autorise à compiler un type/terme vers un type/terme défini par défaut dans le langage cible.
La figure 1.8 présente un λ-calcul par valeur en Lem. Le TEX est généré par Lem.
Ott [26, 21] est un langage et un outil pour spécifier des langages de programmation. Il permet de générer divers codes, notamment une version LATEX pour affichage, des versions Coq et Isabelle/HOL pour faire des preuves formelles, une version OCaml pour effectuer des calculs, et une version Lem.
Ott est conçu pour que les codes écrit en Ott ressemblent à des règles d’inférence écrites à la main. Il y a également une gestion native des lieurs qui présente une importance forte pour les auteurices de l’outil et qui est donc très aboutie. Ott gère les listes et les compréhensions de manière interne, avec des syntaxes utilisant des « . . . ».
On donne dans la figure 1.9 un λ-calcul avec évaluation par valeur en Ott K [24] est un framework exécutable de sémantiques, basé sur des règles de réécriture. Il fonctionne à base de configurations qui capturent les éléments nécessaires au calcul, comme l’état par exemple, tout en cloisonnant les différents éléments, de manière à modulariser au maximum le calcul.
Si la théorie derrière K, et ses nombreuses applications, sont intéressantes, le fort coût d’apprentissage peut être décourageant. De plus, il ne permet pas de s’intéresser aux méta-théories d’un langage 1.
Enfin, la complexité de K rend difficile d’ajouter des extracteurs, par exemple si l’on souhaite générer du code Coq, ce que K ne permet pas encore.
On donne dans la figure 1.10 un λ-calcul avec évaluation par valeur en K.
open import Pervasives
type ident = string
type lambda =
| Ident of ident
| App of lambda ∗ lambda
| Lam of ident ∗ lambda
let is_value (l : lambda) : bool =
match l with
| App _ _ → false
| _ → true end
let rec subst (v : lambda) (x : ident) (w : lambda) = match v with
| Ident y → if y=x then w else v
| App v1 v2 → App (subst v1 x w) (subst v2 x w)
| Lam y body →
if y=x then Lam y body
else Lam y (subst body x w)
end
indreln [Lambda_ss : lambda → lambda → bool]
Lambda_app_ctx_right : ∀ v v′ f .
(Lambda_ss v v′)
=⇒
Lambda_ss (App f v) (App f v′)
and
Lambda_app_ctx_left : ∀ v f f ′ .
(Lambda_ss f f ′) ∧
(is_value v)
=⇒
Lambda_ss (App f v) (App f ′ v)
and
Lambda_app_beta_red : ∀ x v w .
(is_value v)
=⇒
Lambda_ss (App (Lam x v) w) (subst v x w)
metavar termvar, x ::= {{ com term variable }}
{{ isa string}} {{ coq nat}} {{ hol string}} {{ coq-equality }} {{ ocaml int}} {{ lex alphanum}} {{ tex \mathit{[[termvar]]} }}
Langages plongés
Une autre méthode est d’utiliser des langages plongés dans un langage existant, ce qui fournit tous les éléments existant pour le langage hôte, notamment des environnements de développe-ment, mais en garde généralement les limitations. Les langages présentés ci-dessous ne visent pas à être extraits vers d’autres outils.
PLT redex
PLT Redex 2 est un langage dédié pour définir des spécifications de langages de programma-tion. Il est plongé dans le langage Racket, ce qui fournit un IDE et un ensemble de bibliothèques standard. On trouve en figure 1.11 l’exemple du λ-calcul par valeur écrit avec PLT Redex.
Twelf
Twelf 3 est un langage dédié pour spécifier, implémenter et prouver des propriétés de systèmes déductifs, tels que des langages de programmation, ou des logiques. Il fournit également un mode emacs permettant d’exécuter et de vérifier les codes twelf. L’exemple duλ-calcul avec plongement superficiel (les abstractions sont représentées par des fonctions) est donné en figure 1.12.

Skel par l’exemple

Nous décrivons ici comment est spécifiée une sémantique en Skel, en utilisant deux exemples. D’abord la sémantique à petit pas du λ-calcul, sans stratégie d’évaluation, puis la sémantique à grand pas du langage IMP présenté en section 1.1. Ainsi, on a un exemple impératif et un exemple fonctionnel, un exemple petit pas et un exemple grand pas. Une sémantique squelettique est une liste de déclarations de deux sortes différentes. Les déclarations de types et les déclarations de termes, dont chacun peut être spécifié ou non spécifié.
Quand un type est non spécifié, on se contente de donner son nom. Par exemple, lorsque l’on définit la sémantique du λ-calcul, on ne souhaitera sans doute pas spécifier comment les variables seront représentés en mémoire interne, et on déclarera donc type ident.
Un type spécifié peut-être un type variant (c’est-à-dire un type de données algébriques, défini en donnant la liste de ses constructeurs, et de leurs types d’entrée), un alias de type, utilisant la notation :=, ou un type enregistrement (défini en listant ses champs, et les types qu’ils attendent). Par exemple, le type des λ-termes sera un type variant, défini comme suit :
type term =
| Var ident
| App (term, term)
| Lam (ident, term)
Dans cet exemple, (ident, term) est le type produit à deux composantes, dont la première est de type ident, et la seconde de type term.
Un type enregistrement est déclaré par type euler_int = (re: int , im: int) et un alias par type nat := int.
Il est à noter que les types sont implicitement mutuellement récursifs, l’ordre choisi pour les définir n’ayant donc aucune importance. En revanche, les alias de types ne sont pas des types à proprement parler, mais uniquement des alias comme leur nom l’indique. Ils peuvent donc être utilisés avec les autres de manière mutuellement récursive, mais ils doivent in fine être évaluable vers un type, et donc ne pas contenir de boucle dans leur définition. Le typeur, que nous présenterons en section 3.3, vérifie que les définitions sont non cycliques.
Voyons maintenant les déclarations de termes. La déclaration d’un terme non spécifié est sim-plement son nom et son type. Pour déclarer un terme spécifié, on donne également sa définition. Dans notre code, on va par exemple choisir de ne pas spécifier la substitution. On déclare alors val subst: ident → term → term → term. Si l’on choisit de donner plus de détail en la spécifiant tout de même, on peut raffiner a posteriori. En annexe A.1 par exemple, on a fait le choix de spécifier la substitution.
Un exemple simple de terme spécifié est alors le suivant, qui exécute une étape petit pas dans l’évaluation d’un λ-terme.
val ss (t:term): term =
match t with
| Var x -> (branch end: term)
| Lam (x, body) -> let b’ = ss body in Lam (x, b’)
| App (t1, t2) -> branch
let t1′ = ss t1 in App (t1′, t2)
or
let t2′ = ss t2 in App (t1, t2′)
or
let Lam (x, body) = t1 in
subst x t2 body (* body[x←t2] *)
end
end
L’annexe A.1 définit la substitution, et les fonctions utiles pour cette définition.
La reconnaissance de motif avec match … with … end fonctionne comme on en a l’habitude. Le premier motif qui correspond à l’expression reconnue est sélectionné, et le code qui correspond est exécuté. La construction branch … or … end est une primitive Skel qui gère les choix non déterministes. Elle est similaire à l’opérateur ambigu de McCarthy [15], dans le sens où un branchement ne donne aucun résultat que dans l’hypothèse où aucune des branches ne donne un résultat. L’assignation déstructurant let Lam (x, body) = t1 in affirme que t1 est de la forme Lam (_, _). Si cela est vrai, alors les valeurs appropriées seront affectées aux variables x et body et l’évaluation continue avec le subst. Sinon, la troisième branche ne s’éva-luera à aucun résultat. Le premier branchement est vide, donc ss (Var x) ne donnera aucun résultat. En revanche, le deuxième branchement contient plusieurs branches qui peuvent être simultanément valide, et cela fournit du non déterminisme. Il est à noter que contrairement aux branchements, la reconnaissance de motif avec match … with est déterministe.
On constate aussi que le branchement vide indiqué comme squelette pour le cas des variables est explicitement typé. En effet, Le typeur que nous présenterons plus loin ne fait pas d’inférence de type, il faut donc pouvoir décider localement du type d’un branchement, ce qui est impossible avec un branchement vide, si l’on ne le donne pas explicitement.
On constate également que le terme ss s’appelle lui-même. De même que pour les types, les termes sont naturellement mutuellement récursifs.
Passons au langage IMP. Le type des expressions et des instructions a été défini formellement en section 1.1 ; on en donne la définition Skel :
type expr =
| Const lit
| Var ident
| Plus (expr, expr)
| Equal (expr, expr)
| Not expr
type stmt =
| Skip
| Assign (ident, expr)
| Seq (stmt, stmt)
| If (expr, stmt, stmt)
| While (expr, stmt)
Servent de base à cela les types non spécifiés type ident et type lit.
Contrairement au λ-calcul, les valeurs ne sont pas des termes mais bien des éléments d’un nouvel ensemble. Il faut donc des types pour définir les valeurs. Pour les expressions, on peut avoir des valeurs entières ou booléennes. On garde les entiers non spécifiés, supposant qu’ils peuvent être représentés de bien des manières différentes, suivant les architectures notamment. Il est toujours possible de modifier la sémantique a posteriori pour ajouter la spécification des entiers si l’on juge que leur spécification ne doit pas dépendre de l’implémentation. En revanche, on spécifie les booléens.
type value = | Int int | Bool boolean
type int
type boolean = | True | False
Techniquement, comme on le verra dans la section 2.2, tous les constructeurs prennent un argument. Ainsi, la définition ci-dessus pour le type boolean est une méta-notation pour la définition
suivante :
type boolean = | True () | False ()
De la même manière dans les termes, on pourra noter indifféremment True () et True.
Les instructions sont calculées dans un état donné, et le résultat de leur évaluation est l’état atteint après les avoir évaluées. Ainsi, il nous faut donc un type pour représenter ces états, que l’on choisira de ne pas spécifier. On définit donc : type state.

Table des matières

Introduction 
Qu’est-ce qu’une sémantique
Importance des sémantiques formelles
Comment définir des sémantiques
Structure de la thèse
Implémentation
1 Contexte 
1.1 Définitions
1.1.1 Grand pas
1.1.2 Petit pas
1.1.3 Machine abstraite
1.2 Équivalence
1.3 Langages de description de sémantiques
2 Skel et les sémantiques squelettiques 
2.1 Skel par l’exemple
2.2 Formalisme
2.3 Existentielles
2.4 Polymorphisme
2.5 Monades en Skel
2.6 Typage
2.7 Interprétation concrète
2.7.1 Ensembles de valeurs
2.7.2 Règles d’inférence (version inductive)
2.7.3 Règles d’inférence (version itérative)
2.7.4 Subject Reduction et progrès
2.8 Interprétation abstraite
2.8.1 Ensemble de valeurs
2.8.2 Évaluation
2.8.3 Cohérence
3 Necro Lib 
3.1 AST
3.1.1 Le type skeletal_semantics
3.1.2 Les types term et skeleton
3.1.3 Le type necro_type
3.2 Analyse lexical et syntaxique
3.3 Typeur
3.4 Transformations
3.4.1 Interprétation
3.4.2 Transformateurs
3.4.3 Application
4 Necro ML 
4.1 Structure du fichier généré
4.2 Monade d’interprétation
4.2.1 Monade identité
4.2.2 Monade de liste
4.2.3 Monade de continuation
4.2.4 Monade BFS
4.2.5 Monade BFSYield
4.2.6 Randomisation de monade
4.2.7 Autres monades
4.2.8 Évaluation
4.3 Instanciation
5 Necro Coq 
5.1 Structure
5.2 Plongement de Skel
5.3 Typage
5.4 Valeurs
5.4.1 Valeurs de base
5.4.2 Valeurs fonctionnelles non-spécifiées
5.5 Interprétation
5.5.1 Grand pas, version inductive
5.5.2 Grand pas, version itérative
5.5.3 Petit pas
5.5.4 Machine abstraite
5.5.5 Subject Reduction
5.6 Des exemples pratiques
5.6.1 Preuve d’un calcul de factoriel
5.6.2 Preuve d’équivalence de sémantiques
5.7 Applications et facilité d’utilisation
6 Autres outils et travaux futurs 
6.1 Necro Debug
6.2 Modularité
6.3 Utilisation externe de Necro
6.4 Travaux futurs
7 Conclusion 
A Annexes
A.1 λ-calcul sans stratégie d’évaluation (avec substitution)
A.2 Polymorphisme

Télécharger le rapport complet