Definitions

Lambda lifting

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.

The term lambda lifting was first introduced by Thomas Johnsson around 1982.

Algorithm

The following algorithm is one way to lambda-lift an arbitrary program in a language which doesn't support closures as first-class objects:

1. Rename the functions so that each function has a unique name.
2. Replace each free variable with an additional argument to the enclosing function, and pass that argument to every use of the function.
3. Replace every local function definition that has no free variables with an identical global function.
4. Repeat steps 2 and 3 until all free variables and local functions are eliminated.

If the language has closures as first-class objects that can be passed as arguments or returned from other functions (closures), the closure will need to be represented by a data structure that captures the bindings of the free variables.

Example

Consider the following OCaml program that computes the sum of the integers from 1 to 100:

let rec sum n =

` if 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 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`
and sum n =
` if 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 ...)))`