Browse Source

Moooore

master
zapashcanon 4 years ago
parent
commit
99ef096ed2
Signed by: zapashcanon GPG Key ID: 8981C3C62D1D28F1
  1. 4
      .gitignore
  2. BIN
      img/ENS_PS.png
  3. BIN
      img/Kent_uni.svg
  4. 3
      src/anonymous_function_01.ml
  5. 3
      src/anonymous_function_02.ml
  6. 3
      src/anonymous_function_03.ml
  7. 3
      src/anonymous_function_04.ml
  8. 1
      src/anonymous_functions.tex
  9. 98
      src/biblio.bib
  10. 36
      src/cakeml.tex
  11. 8
      src/content.tex
  12. 2
      src/contexte_du_stage.tex
  13. 43
      src/flat_lang.ml
  14. 41
      src/flat_lang.tex
  15. 5
      src/fold_right_01.ml
  16. 5
      src/fold_right_02.ml
  17. 6
      src/fold_right_03.ml
  18. 3
      src/intro.tex
  19. 48
      src/lambda_lifting.tex
  20. 72
      src/lambda_lifting_algorithms.tex
  21. 16
      src/main.tex
  22. 2
      src/mk_unique_name.ml
  23. 2
      src/méthodes_formelles.tex
  24. 23
      src/our_algo_compute_sol.tex
  25. 20
      src/packages.tex
  26. 34
      src/scope_analysis.tex
  27. 97
      src/scope_analysis_compile_exp.ml
  28. 27
      src/state_of_the_art.tex
  29. 88
      src/title.tex
  30. 9
      src/typing_issue_01.ml
  31. 9
      src/typing_issue_02.ml
  32. 2
      src/typing_issue_out.txt
  33. 16
      src/typing_issue_test.ml

4
.gitignore

@ -6,3 +6,7 @@
*.run.xml
*.aux
*.out
*.cmi
*.cmx
*.o
src/svg-inkscape/

BIN
img/ENS_PS.png

Binary file not shown.

After

Width:  |  Height:  |  Size: 14 KiB

BIN
img/Kent_uni.svg

Binary file not shown.

3
src/anonymous_function_01.ml

@ -0,0 +1,3 @@
let x = 1 in
List.iter (fun el -> print_int (el - x)) [0; 1; 2]

3
src/anonymous_function_02.ml

@ -0,0 +1,3 @@
let x = 1 in
List.iter (let f el = print_int (el - x) in f) [0; 1; 2]

3
src/anonymous_function_03.ml

@ -0,0 +1,3 @@
let x = 1 in
List.iter (let f x el = print_int (el - x) in f x) [0; 1; 2]

3
src/anonymous_function_04.ml

@ -0,0 +1,3 @@
let x = 1 in
List.iter (let f el x = print_int (el - x) in f x) [0; 1; 2]

1
src/anonymous_functions.tex

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

98
src/biblio.bib

