l-lifting

6.2 l-lifting

Le l-lifting ([]) transforme un programme fonctionnel contenant des déclarations de fonctions locales avec ou sans variables libres en un programme qui ne possède que des définitions de fonctions globales (combinateurs). Cette technique aplatit le programme en rendant au même niveau (global) toutes les déclarations rencontrées.
Toute variable libre d'une expression fonctionnelle peut être vue comme un paramètre supplémentaire de celle-ci. Par exemple, l'expression lx.e où e contient une variable libre y peut se réécrire en (ly.lx.e)y. Cette b-réduction inverse s'effectue sur toutes les variables libres de e.
Cette transformation ne s'appliquera qu'aux expressions contenant des déclarations locales (let ...in ...) de la manière suivante :

Pour chaque variable libre d'une déclaration locale de fonction, on ajoute un argument à la fonction (par lamb da abstraction). Les noms de fonctions sont traités comme des fonctions et ne nécessitent pas d'abstraction.
Chaque application d'une fonction locale f est remplacée par l'application de f à toutes ses variable libres (f est substituée par f x1 ... xn où xi appartient à l'ensemble des variables libres de f). Comme il ne doit pas avoir de conflit de noms, un renommage des variables locales est nécessaire avant le l-lifting.

Par exemple, dans l'expression suivante :

let i = 5 in let rec f x = f (i+i) in f(i*i);;

où la variable i apparaît libre dans la définition de f qui devient après l-lifting :

let i = 5 in let rec f i x = f i (i+i) in f i (i*i);;

A ce moment là, f peut être passée au niveau global :

let rec f i x = f i (i+i);;
let i = 5 in f i (i*i);;

Les dépendances peuvent être plus complexes principalement dans les déclarations locales imbriquées (let in) et les déclarations locales récursives combinées (let rec ... and). L'exemple suivant montre les différentes étapes à la globalisation de déclarations de fonctions récursives combinées :

let a = ... and b = ...
in let rec f x = ... a ... g ...
       and g y = ... b ... f ...
   in ... f ... g ...
;;

a est libre dans f et b l'est dans g. Une première transformation nous donne :

let a = ... and b = ...
in let rec f a x = ... a ... g b ...
       and g b y = ... b ... f a ...
   in ... f a ... g b ...
;;

Mais nous venons d'introduire b dans le corps de f (et a dans g). Nous devons répéter le l-lifting :

let a = ... and b = ...
in let rec f b a x = ... a ... g a b ...
       and g a b y = ... b ... f b a ...
   in ... f b a ... g a b ...
;;

Ce qui permet enfin de déclarer globalement f et g :

let rec f b a x = ... a ... g a b ...;;
let rec g a b y = ... b ... f b a ...;;
let a = ... and b = ...
   in ... f b a ... g a b ...
;;

En fait, plutôt que de répéter les phases de l-lifting, qui sont coûteuses, il est préférable d'analyser les dépendances en une seule passe en indiquant que les dépendances d'une fonction sont celles de son corps, celles de ses déclaration locales et celles des déclaration récursives combinées.