Lambda lifting
From Wikipedia, the free encyclopedia
Lambda lifting or closure conversion is the process of eliminating free variables from local function definitions from a computer program. The elimination of free variables allows the compiler to hoist local definitions out of their surrounding context into a fixed set of closed global functions (or rewriting rules). This removes the need for implicit scope for executing the program. Many functional programming language implementations use lambda lifting during compilation.
[edit] Algorithm
The following algorithm is one way to lambda-lift an arbitrary program:
- Rename the functions so that each function has a unique name.
- Replace each free variable with an additional argument to the enclosing function, and pass that argument to every use of the function.
- Replace every local function definition that has no free variables with an identical global function.
- Repeat steps 2 and 3 until all free variables and local functions are eliminated.
[edit] Example
Consider the following OCaml program that computes the sum of the integers from 1 to 100:
let rec sum n = if equal n 1
then 1
else (let f x = n + x in f (sum (n - 1))) in
sum 100
(The word let rec declares sum as a function that may call itself.) The function f, which adds sum's argument to the sum of the numbers less than the argument, is a local function. Within the definition of f, n is a free variable. Start by converting the free variable to an argument:
let rec sum n = if equal n 1
then 1
else (let f w x = w + x in f n (sum (n - 1))) in
sum 100
Next, lift f into a global function:
let rec f w x = w + x in
let rec sum n = if equal n 1
then 1
else f n (sum (n - 1)) in
sum 100
Finally, convert the functions into rewriting rules:
f w x → w + x sum 1 → 1 sum n → f n (sum (n - 1)) when n ≠ 1
The expression "sum 100" rewrites as:
sum 100 → f 100 (sum 99) → 100 + (sum 99) → 100 + (f 99 (sum 98)) → 100 + (99 + (sum 98) . . . → 100 + (99 + (98 + (... + 1 ...)))