@ -1,30 +1,74 @@
@article{BOUAJJANI1999211,
title = "Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations",
journal = "Theoretical Computer Science",
volume = "221",
number = "1",
pages = "211 - 250",
year = "1999",
issn = "0304-3975",
doi = "https://doi.org/10.1016/S0304-3975(99)00033-X",
url = "http://www.sciencedirect.com/science/article/pii/S030439759900033X",
author = "Ahmed Bouajjani and Peter Habermehl",
keywords = "Verification, Infinite-state systems, FIFO-channel systems, Symbolic reachability analysis, Non-regular sets, Automata, Linear constraints"
@inproceedings{Joh85,
author = {Johnsson, Thomas},
title = {Lambda Lifting: Transforming Programs to Recursive Equations},
booktitle = {Proc. Of a Conference on Functional Programming Languages and Computer Architecture},
year = {1985},
isbn = {3-387-15975-4},
location = {Nancy, France},
pages = {190--203},
numpages = {14},
url = {http://dl.acm.org/citation.cfm?id=5280.5292},
acmid = {5292},
publisher = {Springer-Verlag New York, Inc.},
address = {New York, NY, USA},
}
@Inbook{Fischer1998,
author="Fischer, Michael J.
and Rabin, Michael O.",
editor="Caviness, Bob F.
and Johnson, Jeremy R.",
title="Super-Exponential Complexity of Presburger Arithmetic",
bookTitle="Quantifier Elimination and Cylindrical Algebraic Decomposition",
year="1998",
publisher="Springer Vienna",
address="Vienna",
pages="122--135",
abstract="Lower bounds are established on the computational complexity of the decision problem and on the inherent lengths of proofs for two classical decidable theories of logic: the first-order theory of the real numbers under addition, and Presburger arithmetic --- the first-order theory of addition on the natural numbers. There is a fixed constant c > 0 such that for every (nondeterministic) decision procedure for determining the truth of sentences of real addition and for all sufficiently large n, there is a sentence of length n for which the decision procedure runs for more than 2 cn steps. In the case of Presburger arithmetic, the corresponding bound is {\$}{\$}{\{}2^{\{}{\{}2^{\{}cn{\}}{\}}{\}}{\}}{\$}{\$} . These bounds apply also to the minimal lengths of proofs for any complete axiomatization in which the axioms are easily recognized.",
isbn="978-3-7091-9459-1",
doi="10.1007/978-3-7091-9459-1_5",
url="https://doi.org/10.1007/978-3-7091-9459-1_5"
@phdthesis{Ler92,
TITLE = {{Polymorphic typing of an algorithmic language}},
AUTHOR = {Leroy, Xavier},
URL = {https://hal.inria.fr/tel-01499951},
SCHOOL = {{Universit{\'e} Paris 7}},
YEAR = {1992},
MONTH = Jun,
KEYWORDS = {Type systems ; Polymorphism ; ML ; Functional languages ; References ; Communication channels ; Continuations ; Dangerous variables ; Closure typing ; Polymorphism by name ; Natural semantics ; Big-step operational semantics ; Structured operational semantics ; Type soundness ; Variables dangereuses ; Continuations ; Canaux de communication ; Typage ; Polymorphisme ; ML ; Langages applicatifs ; R{\'e}f{\'e}rences ; Typage des fermetures ; Polymorphisme par nom ; S{\'e}mantique naturelle ; S{\'e}mantique op{\'e}rationnelle structur{\'e}e ; S{\^u}ret{\'e} du typage},
TYPE = {Theses},
PDF = {https://hal.inria.fr/tel-01499951/file/these-doctorat.pdf},
HAL_ID = {tel-01499951},
HAL_VERSION = {v1},
}
@InProceedings{Dan02,
author="Danvy, Olivier and Schultz, Ulrik P.",
editor="Hu, Zhenjiang and Rodr{\'i}guez-Artalejo, Mario",
title="Lambda-Lifting in Quadratic Time",
booktitle="Functional and Logic Programming",
year="2002",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="134--151",
abstract="Lambda-lifting is a program transformation used in compilers and in partial evaluators and that operates in cubic time. In this article, we show how to reduce this complexity to quadratic time.",
isbn="978-3-540-45788-6"
}
@inproceedings{Mor06,
title={Improved Graph-Based Lambda Lifting.},
author={Moraz{\'a}n, Marco T. and Mucha, Barbara},
booktitle={Software Engineering Research and Practice},
pages={896--902},
year={2006},
organization={Citeseer}
}
@InProceedings{Mor08,
author="Moraz{\'a}n, Marco T. and Schultz, Ulrik P.",
editor="Chitil, Olaf and Horv{\'a}th, Zolt{\'a}n and Zs{\'o}k, Vikt{\'o}ria",
title="Optimal Lambda Lifting in Quadratic Time",
booktitle="Implementation and Application of Functional Languages",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="37--56",
abstract="The process of lambda lifting flattens a program by lifting all local function definitions to the global level. Optimal lambda lifting computes the minimal set of extraneous parameters needed by each function as is done by the O(n^3) equation-based algorithm proposed by Johnsson. In contrast, modern lambda lifting algorithms have used a graph-based approach to compute the set of extraneous parameters needed by each function. Danvy and Schultz proposed an algorithm that reduced the complexity of lambda lifting from O(n^3) to O(n^2). Their algorithm, however, is an approximation of optimal lambda lifting. Moraz{\'a}n and Mucha proposed an optimal graph-based algorithm at the expense of raising the complexity to O(n^3). Their algorithm, however, suggested that dominator trees might be used to develop an O(n^2) algorithm. This article explores the relationship between the call graph of a program, its dominator tree, and lambda lifting by developing algorithms for successively richer sets of programs. The result of this exploration is an O(n^2) optimal lambda lifting algorithm.",
isbn="978-3-540-85373-2"
}
@PHDTHESIS{Bal12,
url = "http://www.theses.fr/2012PA077198",
title = "La pleine paresse, une certaine optimalité : partage de sous-termes et stratégies de réduction en réécriture d'ordre supérieur",
author = "Balabonski, Thibaut",
year = "2012",
pages = "1 vol. (368 p.)",
note = "Thèse de doctorat dirigée par Kesner, Delia Informatique Paris 7 2012",
note = "2012PA077198",
}

36
src/cakeml.tex

@ -1,2 +1,34 @@
\section{CakeML}
CakeML c'est bien parce que y'a des preuves. C'est plus compliqué à faire. On rend des choses simples compliquées, pour les rendre simples.
\section{\bsc{CakeML}}
\paragraph{}
\href{https://cakeml.org/}{\bsc{CakeML}} est l'un des projets mené - en partie - par l'équipe \bsc{plas}. Il s'agit, en résumé, d'un \emph{compilateur vérifié} pour un dialecte \href{https://fr.wikipedia.org/wiki/ML_(langage)}{\bsc{ml}} proche de \href{https://fr.wikipedia.org/wiki/Standard_ML}{Standard ML}, diverses informations à ce propos sont disponibles sur le site web du \href{http://sml-family.org/}{Standard ML Family project}.
% TODO: define PLAS with some nice HTML-like thing showing the definition on hover
% TODO: use some consistent way to display ML, SML etc.
% TODO: CakeML is Free Software :-) should be mentionned somewhere, maybe after explaining what `source code` is
% TODO: move this after the explanation of what a compiler and a language is ?
\paragraph{}
Tout d'abord, afin de donner une idée de ce qu'est un compilateur au lecteur profane, il faut tenter de montrer ce que sont les ordinateurs et les langages de programmation. Pour cela, reposons-nous sur cette citation\cite{Bal12}:
\begin{quotation}
L'ordinateur est un exécutant parfait. Que des ordres lui soient donnés, il les suit sans sourciller. Il va vite, il ne se trompe pas, il ne connaît pas l'Ennui. Il fait tout ce qui lui est demandé, rien que ce qui lui est demandé, et tout cela sans s'inquiéter des raisons de ses actes.
Et pour cause, l'ordinateur vit dans le \emph{comment}, et ne comprendrait rien au \emph{quoi} ni au \emph{pourquoi}.
Il est parfaitement inutile de lui dire ``j'ai une liste de nombres et j'aimerais en connaître le produit". Pour le faire bouger, tout ce qui compte est de lui préciser la manière dont il doit s'y prendre et lui détailler pas à pas tout ce qu'il doit faire, en n'utilisant que les quelques dizaines d'\emph{instructions} de base qu'il comprend, comme multiplier deux nombres entiers ou aller rechercher en mémoire une information préalablement enregistrée.
Chaque ordinateur a ainsi son propre \emph{langage machine}, formé d'une poignée de mots et de la plus pauvre des grammaires, dont les phrases permettent seulement de lui affecter les quelques tâches qu'il sait réaliser. Pour utiliser ce langage, il faut connaître parfaitement les mécanismes de l'ordinateur, et être capable sans le secours d'Ornicar de prévoir en détail les effets d'une jungle de monosyllabes.
Avouons que programmer dans ces conditions est laborieux. Pour simplifier cela nous utilisons des \emph{langages de programmation} au vocabulaire et aux structures grammaticales plus riches.
% TODO: display this as a nice quotation, format it as in the original document
% TODO: use csquote for the quote inside the quotation block :-)
\end{quotation}
\paragraph{}
Une fois éclairé par cette explication, il est plus simple de comprendre le rôle d'un compilateur. Il s'agit simplement de l'outil qui transforme un programme généralement écrit par un humain dans un langage de programmation \emph{riche} vers un autre langage de programmation plus \emph{pauvre}, celui compréhensible par l'ordinateur. On parle généralement plutôt de langage \emph{bas niveau} pour désigner un langage proche de ce que comprend l'ordinateur et de langage \emph{haut niveau} pour un langage proche de ce que comprend l'humain.
\paragraph{}
Plusieurs questions se posent alors. Comment fait-on un compilateur ? En fait, le compilateur est lui-même un programme. Comme tout programme, il est courant qu'il ne soit pas parfait et qu'il contienne de nombreux bugs. Cela est problématique. Si j'écris un programme, que je l'exécute et qu'il ne se comporte pas de la façon attendue, c'est peut-être parce que j'ai fait une erreur en écrivant le programme, ou peut-être parce que le compilateur a fait une erreur en transformant mon programme.
\paragraph{}
La solution à cela, est de faire une preuve mathématique qui garanti que le compilateur ne fera pas d'erreur. Pour cela, il faut définir formellement ce que signifie \emph{ne pas faire d'erreur}. Un des moyens d'y arriver, est de définir mathématiquement la \emph{sémantique} de notre langage. Une fois cela fait, on peut prouver que, pour n'importe quel programme, le compilateur préserve la sémantique. On a alors la garantie que le résultat produit par le compilateur se comportera exactement comme il devrait. Cela a pour conséquence qu'un programme correctement écrit se comportera exactement comme on l'attend.
\paragraph{}
Il est possible d'effectuer cette formalisation et ces preuves, non pas à la main sur une feuille de papier, mais au moyen de ce que l'on appelle des \href{https://fr.wikipedia.org/wiki/Assistant_de_preuve}{\emph{assistants de preuve}}. Cela revient à écrire les définitions et les preuves sous forme de programme.
\paragraph{}
La sémantique de \bsc{CakeML} a été formalisée au moyen de \href{https://www.cl.cam.ac.uk/~pes20/lem/}{Lem}. Lem permet d'exporter une sémantique donnée vers des définitions compréhensibles par différents assistants de preuve. Dans le cadre du projet \bsc{CakeML}, les preuves sont réalisées en utilisant \href{https://hol-theorem-prover.org/}{\bsc{hol}}.
\paragraph{}
Une fois que la sémantique de notre langage a été formalisée sous forme de définition compréhensible par un assistant de preuve, il ne reste plus qu'à écrire notre compilateur et à prouver que les transformations qu'il effectue préservent la sémantique.

8
src/content.tex

@ -1,8 +0,0 @@
\paragraph{}
La vérification de protocoles revient en partie à vérifier des propriétés sur des \emph{Communicating Finite State Machines} (CFSM). Un moyen de représenter ces CFSM, est d'utiliser des \emph{Constrained Queue Decision Diagram} (CQDD), qui possèdent de nombreuses propriétés intéressantes pour effectuer de l'analyse d'atteignabilité. Les contraintes des CQDD sont des formules de l'arithmétique de Presburger, qui est une logique décidable\cite{BOUAJJANI1999211}.
\paragraph{}
Il peut alors sembler légitime de se demander s'il est possible de trouver une logique \emph{minimale} permettant de représenter les contraintes d'un CQDD et qui soit telle que ce CQDD soit toujours suffisant pour calculer l'effet de n'importe quel cycle dans le graphe de contrôle d'un CFSM\@. Il a été montré que l'arithmétique de Presburger est suffisante\cite{BOUAJJANI1999211}, cependant, il a aussi été montré que la décidabilité d'une formule de l'arithmétique de Presburger est un problème 2EXPTIME-dur\cite{Fischer1998}, il serait donc intéressant d'utiliser une logique moins expressive afin d'essayer d'obtenir une meilleure complexité. Une des raisons qui laissent penser qu'il est possible de faire mieux est le fait que la quantification universelle de l'arithmétique de Presburger n'est jamais utilisée dans les contraintes d'un CQDD\cite{BOUAJJANI1999211}.
\paragraph{}
Une approche pour tenter de répondre à cette question serait de commencer par enlever la quantification universelle: on sait déjà qu'elle n'est pas nécessaire ; puis, de chercher à savoir si le problème de décision est toujours 2EXPTIME-dur. On pourrait ensuite regarder s'il est possible d'exprimer les contraintes de telle sorte qu'on puisse réduire encore notre logique et réitérer le processus de savoir si cela améliore la complexité. On peut aussi montrer que des parties de la logique sont absolument nécessaires et ainsi, savoir qu'on ne pourra faire mieux que ce que l'on fait déjà et que pour vérifier des systèmes trop gros, il faudra se tourner vers d'autres méthodes et non pas seulement attendre que des algorithmes plus efficaces apparaissent.
\paragraph{}
Ainsi, on devrait pouvoir vérifier des protocoles en utilisant les mêmes méthodes, mais en moins de temps. La vérification de programme est importante puisqu'en effet, on sait pas a priori, si un programme est correct. Dans de nombreux cas, le fait de détecter les problèmes une fois qu'ils surviennent n'aura pas de graves conséquences, mais il y a des domaines où cela n'est pas souhaitable: énergie, transport, médecine etc. La vérification de programmes au moyen de preuves mathématiques est donc utile. Cependant, dans des approches telles que le \emph{model checking}, cela n'est pas toujours possible puisque la vérification du programme prend trop de temps. Le fait de réduire le temps de calcul des problèmes d'atteignabilité permet donc d'accélérer la vérification et lorsqu'on change de classe de complexité, la différence est sensible.

2
src/contexte_du_stage.tex

@ -4,4 +4,4 @@
\paragraph{}
Le stage a eu lieu à l'\href{https://www.kent.ac.uk/}{université du Kent}, au sein de la \href{https://www.cs.kent.ac.uk/}{School of Computing} située à \href{https://fr.wikipedia.org/wiki/Canterbury}{Canterbury} et constituée de plusieurs équipes de recherche. J'ai travaillé au sein de l'équipe \href{https://www.cs.kent.ac.uk/research/groups/plas/}{Programming Languages and Systems}.
\paragraph{}
TODO: L'équipe PLAS c'est très bien. Ils font des choses autour des langages et des méthodes formelles.
Un des axes de recherche de l'équipe Programming Languages and System est l'étude des langages de programmation, tant du point de vue de l'implémentation des langages, que de leur formalisation afin de prouver diverses propriétés.

43
src/flat_lang.ml

@ -0,0 +1,43 @@
(** Langage **)
type op = Add | Sub (* etc. *)
type lit = Int of int | String of string (* etc. *)
type varN = string
type con_typ = (int * (int option)) option
type pat =
| Pany (* _ *)
| Pvar of varN (* x *)
| Pcon of con_typ * (pat list) (* Constructor (pat1, ...) *)
| Pref of pat
type exp =
| Raise of exp
(* try `exp` with `pat_exp_map` *)
| Handle of exp * pat_exp_map
| Lit of lit
| Con of con_typ * (exp list)
| Var_local of varN
| Fun of varN * exp (* fun `varN` -> `exp` *)
| App of op * (exp list)
(* if `exp` then `exp` else `exp *)
| If of exp * exp * exp
(* match `exp` with `pat_exp_map` *)
| Mat of exp * pat_exp_map
(* Some varN, then: let `varN` = `exp` in `exp *)
(* None, then: `exp`; `exp` *)
| Let of (varN option) * exp * exp
(* let rec `varN` `varN` = `exp` and ... in `exp` *)
| Letrec of ((varN * varN * exp) list) * exp
and pat_exp_map = (pat * exp) list
(** Sémantique **)
type v =
| Lit_v of lit
| 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

41
src/flat_lang.tex

@ -0,0 +1,41 @@
\section{Flat lang}
\subsection{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.}.
Cet \bsc{ast} n'est autre que notre programme original, représenté sous une forme facilement manipulable, on appelle cette représentation le langage source.
Le lambda lifting est généralement décrit comme étant une transformation \emph{source to source}, c'est-à-dire, opérant directement sur le langage 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é le \emph{type checking}, donc 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 \emph{type checker} 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é:
\inputminted[bgcolor=darkBackground]
{ocaml}
{typing_issue_01.ml}
Cependant, si l'on s'intéresse à son équivalent après lambda lifting\footnote{Cela n'a pas été précisé avant, mais l'étape de \emph{block floating} transforme les fonctions imbriquées en fonctions mutuellement récursives.}:
\inputminted[bgcolor=darkBackground]
{ocaml}
{typing_issue_02.ml}
On obtiendra l'erreur de type suivante\footnote{Cette erreur est dûe à la \emph{value restriction}, plus de détails sont donnés dans }:
\begin{quotation}
\texttt{\input{typing_issue_out.txt}}
\end{quotation}
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 le \emph{type checking}. 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.
Le premier langage intermédiaire, 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{clos lang}, possède une sémantique plus compliquée que \emph{flat lang}, notamment du fait de la présence de fonctions à plusieurs arguments et n'est donc pas adéquat.
Le candidat idéal semble donc être \emph{flat lang}, dont voici un aperçu:
\inputminted[bgcolor=darkBackground]
{ocaml}
{flat_lang.ml}

5
src/fold_right_01.ml

@ -0,0 +1,5 @@
let fold_right f acc l =
let rec aux = function
| [] -> acc
| h::t -> f h (aux t)
in aux l

5
src/fold_right_02.ml

@ -0,0 +1,5 @@
let fold_right f acc l =
let rec aux acc f = function
| [] -> acc
| h::t -> f h (aux acc f t)
in aux acc f l

6
src/fold_right_03.ml

@ -0,0 +1,6 @@
let rec aux acc f = function
| [] -> acc
| h::t -> f h (aux acc f t)
and fold_right f acc l =
aux acc f l

3
src/intro.tex

@ -1,3 +0,0 @@
\section{Introduction}
We assume you're working on a Debian system.

48
src/lambda_lifting.tex

@ -1,2 +1,48 @@
\section{Le lambda-lifting}
Le lambda-lifting c'est bien.
\paragraph{}
En réalité, le compilateur ne se contente généralement pas de transformer le programme naïvement. Il effectue des modifications qui permettent d'optimiser le résultat, afin d'obtenir un programme plus rapide, moins coûteux à la fin. Chacune de ces modifications est appelée une \emph{optimisation}.
\paragraph{}
Le lambda lifting est une optimisation possible. On peut en donner une intuition en passant par la langue française. Faisons pour cela appel au \emph{Maître}, qui nous fournit la phrase suivante:
\begin{quotation}
On cherchait à l'impressionner, à devenir son préféré.
\end{quotation}
Les mots \emph{l'} et \emph{son} font ici référence à une chose qui n'est pas contenue dans la phrase. Il faut nous référer au contexte dans lequel est placée la phrase pour en saisir tout le sens. Et en effet, si l'on regarde quelques lignes plus haut dans l'œuvre:
\begin{quotation}
Elle répondait au nom de Bella. [\ldots] On cherchait à l'impressionner, à devenir son préféré.
\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}.
Le lambda-lifting consisterait tout simplement à éliminer toutes les variables libres. Il s'agirait par exemple de transformer notre exemple afin d'obtenir cela:
\begin{quotation}
On cherchait à impressionner Bella, à devenir son préféré.
\end{quotation}
\paragraph{}
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}.
% TODO: citer le guide de survie ML de la thèse de X. Leroy
\paragraph{}
Pour illuster le lambda lifting, prenons l'exemple de la fonction \texttt{fold\_right} suivante:
% TODO: exemple sans variable libre, plus simple
\inputminted[bgcolor=darkBackground]
{ocaml}
{fold_right_01.ml}
On remarque que les variables \texttt{acc} et \texttt{f} sont libres dans la fonction \texttt{aux}. Du point de vue du programmeur cela a l'avantage d'expliciter le fait qu'au cours des différents appels récursifs successifs de \texttt{aux}, les valeurs de ces variables restent les mêmes que celles que l'on avait lors de l'appel initial à \texttt{fold\_right} ; cela permet aussi de réduire la taille du code écrit.
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'information 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
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 ?
Le but du lambda lifting est donc de se débarasser des variables libres. Si l'on reprend l'exemple précédent, cela consisterait par exemple à transformer le programme de sorte à obtenir ceci:
\inputminted[bgcolor=darkBackground]{ocaml}{fold_right_02.ml}

72
src/lambda_lifting_algorithms.tex

@ -1,6 +1,66 @@
\section{Les algorithmes existant pour le lambda-lifting}
1: $O(n^3)$, pas optimal
2: $O(n^2)$, pas optimal
3: $O(n^3)$, optimal
4: $O(n^2)$, optimal
On va faire le 4ème pck on est forts.
\section{Les algorithmes existants pour le lambda lifting}
\subsection{Différences}
Plusieurs algorithmes ont été présentés pour le lambda lifting. Lorsque l'on parle d'un algorithme pour le lambda lifting, il est généralement question d'une seule étape parmi toutes celles qui composent le processus de lambda lifting: le calcul des paramètres à ajouter à chaque fonction. Les autres étapes n'étant généralement pas abordées, elles sont en effet relativement simples à implémenter en comparaison. Ainsi, lors de la phase de calcul des paramètres, ils se distinguent par plusieurs caractéristiques:
\begin{itemize}
\item l'utilisation d'équations ensemblistes ou bien de graphes
\item la complexité
\item la nécessité d'une évaluation paresseuse
\item l'optimalité dans le sens où l'on veut qu'aucun paramètre inutile ne soit ajouté aux fonctions
\end{itemize}
Voici un tableau résumant cela:
% TODO: less ugly colors %
\begin{tabular}{ccccc}
Algorithme & Méthode & Complexité & Évaluation par. recquise & Optimal\\
\hline
\cite{Joh85} & équations & \cellcolor{red}$O(n^3)$ & \cellcolor{red}oui & \cellcolor{green}oui\\
\cite{Dan02} & graphes & \cellcolor{green}$O(n^2)$ & \cellcolor{green}non & \cellcolor{red}non\\
\cite{Mor06} & graphes & \cellcolor{red}$O(n^3)$ & \cellcolor{green}non & \cellcolor{green}oui\\
\cite{Mor08} & graphes & \cellcolor{green}$O(n^2)$ & \cellcolor{green}non & \cellcolor{green}oui
\end{tabular}
\subsection{Points communs}
\subsubsection{Scope analysis}
Chacun de ces algorithmes fait au départ l'hypothèse que tous les identifiants sont uniques, c'est-à-dire qu'il n'existe pas deux fonctions ou variables portant le même nom. Cette hypothèse est généralement fausse, il faut donc procéder à une première transformation du programme, nommée \emph{scope analysis}, dont le but est de rendre les identifiants uniques.
\subsubsection{Désanonymisation}
Dans les langages de programmation fonctionnelle, il est généralement possible d'écrire des \emph{fonctions anonymes}. Comme toute fonction, elles peuvent contenir des variables libres, par exemple ici, \texttt{x} est libre dans la fonction anonyme:
\inputminted[bgcolor=darkBackground]
{ocaml}
{anonymous_function_01.ml}
On va donc ajouter une phase de désanonymisation, elles subiront ainsi le même traitement que les autres ; sur notre exemple précédent, cela donnerait le résultat suivant:
\inputminted[bgcolor=darkBackground]
{ocaml}
{anonymous_function_02.ml}
\subsubsection{Modification des définitions et appels de fonction}
Une fois que pour chaque fonction on a calculé l'ensemble des paramètres à lui ajouter, il faut les rajouter à sa définition ainsi qu'à chaque appel fait à cette fonction. Sur notre exemple précédent, on aurait l'ensemble de solutions suivant:
\[sol(f) = \{x\}\]
On rajoute donc \texttt{x} à la définition de \texttt{f} ainsi qu'à chaque appel à la fonction:
\inputminted[bgcolor=darkBackground]
{ocaml}
{anonymous_function_03.ml}
Il faut bien noter que l'on place les nouveaux paramètres au début, afin d'éviter des problèmes en liens avec une éventuelle application partielle.\footnote{Le lecteur curieux pourra essayer de placer \texttt{x} après \texttt{el} au moment de la définition de la fonction et observer le résultat.} Il n'y aura de plus pas de conflits d'identifiants, puisqu'on a au préalable pris soin de les rendre uniques.
\subsubsection{Block floating}
Dès lors, chaque fonction est indépendante des autres en termes de \emph{scope}. On peut alors toutes les mettre au même niveau sous forme de fonctions mutuellement récursives. Si l'on reprend l'exemple de la fonction \texttt{fold\_right}, on obtiendrait cela:
\inputminted[bgcolor=darkBackground]
{ocaml}
{fold_right_03.ml}

16
src/main.tex

@ -1,4 +1,4 @@
\documentclass[a4paper,11pt]{article}
\documentclass[a4paper,12pt,titlepage]{article}
\input{packages.tex}
@ -8,22 +8,28 @@
\input{title.tex}
\maketitle
\input{abstract.tex}
\tableofcontents
\input{contexte_du_stage.tex}
\input{méthodes_formelles.tex}
\input{cakeml.tex}
\input{lambda_lifting.tex}
\input{lambda_lifting_algorithms.tex}
\input{flat_lang.tex}
\input{scope_analysis.tex}
\input{anonymous_functions.tex}
\input{our_algo_compute_sol.tex}
\input{state_of_the_art.tex}
\printbibliography{}
\end{document}

2
src/mk_unique_name.ml

@ -0,0 +1,2 @@
let mk_unique_name n s =
(string_of_int n) ^ "_" ^ s

2
src/méthodes_formelles.tex

@ -1,2 +0,0 @@
\section{À propos des langages et des méthodes formelles}
Les langages c'est bien, mais parfois non. Les compilateurs aussi. C'est mieux avec des méthodes formelles.

23
src/our_algo_compute_sol.tex

@ -0,0 +1,23 @@
\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.
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.
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}
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}\]
\[oldSols := \text{pour chaque fonction appartenant à } oldFuns, \text{son ensemble de solution}\]
Nos fonctions mutuellement récursives ne sont dotées que d'un seul argument. 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 \]
\[\text{\ldots}~~~~~~\]
\[~~~~\text{and}~f_n~x_n = e_n \]
\[\text{in}~e~~~~~~~~~~~~~~~~~~~\]

20
src/packages.tex

@ -16,7 +16,7 @@
\usepackage{amssymb} % more maths
\usepackage{dsfont} % and even more maths
\usepackage{color} % color power
\usepackage[dvipsnames]{xcolor} % more color power
\usepackage[dvipsnames, table]{xcolor} % more color power
\definecolor{darkBackground}{HTML}{282c34} % source code background
\definecolor{darkBackgroundHighlight}{HTML}{2c323c} % source code background
\definecolor{lightBackground}{HTML}{D7D3CB} % source code background
@ -33,7 +33,7 @@
\usepackage[cache=false, draft=false]{minted} % source code
\usemintedstyle{paraiso-dark}
\setminted{bgcolor=lightBackground}
\setminted{linenos, autogobble, breaklines, breakanywhere, breakautoindent, fontseries=m, fontsize=\fontsize{9pt}{7pt}, frame=none, stepnumber=2}
\setminted{linenos, autogobble, breaklines, breakanywhere, breakautoindent, fontseries=m, fontsize=\fontsize{12pt}{12pt}, frame=none, stepnumber=2}
\usepackage{placeins} % float displaying
\usepackage{tikz} % .tex figures (e.g. from Dia)
@ -45,14 +45,28 @@ colorlinks = true,
pdfstartview=FitH
}
\usepackage{csquotes}
\usepackage{ellipsis} % correct ...
\usepackage{svg}
\usepackage[
autolang=other,
backend=biber, % choix de l'outil de traitement
babel=hyphen, % environnement linguistique dédié aux entrées en langues alternatives (utilise l'attribut « hyphenation »)
backref=true, % liens dans la bibliographie pour remonter dans le texte
backrefstyle=none, % afficher toutes les utilisations de la référence
bibstyle=alphabetic, % style pour les clés des références dans la bibliographie : [initialesAnnée]
citestyle=alphabetic, % style pour les clés des références dans le texte : [initialesAnnée]
sorting=none, % bibliographie triée par ordre d'utilisation des références
]{biblatex} % support des bibliographies
\usepackage{calligra}
\usepackage{tikz}
\usetikzlibrary{matrix,fit,chains,calc,scopes}
\usepackage{auto-pst-pdf} %To compile psvectorian directly
\usepackage{psvectorian}
\renewcommand*{\psvectorianDefaultColor}{Red}%
\graphicspath{{./../img/}}
\usepackage[bottom]{footmisc}

34
src/scope_analysis.tex

@ -0,0 +1,34 @@
\section{Scope analysis}
\subsection{L'algorithme}
On a tout d'abord la fonction suivante:
\inputminted[bgcolor=darkBackground]
{ocaml}
{mk_unique_name.ml}
Et le cœur de l'algorithme:
\inputminted[bgcolor=darkBackground]
{ocaml}
{scope_analysis_compile_exp.ml}
\subsection{Preuves}
\subsubsection{Preuves de terminaison}
TODO
\subsubsection{Alpha équivalence}
TODO
\subsubsection{Alpha équivalence et scope analysis}
TODO
\subsubsection{Alpha équivalence et évaluation}
TODO

97
src/scope_analysis_compile_exp.ml

@ -0,0 +1,97 @@
let rec compile_p counter repl = function
| Pany => counter, repl, Pany
| Pvar x =>
let newName = mk_unique_name counter x in
counter + 1, (x, newName)::repl, Pvar newName
| Plit lit =>
counter, repl, Plit lit
| Pcon (id, l) =>
| Pref p =>
and compile_ps counter repl = function
| [] => counter, repl, []
| p::ps =>
let counter, repl, p = compile_p counter repl p in
let counter, repl, ps = compile_ps counter repl ps in
counter, repl, p::ps
let rec compile_name_rec_funs counter repl = function
| [] => counter, repl, []
| (fName, vName, e)::funs =>
let newFName = mk_unique_name counter fName in
let (counter, repl, funs) = compile_name_rec_funs (counter + 1) repl funs in
counter, (fName, newFName)::repl, (newFName, vName, e)::funs
let rec compile_exp counter repl = function
| Raise e =>
let (counter, e) = compile_exp counter repl e in
counter, Raise e
| Handle (e, pes) =>
let (counter, e) = compile_exp counter repl e in
let (counter, pes) = compile_pes counter repl pes in
counter, Handle (e, pes)
| Lit l => Lit l
| Con (id, es) =>
let (counter, es) = compile_exps counter repl es in
counter, Con (id, es)
| Var_local x =>
counter, Var_local (match ALOOKUP repl x with
| None => x (* should not happen *)
| Some x => x)
| Fun (x, e) =>
let newName = mk_unique_name counter x in
let counter, e = compile_exp (counter + 1) ((x, newName)::repl) in
counter, Fun (newName, e)
| App (op, es) =>
let counter, es = compile_exps counter repl es in
counter, App (op, es)
| If (e1, e2, e3) =>
let (counter, e1) = compile_exp counter repl e1 in
let (counter, e2) = compile_exp counter repl e2 in
let (counter, e3) = compile_exp counter repl e3 in
counter, If (e1, e2, e3)
| Mat (e, pes) =>
let (counter, e) = compile_exp counter repl e in
let (counter, pes) = compile_pes counter repl pes in
counter, Mat (e, pes)
| Let (x, e1, e2) =>
let newRepl, x, counter = ( match x with
| Some x =>
let newName = mk_unique_name counter x in
((x, newName)::repl), Some newName, (counter + 1)
| None => repl, None, counter
) in
let counter, e1 = compile_exp counter repl e1 in
let counter, e2 = compile_exp counter newRepl e2 in
counter, Let (x, e1, e2)
| Letrec (funs, e) =>
let counter, repl, funs = compile_name_rec_funs counter repl funs in
let counter, funs = compile_funs counter repl funs in
let counter, e = compile_exp counter repl e in
counter, Letrec (funs, e)
and compile_fun counter repl (vName, e) =
let newVName = mk_unique_name counter vName in
let counter, e = compile_exp (counter + 1) ((vName, newVName)::repl) e in
counter, (newName, e)
and compile_funs counter repl = function
| [] => counter, []
| (fName, f)::funs =>
let counter, f = compile_fun counter repl f in
let counter, funs = compile_funs counter repl funs in
counter, (fName, f)::funs
and compile_exps counter repl = function
| [] => counter, []
| e::es =>
let counter, e = compile_exp counter repl e in
let counter, es = compile_exps counter repl es in
counter, e::es
and compile_pe counter repl (p, e) =
let counter, repl, p = compile_p counter repl p in
let counter, e = compile_exp counter repl e in
counter, (p, e)
and compile_pes counter repl = function
| [] => counter, []
| pe::pes =>
let counter, pe = compile_pe counter repl pe in
let counter, pes = compile_pes counter repl pes in
counter, pe::pes

27
src/state_of_the_art.tex

@ -0,0 +1,27 @@
\section{Comparaison avec l'état de l'art, futur}
\subsection{L'algorithme de lambda lifting}
TODO: améliorer la complexité
\subsection{Preuve}
TODO: comparer avec la preuve papier de Julius
\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

88
src/title.tex

@ -1,5 +1,87 @@
\title{Rapport de stage: implémentation et vérification du lambda-lifting dans le compilateur \bsc{CakeML}}
\begin{titlepage}
\begin{center}
\author{\href{mailto:leo@ndrs.fr}{Léo \bsc{Andrès}}}
\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}
\date{\today}
{\fontsize{14}{14}\calligra{Rapport de stage par\\}}
{\fontsize{28}{28}\scshape Léo \bsc{Andrès}\\}
\vspace*{0.01\textheight}
{\fontsize{14}{14}\calligra{\today\\}}
\vspace*{0.03\textheight}
{\fontsize{14}{14}\calligra{Master 1 Jacques \bsc{Herbrand}\\}}
\vspace*{0.03\textheight}
{\includegraphics[width=0.5\textwidth]{ENS_PS.png}}\\
\vspace*{0.1\textheight}
\begin{tikzpicture}[start chain=main going right]
\node[on chain,align=center,draw=none](a1)
{{\fontsize{14}{14}\calligra Supervisé par} \\
{\Large {Dr.~Scott~\bsc{Owens}}}\\
{\fontsize{14}{14}\calligra et} \\
{\Large {Dr.~Hugo~\bsc{Férée}}}};
\node[on chain,align=center,draw=none](a2)
{\psvectorian[width=0.08\textwidth]{67}};
\node[on chain,align=center,draw=none](a3)
{{\fontsize{14}{14}\calligra Effectué à} \\
{\includesvg{Kent_uni.svg}}};
\end{tikzpicture}
\end{center}
\end{titlepage}
%\begin{comment}
%\begin{titlepage}
% \centering
% \includegraphics[width=0.5\textwidth]{./../img/ENS_PS.png}\par\vspace{1cm}
% \includesvg{./../img/Kent_uni.svg}\par\vspace{1cm}
% {\scshape\LARGE École Normale Supérieure Paris-Saclay \par}
% \vspace{1cm}
% {\scshape\Large Rapport de stage\par}
% \vspace{1.5cm}
% {\huge\bfseries Implémentation et vérification du lambda-lifting dans le compilateur \bsc{CakeML}\par}
% \vspace{2cm}
% {\Large Léo \bsc{Andrès}\par{}}
% \vfill
% supervisé par\\
% \vspace{0.5cm}
% Dr.~Scott \bsc{Owens}\\
% et\\
% Dr.~Hugo \bsc{Férée}
% \vfill
% effectué à\\
% \vspace{0.5cm}
% University of Kent
% \vfill
% Bottom of the page
% {\large \today\par}
%\end{titlepage}
%\end{comment}
%\title{Rapport de stage: implémentation et vérification du lambda-lifting dans le compilateur \bsc{CakeML}}
%
%\author{\href{mailto:leo@ndrs.fr}{Léo \bsc{Andrès}}}
%
%\date{\today}

9
src/typing_issue_01.ml

@ -0,0 +1,9 @@
let main () =
let aux x = 42 in
(aux 1) + (aux true)
let _ =
print_int (main ())

9
src/typing_issue_02.ml

@ -0,0 +1,9 @@
let rec aux x = 42
and main () =
(aux 1) + (aux true)
let _ =
print_int (main ())

2
src/typing_issue_out.txt

@ -0,0 +1,2 @@
line 5, characters 17-21:
Error: This expression has type bool but an expression was expected of type int

16
src/typing_issue_test.ml

@ -0,0 +1,16 @@
(* let rec aux = fun x -> 42
and main () =
(aux 1) + (aux true)
*)
let rec aux (x : ('a. 'a)) : int = 42
and m () = aux 1
and n () = aux true
let _ =
print_int ((m ()) + (n ()))
Loading…
Cancel
Save