Browse Source

More and more

master
zapashcanon 4 years ago
parent
commit
76bf92645b
Signed by: zapashcanon GPG Key ID: 8981C3C62D1D28F1
  1. BIN
      img/graph_01.png
  2. BIN
      img/graph_02.png
  3. 4
      src/abstract.tex
  4. 1
      src/anonymous_functions.tex
  5. 8
      src/appendix.tex
  6. 1
      src/flat_lang.ml
  7. 24
      src/flat_lang.tex
  8. 10
      src/lambda_lifting.tex
  9. 2
      src/lambda_lifting_algorithms.tex
  10. 15
      src/letrec.ml
  11. 4
      src/main.tex
  12. 125
      src/our_algo_compute_sol.tex
  13. 4
      src/packages.tex
  14. 29
      src/scope_analysis.tex
  15. 35
      src/state_of_the_art.tex
  16. 5
      src/thx.tex
  17. 4
      src/title.tex

BIN
img/graph_01.png

Binary file not shown.

After

Width:  |  Height:  |  Size: 20 KiB

BIN
img/graph_02.png

Binary file not shown.

After

Width:  |  Height:  |  Size: 5.9 KiB

4
src/abstract.tex

@ -1,5 +1,3 @@
\begin{abstract}
Ce document est un rapport de mon stage \emph{Implémentation et vérification du lambda-lifting dans le compilateur \bsc{CakeML}}, effectué dans le cadre de ma formation en Master 1 Jacques Herbrand à l'École Normale Supérieure Paris-Saclay. Ce stage s'est déroulé sous la direction conjointe de \href{https://www.cs.kent.ac.uk/people/staff/sao/}{Scott \bsc{Owens}} et de \href{https://www.cs.kent.ac.uk/people/staff/hf216/}{Hugo \bsc{Férée}}.
Ce document est un rapport de mon stage \emph{Le psittacisme pour permettre l’oubli motivé: implémentation et vérification du lambda-lifting dans le compilateur \bsc{CakeML}}, effectué dans le cadre de ma formation en Master 1 Jacques Herbrand à l'École Normale Supérieure Paris-Saclay. Ce stage s'est déroulé sous la direction conjointe de \href{https://www.cs.kent.ac.uk/people/staff/sao/}{Scott \bsc{Owens}} et de \href{https://www.cs.kent.ac.uk/people/staff/hf216/}{Hugo \bsc{Férée}}.
\end{abstract}

1
src/anonymous_functions.tex

@ -1 +0,0 @@
\section{Fonctions anonymes}

8
src/appendix.tex

@ -1,9 +1,13 @@
\section{Chaîne de compilation de cakeml}
\section{Chaîne de compilation de cakeml}\label{cakeml-langs}
%\includesvg[width=6cm]{compiler_langs.svg} % TODO: why this one doesn't work ?
\includegraphics[width=6cm]{compiler_langs.png}
\section{Code source des algorithmes et preuves}
\section{Flat lang}\label{flat-lang-def}
\inputminted[bgcolor=darkBackground]{ocaml}{flat_lang.ml}
\section{Code source des algorithmes et preuves}\label{source-code-links}
\begin{itemize}
\item \href{https://github.com/zapashcanon/cakeml/blob/lambdalifting/compiler/backend/flat_lambdaLiftingScript.sml}{application successives des différentes étapes composant le lambda lifting}

1
src/flat_lang.ml

@ -38,6 +38,5 @@ type v =
| Con_v of con_typ * (v list)
| Closure of env * varN * exp
| Rec_closure of env * ((varN * varN * exp) list) * varN
| Loc of int (* TODO: remove this ? *)
| Vector_v of (v list)
and env = (varN * v) list

24
src/flat_lang.tex

@ -1,6 +1,4 @@
\section{Flat lang}
\subsection{La question du langage}
\section{La question du langage}
Lorsque l'on écrit un programme, on l'écrit sous forme de texte. Le compilateur commence alors par procéder à l'analyse lexicale et à l'analyse syntaxique du programme. On récupère alors un \bsc{ast} -- \emph{Abstract Syntax Tree}\footnote{Le français étant une langue dotée de nombreuses nuances, on a le choix entre \emph{Arbre de Syntaxe absTraite} et \emph{Arbre de Syntaxe abstraiTe} ; voire même \emph{Arbre de SynTaxe abstraite} pour les plus téméraires.}.
@ -8,7 +6,7 @@
Le lambda lifting est généralement décrit comme étant une transformation \emph{source to source}, c'est-à-dire, opérant directement sur l'\bsc{ast} source, avant toute autre transformation.
Cependant, on ne peut pas effectuer le lambda lifting avant toute autre transformation. En effet, une des premières étapes, appelée la \emph{vérification de type}\footnote{\emph{Type checking} en anglais.}, dont le but est de vérifier que notre programme est correctement typé, doit être effectuée \emph{avant} le lambda lifting, pour une raison simple: un programme qui sera jugé correct par le compilateur ne le sera plus forcément après l'étape de lambda lifting. En voici un exemple ; le code suivant sera jugé comme étant bien typé:
Cependant, on ne peut pas effectuer le lambda lifting avant toute autre transformation. En effet, une des premières étapes, appelée la \emph{vérification de type}\footnote{\emph{Type checking} en anglais.}, dont le but est de vérifier que notre programme est correctement typé, doit être effectuée \emph{avant} le lambda lifting, pour une raison simple: un programme qui sera jugé correct par le compilateur ne le sera pas forcément après l'étape de lambda lifting. En voici un exemple ; le code suivant sera jugé comme étant bien typé:
\inputminted[bgcolor=darkBackground]
{ocaml}
@ -26,22 +24,12 @@ Cependant, si l'on s'intéresse à son équivalent après lambda lifting\footnot
\texttt{\input{typing_issue_out.txt}}
\end{quotation}
Se pose alors la question suivante: à quel moment est-il judicieux d'effectuer le lambda lifting ?
% TODO: move this in appendix
%\begin{wrapfigure}{r}{2.8cm}
%\caption{L'ensembles des langages intermédiaires de \bsc{CakeML}}\label{compiler-langs}
% \includegraphics[width=2.8cm]{compiler_langs.png}
%\end{wrapfigure}
Se pose alors la question suivante: à quel moment est-il judicieux d'effectuer le lambda lifting ?
Premièrement, on sait déjà qu'il est nécessaire de l'effectuer après la vérification de type. Il s'agit ensuite de choisir s'il est préférable de l'effectuer sur le langage source ou bien sur un langage intermédiaire. Le but étant d'avoir à la fois un langage dont la grammaire est la plus petite possible, afin de minimiser le nombre de cas à traiter lors de l'implémentation\footnote{Et donc, indirectement, de minimiser la taille de la preuve.} mais aussi de choisir un langage possédant une sémantique simple pour ne pas complexifier la preuve.
Premièrement, on sait déjà qu'il est nécessaire de l'effectuer après la vérification de type. Il s'agit ensuite de choisir s'il est préférable de l'effectuer sur le langage source ou bien sur un langage intermédiaire. Le but étant d'avoir à la fois un langage dont la grammaire soit la plus petite possible, afin de minimiser le nombre de cas à traiter lors de l'implémentation\footnote{Et donc, indirectement, de minimiser la taille de la preuve.} mais aussi de choisir un langage possédant une sémantique simple pour ne pas complexifier la preuve.
Un graphique représentant l'ensemble des langages intermédiaires est donné en annexe. (TODO: ref)Le premier d'entre, appelé \emph{flat lang}, est plus simple que le langage source: il n'y a plus de module, de tuple et de variable et fonction globale, les constructeurs sont simplifiés\footnote{Ils ne sont plus identifiés par des noms mais par des entiers uniques.}\ldots De plus, sa sémantique est comparable à celle du langage source. % TODO: ldots with a correct space after
Un graphique représentant l'ensemble des langages intermédiaires est donné en annexe \ref{cakeml-langs}. Le premier d'entre eux, appelé \emph{flat lang}, est plus simple que le langage source: il n'y a plus de module, de tuple et de variable et fonction globale, les constructeurs sont simplifiés\footnote{Ils ne sont plus identifiés par des noms mais par des entiers uniques.}\ldots De plus, sa sémantique est comparable à celle du langage source. % TODO: ldots with a correct space after
Le langage intermédiaire suivant, \emph{pat lang}, n'utilise plus des noms pour identifier les variables et les fonctions, mais \href{https://en.wikipedia.org/wiki/De_Bruijn_index}{des indices de \bsc{de Bruijn}} ce qui rend difficile la manipulation des termes.
Le candidat idéal semble donc être \emph{flat lang}, dont voici un aperçu:
\inputminted[bgcolor=darkBackground]
{ocaml}
{flat_lang.ml}
Le candidat idéal semble donc être \emph{flat lang}, dont un aperçu est donné en annexe \ref{flat-lang-def}.

10
src/lambda_lifting.tex

@ -1,4 +1,4 @@
\section{Le lambda-lifting}
\section{Le lambda lifting}
\subsection{Les optimisations du compilateur}
@ -29,7 +29,7 @@
\end{quotation}
% TODO: better [\ldots]
On s'aperçoit qu'il est ici question de \emph{Bella}. En mathématiques et en informatique, lorsque l'on s'intéresse à une phrase --- on parlera plutôt de \emph{terme} ---, lorsqu'un mot --- on parlera plutôt de \emph{variable} --- fait référence à une chose qui n'est pas définie au sein même du terme, on dit que la variable est \emph{libre}. Sinon, elle est dite \emph{liée}. Lorsque toutes les variables sont liées dans un terme, on dit qu'il est \emph{clos}. Autrement, on parle de terme \emph{ouvert}. % TODO: changer l'analogie phrase/mot par bout de texte/truc
On s'aperçoit qu'il est ici question de \emph{Bella}. En mathématiques et en informatique, lorsque l'on s'intéresse à une phrase --- on parlera plutôt de \emph{terme} ---, si un mot --- on parlera plutôt de \emph{variable} --- fait référence à une chose qui n'est pas définie au sein même du terme, on dit que la variable est \emph{libre}. Sinon, elle est dite \emph{liée}. Lorsque toutes les variables sont liées dans un terme, on dit qu'il est \emph{clos}. Autrement, on parle de terme \emph{ouvert}. % TODO: changer l'analogie phrase/mot par bout de texte/truc
Le lambda-lifting consisterait tout simplement à éliminer toutes les variables libres. Il s'agirait par exemple de transformer notre exemple afin d'obtenir cela:
@ -42,7 +42,7 @@
En réalité, il s'agit plus exactement d'éliminer les variables libres de chaque \emph{fonction}. Dès que l'on parle de fonction, il est plus simple de s'appuyer sur un langage de programmation, or il est difficile d'écrire un cours de programmation qui permette de comprendre tout ce qui va suivre en seulement quelques paragraphes. Le langage utilisé pour les exemples sera \bsc{OCaml}.
\subsection{Un exemple informatique}
% TODO: citer le guide de survie ML de la thèse de X. Leroy
Pour illuster le lambda lifting, prenons l'exemple de la fonction \texttt{fold\_right} suivante:
Pour illustrer le lambda lifting, prenons l'exemple de la fonction \texttt{fold\_right} suivante:
% TODO: exemple sans variable libre, plus simple
\inputminted[bgcolor=darkBackground]
{ocaml}
@ -52,9 +52,9 @@
Cependant, si l'on se place du point de vue du compilateur, une variable libre signifie qu'il faudra créer ce que l'on appelle une \emph{fermeture} --- ou \emph{closure} en anglais. Une fermeture est stockée dans un endroit de la mémoire appelé le \emph{tas}. % TODO: parler du fait de la survie aux appels de fonctions etc. voir le cours de Jean-Christophe page 102
Il existe plusieurs autres endroits où stocker de l'information. Le dilemme étant généralement le suivant: plus l'accès à un endroit permettant de stocker de la mémoire est rapide, plus la quantité d'informations qu'il est possible d'y stocker est faible. Par exemple, les \emph{registres} sont ce qu'il y a de plus rapide, mais il est généralement possible d'y stocker quelques nombres seulement ; à l'opposé, le disque dur d'un ordinateur permet aujourd'hui de stocker énormément d'informations, mais il est très lent d'y accéder. Le tas se situe à mi-chemin entre les registres et le disque dur. % TODO: analogie avec campagne / banlieue / grandes villes, et le prix / temps
Il existe plusieurs autres endroits où stocker de l'information. Le dilemme étant généralement le suivant: plus l'accès à un endroit permettant de stocker de la mémoire est rapide, plus la quantité d'informations qu'il est possible d'y stocker est faible. Par exemple, les \emph{registres} sont ce qu'il y a de plus rapide, mais il n'est généralement possible d'y stocker que quelques nombres ; à l'opposé, le disque dur d'un ordinateur permet aujourd'hui de stocker une très importante quantité d'informations, mais il est très long d'y accéder. Le tas se situe à mi-chemin entre les registres et le disque dur. % TODO: analogie avec campagne / banlieue / grandes villes, et le prix / temps
Si l'on évitait la création de la fermeture, il serait alors possible de ne pas avoir à stocker cette information sur le tas et de pouvoir utiliser un autre endroit de la mémoire plus rapide, comme la pile ou les registres. % la pile est-elle vraiment plus rapide que les registres ?
Si l'on évite la création de la fermeture, il est alors possible d'utiliser les registres dans un plus grand nombre de cas ; et donc, d'obtenir un programme plus rapide.
Le but du lambda lifting est donc de se débarrasser des variables libres. Si l'on reprend l'exemple précédent, cela consisterait par exemple à transformer le programme de sorte à obtenir ceci:

2
src/lambda_lifting_algorithms.tex

@ -65,4 +65,4 @@
{ocaml}
{fold_right_03.ml}
Dans l'article original \cite{Joh85}, le lambda lifting, avant d'être vu comme une optimisation possible, était surtout un moyen de parvenir à compiler des fonctions imbriquées pouvant posséder des variables libres. L'étape de \emph{block floating} était donc celle qui débarrassait le programme des fonctions imbriquées et où l'on avait donc atteint l'objectif visé. Dans notre cas, cette étape revêt moins d'importance, plus de détails seront donnés au moment plus bas. TODO: lien vers l'étape où l'on explique qu'on ne fait pas de block floating puisque c'est déjà implémenté indirectement avec la création de closure (vides dans notre cas).
Dans l'article original \cite{Joh85}, le lambda lifting, avant d'être vu comme une optimisation possible, était surtout un moyen de parvenir à compiler des fonctions imbriquées pouvant posséder des variables libres. L'étape de \emph{block floating} était donc celle qui débarrassait le programme des fonctions imbriquées et où l'on avait donc atteint l'objectif visé. Dans notre cas, cette étape revêt moins d'importance, un équivalent étant déjà implémenté dans \bsc{CakeML} lors de la création des fermetures\footnote{Les fermetures seront donc vides du fait du lambda lifting, mais les fonctions seront toujours indépendantes}.

15
src/letrec.ml

@ -0,0 +1,15 @@
let f x =
let rec g ... =
... x ... a ... b .... c ... d ...
and a ... =
... b ...
and b ... =
... c ... d ...
and c ... =
... g ...
and d ... =
...
in
...

4
src/main.tex

@ -24,12 +24,12 @@
\input{scope_analysis.tex}
\input{anonymous_functions.tex}
\input{our_algo_compute_sol.tex}
\input{state_of_the_art.tex}
\input{thx.tex}
\appendix
\input{appendix.tex}

125
src/our_algo_compute_sol.tex

@ -1,22 +1,28 @@
\section{Notre algorithme}
Notre algorithme utilise tout d'abord des équations ensemblistes, puis utilise des graphes pour traiter le cas des équations mutuellement récursives, puisque l'on ne dispose pas de l'évaluation paresseuse.
\subsection{Présentation générale}
La complexité de l'algorithme est supérieure à celle des autres algorithmes. En effet, l'implémentation pour les opérations ensemblistes et sur les graphes utilise des listes et des listes d'association. Il n'y a pas d'implémentation vérifiée des tables de hachage en HOL/CakeML et il est de manière générale plus facile de raisonner sur les listes, d'où ce choix.
Notre algorithme utilise tout d'abord des équations ensemblistes, puis utilise momentanément des graphes pour traiter le cas des équations mutuellement récursives, puisque l'on ne dispose pas de l'évaluation paresseuse.
La complexité de l'algorithme est supérieure à celle des autres algorithmes. En effet, l'implémentation pour les opérations ensemblistes et sur les graphes utilise des listes et des listes d'associations. Il n'y a pas d'implémentation vérifiée des tables de hachage en \bsc{hol} et il est de manière générale plus facile de raisonner sur les listes, d'où ce choix.
En revanche, notre algorithme est optimal, dans le sens où il ne rajoute aucun argument qui ne soit nécessaire.
\subsection{Cas des fonctions mutuellement récursives}
Actuellement, la quasi-totalité des preuves de terminaison est réalisée. Il reste à prouver la correction de l'algorithme, pour l'instant seules quelques propriétés ont été prouvées.
On utilise un algorithme récursif sur les expressions. La plupart des cas sont simples à traiter, c'est pourquoi seul le cas des fonctions mutuellement récursives sera détaillé.
On maintient en permanence ces trois ensembles:
On définit d'abord les ensembles suivants:
\[oldVars := \text{l'ensemble des variables dans le scope courant}\]
\[oldFuns := \text{l'ensemble des fonctions dans le scope courant}\]
\[oldSol_g := \text{si } g \in oldFuns, \text{son ensemble de solutions, sinon } \varnothing\]
\[oldVars := \text{l'ensemble des variables dans le scope courant}\]
\[oldFuns := \text{l'ensemble des fonctions dans le scope courant}\]
\[oldSol_g := \text{si } g \in oldFuns, \text{son ensemble de solutions, sinon } \varnothing\]
Ils sont au départ tous vides.
Dans tous les autres cas, ces ensembles se calculent facilement.
\subsection{Cas des fonctions mutuellement récursives}
Nos fonctions mutuellement récursives ne sont dotées que d'un seul argument. On a ainsi quelque chose de cette forme:
Nos fonctions mutuellement récursives ne sont dotées que d'un seul argument\footnote{Dans le cas d'une fonction à plusieurs arguments, on aura tout simplement quelque chose de la forme \texttt{let rec f x = fun y -> \ldots}}. On a ainsi quelque chose de cette forme:
\[\text{let rec}~f_1~x_1 = e_1 \]
\[~~~~\text{and}~f_2~x_2 = e_2 \]
@ -26,10 +32,12 @@
On pose alors:
\[introducedFuns := \{f_1, \ldots, f_n\}\]
\[introducedVars := \varnothing \]
\[accessibleFuns := oldFuns \cup introducedFuns \]
\[accessibleVars := oldVars \cup introducedVars \]
\begin{align}
introducedFuns &:= \{f_1, \ldots, f_n\}\notag\\
introducedVars &:= \varnothing \notag\\
accessibleFuns &:= oldFuns \cup introducedFuns \notag\\
accessibleVars &:= oldVars \cup introducedVars \notag
\end{align}
Notre langage ne dispose pas de variables mutuellement récursives comme c'est par exemple le cas en \bsc{OCaml}, d'où l'ensemble vide. Dans le cas contraire, il suffirait d'ajouter ces variables à l'ensemble idoine pour que l'algorithme fonctionne tout de même.
@ -67,14 +75,95 @@
Autrement dit, si notre nœud $A$ contient les fonctions $\{g_1, \ldots, g_m\}$ et qu'il a pour voisins extérieurs l'ensemble des nœuds $outNeighbours$, on pose:
\[SCCSol_A = localSCCSol_A \cap globalSCCSol_A\]
\begin{align}
SCCSol_A &= localSCCSol_A \cap globalSCCSol_A\notag\\
localSCCSol_A &= \bigcup\limits_{i \in \{1, \ldots, m\}} localSol_i\notag\\
globalSCCSol_A &= \bigcup\limits_{X \in outNeighbours} SCCsol_X \notag
\end{align}
On a alors:
\[\forall f_i \in A, sol_i = SCCSol_A\]
Il ne reste plus qu'à poursuivre notre algorithme récursivement sur chacun des $e_i$ avec $i \in \{1, \ldots, n\}$ et sur $e$.
\subsection{Exemple}
Prenons le code suivant\footnote{Inspiré d'un exemple utilisé dans \cite{Mor08}.}:
\inputminted[bgcolor=darkBackground]
{ocaml}
{letrec.ml}
Au moment de traiter l'ensemble des fonctions mutuellement récursives, on a les ensembles suivants:
\begin{align}
oldVars &= \{x\}\notag\\
oldFuns &= \varnothing\notag\\
oldSol &= \varnothing\notag
\end{align}
\[localSCCSol_A = \bigcup\limits_{i \in \{1, \ldots, m\}} localSol_i\]
Si \texttt{f} était récursive, on aurait $oldFuns = \{f\}$. On commence alors par calculer les ensembles suivants:
\[globalSCCSol_A = \bigcup\limits_{X \in outNeighbours} SCCsol_X \]
\begin{align}
introducedFuns &= \{g, a, b, c, d\}\notag\\
introducedVars &= \varnothing\notag\\
accessibleFuns &= \{g, a, b, c, d\}\notag\\
accessibleVars &= \{x\}\notag
\end{align}
Puis:
\begin{align}
freeID_g &= \{x, a, b, c, d\}\notag\\
freeID_a &= \{b\}\notag\\
freeID_b &= \{c, d\}\notag\\
freeID_c &= \{g\}\notag\\
freeID_d &= \varnothing\notag
\end{align}
Ici, $oldFuns = \varnothing$, donc $\forall i, freeID_i = localDeps_i$. D'où:
\begin{align}
localSol_g &= \{x\}\notag\\
localSol_a = localSol_b = localSol_c = localSol_d &= \varnothing\notag
\end{align}
Il faut maintenant passer à une représentation utilisant des graphes. On aura le graphe d'appel initial suivant:
\begin {center}
\includegraphics[scale=0.6]{graph_01.png}
\end{center}
Notre calcul des composantes fortement connexes nous donne l'ensemble suivant:
\[\{\{g, a, b, c\}, \{d\}\}\]
On reconstruit le graphe d'appel entre les composantes fortement connexes et en retirant les arrêtes d'un nœud vers lui-même:
\begin {center}
\includegraphics[scale=0.6]{graph_02.png}
\end{center}
On a alors:
\[\forall f_i \in A, sol_i = SCCSol_A\]
\begin{align}
localSCCSol_{\{g, a, b, c\}} &= \{x\}\notag\\
localSCCSol_{\{d\}} &= \varnothing\notag
\end{align}
D'où:
\begin{align}
globalSCCSol_{\{g, a, b, c\}} &= \{x\}\notag\\
globalSCCSol_{\{d\}} &= \varnothing\notag
\end{align}
Finalement:
\begin{align}
sol_g = sol_a = sol_b = sol_c &= \{x\}\notag\\
sol_d &= \varnothing\notag
\end{align}
Il ne reste plus qu'à poursuivre notre algorithme récursivement sur chacun des $e_i$ avec $i \in \{1, \ldots, n\}$ et sur $e$. TODO: parler des nouvelles valeurs pour oldFuns, oldVars et oldSol.
Si l'on introduit les paramètres à l'endroit idoine, il est facile de vérifier à la main que plus aucune fonction ne possède de variable libre, qu'aucune ne possède de paramètre inutile\footnote{\texttt{x} n'est pas ajouté aux arguments de \texttt{d}} et qu'il ne leur manque aucun paramètre.

4
src/packages.tex

@ -62,7 +62,7 @@ pdfstartview=FitH
\usepackage{calligra}
\usepackage{tikz}
\usetikzlibrary{matrix,fit,chains,calc,scopes}
\usetikzlibrary{matrix, fit, chains, calc, scopes, positioning}
\usepackage{auto-pst-pdf} %To compile psvectorian directly
\usepackage{psvectorian}
\renewcommand*{\psvectorianDefaultColor}{Red}%
@ -71,3 +71,5 @@ pdfstartview=FitH
\usepackage[bottom]{footmisc}
\usepackage{wrapfig}
\definecolor {processblue}{cmyk}{0.96,0,0,0}

29
src/scope_analysis.tex

@ -1,23 +1,40 @@
\section{Scope analysis}
\section{Analyse de portée}
\subsection{L'algorithme}
Un lien vers le code de l'algorithme est donné en annexe. L'idée de l'algorithme est simple: on parcourt récursivement notre programme et on maintient une liste d'association faisant correspondre à chaque identifiant son remplaçant. On ne peut pas utiliser de références, ce qui rend notre algorithme moins lisible ; en effet, dans le cas contraire, il aurait suffit de gérer le compteur dans la fonction \texttt{mk\_unique\_name} en utilisant une fermeture.
Un lien vers le code de l'algorithme est donné en annexe. L'idée de l'algorithme est simple: on parcourt récursivement notre programme et on maintient une liste d'association faisant correspondre à chaque identifiant son remplaçant. On ne peut utiliser de références, ce qui rend notre algorithme moins lisible ; en effet, dans le cas contraire, il aurait suffit de gérer le compteur dans la fonction \texttt{mk\_unique\_name} en utilisant une fermeture.
\subsection{Preuves}
\subsubsection{Preuves de terminaison}
Dès que l'on définit une fonction, si sa terminaison n'est pas évidente pour \bsc{hol}, il faut en donner une preuve. Cela se fait généralement en utilisant la tactique \texttt{WF\_REL\_TAC} qui prend une relation bien fondée, puis en montrant ce que nous demande \bsc{hol} par récurrence. Dans la plupart des cas, des relations déjà existantes suffisaient ; cela n'a pas été le cas au moment où l'on modifie les identifiants puisqu'en effet, la relation usuelle \texttt{exp\_size} utilise entre autres la taille des identifiants.
Dès que l'on définit une fonction, si sa terminaison n'est pas évidente pour \bsc{hol}, il faut en donner une preuve. Cela se fait généralement en utilisant la tactique \texttt{WF\_REL\_TAC} qui prend une relation bien fondée, puis en montrant ce que nous demande \bsc{hol} par récurrence. Dans la plupart des cas, des relations déjà existantes suffisaient ; cela n'a pas été le cas au moment où l'on a modifié les identifiants puisqu'en effet, la relation usuelle \texttt{exp\_size} utilise entre autres la taille des identifiants.
\subsubsection{Alpha équivalence}
L'idée ici a été de définir une relation s'apparentant à l'alpha équivalence. Cependant, dans notre cas, cette relation ne s'applique pas seulement à deux expresssions, mais aussi à un environnement. On a ensuite pu prouver diversers propriétés sur cette relation, elle est notamment réflexive et transitive.
L'idée ici a été de définir une relation s'apparentant à l'alpha équivalence. Cependant, dans notre cas, cette relation ne s'applique pas seulement à deux expressions, mais aussi à un environnement. On a ensuite pu prouver diverses propriétés sur cette relation, elle est notamment réflexive et transitive.
\subsubsection{Alpha équivalence et analyse de portée}
Une fois cette relation d'alpha équivalence définie, il a été possible de montrer que pour un programme bien formé, c'est-à-dire clos et bien typé, ce programme et son image après analyse de portée sont alpha équivalents.
Une fois cette relation d'alpha équivalence définie, il a été possible de montrer que pour un programme bien formé, c'est-à-dire clos et bien typé, ce programme et son image après analyse de portée sont alpha équivalents. Une version simplifiée du théorème est la suivante:
\begin{align}
\forall~&(\texttt{exp},~\texttt{exp'},~\texttt{env}),\notag\\
&\texttt{is\_valid\_exp}(\texttt{env},~\texttt{exp})\notag\\
\land~&\texttt{is\_valid\_env}(\texttt{env})\notag\\
\land~&\texttt{compile\_exp}(\texttt{env},~\texttt{exp}) = (\texttt{exp'})\notag\\
\implies~&\texttt{alpha\_eq\_exp}(\texttt{env},~\texttt{exp},~\texttt{exp'})\notag
\end{align}
\subsubsection{Alpha équivalence et évaluation}
Dès lors, il reste à montrer que si deux programmes sont alpha équivalents, leur sémantique est identique. Pour cela, on montre que leur image par la fonction \texttt{eval} est la même.
Dès lors, il reste à montrer que si deux programmes sont alpha équivalents, leur sémantique est identique. Pour cela, on montre que leur image par la fonction \texttt{eval} est la même:
\begin{align}
\forall~&(\texttt{exp},~\texttt{exp'}, \texttt{env},~\texttt{env'},~\texttt{result},~\texttt{result'}),\notag\\
&\texttt{alpha\_eq\_env}(\texttt{env},~\texttt{env'})\notag\\
\land~&\texttt{alpha\_eq\_exp}(\varnothing,~\texttt{exp},~\texttt{exp'})\notag\\
\land~&\texttt{evaluate}(\texttt{env},~\texttt{exp}) = \texttt{result}\notag\\
\land~&\texttt{evaluate}(\texttt{env'},~\texttt{exp'}) = \texttt{result'}\notag\\
\implies&\texttt{result\_eq}(\texttt{res},~\texttt{res'})\notag
\end{align}

35
src/state_of_the_art.tex

@ -1,28 +1,15 @@
\section{Comparaison avec l'état de l'art, futur}
\section{Comparaison avec l'état de l'art}
\subsection{L'algorithme de lambda lifting}
En comparaison des algorithmes existant, notre algorithme remplit tous les critères intéressants à l'exception de la complexité, qui peut cependant encore être améliorée. En revanche, dans les différents articles cités précedemment, aucun ne donne plus qu'une intuition quant à la correction de l'algorithme. Une preuve est donnée dans~\cite{Ker12}, cependant, l'algorithme n'y est pas optimal\footnote{Dans le sens où des paramètres inutiles seront ajoutés.}, seulement l'étape de calcul des paramètres y est traitée et la preuve n'est pas vérifiée par un assistant de preuve.
TODO: comparer avec les autres algos.
Un des principal aspect de notre algorithme qu'il serait intéressant d'améliorer serait la complexité. Nos fonctions sur les graphes et les ensembles ne sont pas efficaces. Ce choix a été fait dans l'optique de simplifier les preuves. Cependant, si l'ensembles des théorèmes touchant à ces fonctions uniquement sont démontrés pour une autre implémentation, l'ensemble des preuves qui ne leurs sont pas directement liées devraient rester valable.
\section{Travaux futurs}
\subsection{Preuve}
Plusieurs points peuvent encore être améliorés ou étudiés, notamment:
Dans les différents articles cités précedemment, aucun ne donne plus qu'une intuition quant à la correction de l'algorithme. Une preuve est donnée dans \cite{Ker12}, cependant, l'algorithme n'y est pas optimal\footnote{Dans le sens où des paramètres inutiles seront ajoutés.}, seulement l'étape de calcul des paramètres y est traitée et la preuve n'est pas vérifiée par un assistant de preuve.
\subsection{Aller plus loin}
\subsubsection{Benchmarks}
TODO
\subsubsection{Gérer plus de scopes}
TODO: cf. page wiki sur les scopes
\subsection{Skolemisation}
TODO
\subsection{Restriction value}
TODO
\begin{itemize}
\item amélioration de la complexité, notamment en implémentant les ensembles et les graphes de façon plus efficace
\item une série de \emph{benchmarks} permettant de mesurer l'impact du lambda lifting sur le temps d'exécution
\item la gestion de l'analyse de portée pour différents types de \emph{scopes} non utilisés dans \bsc{CakeML}: l'\emph{overloading}, les \emph{namespaces} \ldots
\item la réutilisation de l'analyse de portée dans le cadre du projet \href{https://www.cs.kent.ac.uk/projects/trustworthy-refactoring/Trustworthy_Refactoring/Home.html}{Trustworthy Refactoring} mené au sein de l'équipe \bsc{plas}.
\item une comparaison avec la \emph{Skolémisation}, il semblerait en effet que ces deux processus partagent certains aspects
\end{itemize}

5
src/thx.tex

@ -0,0 +1,5 @@
\section{Des conditions optimales}
Ce stage s'est déroulé sous des conditions optimales ; de quoi se promener, du café, un piano, et la sémantique préservée: que demander de plus ?
Il me tient donc à cœur de remercier plusieurs personnes pour avoir permis cela. Tout d'abord, David \bsc{Baelde} qui a su me diriger vers ce stage malgré mon absence quasi-totale d'idée quant à ce que je voulais faire\footnote{"J'aime bien \bsc{OCaml}, la compilation et la logique."}. Scott \bsc{Owens} pour m'avoir accepté comme stagiaire et tout ce qui s'en est suivi\footnote{C'est-à-dire: beaucoup de choses!}. Hugo \bsc{Férée}, pour avoir pris le temps de me fournir de nombreuses explications sur les assistants de preuves, la culture anglaise et son aide permanente. Tous mes camarades du bureau \bsc{sw12}, qui ont égayé bien des journées: Anouk, Marco, Reuben et Simon\footnote{Et bien évidemment Hugo une seconde fois !}. L'ensemble des membres de l'équiple \bsc{plas} (et les quelques autres venus d'ailleurs!) pour ces repas et ces vendredis soirs partagés. Enfin, j'ai eu la chance de croiser le chemin de plusieurs autres personnes qui ont donné une petite touche céleste à ces quelques mois, je ne peux toutes les nommer ici, j'aimerais cependant dire merci de façon particulière à Charlotte et ειρηνη pour les instants à Londres, à Tim et Rebecca pour avoir été d'aussi formidables \emph{housemates} et à Dulcie qui a su envoyer un peu de \emph{cosmic dust} au moyen de sa voix lors de ces nombreuses soirées jazz.

4
src/title.tex

@ -1,8 +1,8 @@
\begin{titlepage}
\begin{center}
\vspace*{0.1\textheight}
\fontsize{25}{25}\scshape Implémentation et vérification du lambda lifting pour le compilateur \bsc{CakeML}\\
%\vspace*{0.1\textheight}
\fontsize{25}{25}\scshape Le psittacisme pour permettre l'oubli motivé: implémentation et vérification du lambda lifting pour le compilateur \bsc{CakeML}\\
\vspace*{0.1\textheight}
{\fontsize{14}{14}\calligra{Rapport de stage par\\}}

Loading…
Cancel
Save