Lambda lifting
From Wikipedia, the free encyclopedia
Lambda lifting is the process of eliminating free variables and local function definitions from a computer program. Eliminating these local definitions removes the need for implicit scope and allows a compiler to generate a fixed set of substitution (or rewriting) rules for executing the program. Many functional programming language implementations treat a program as a set of rewriting rules at runtime, so they must incorporate lambda lifting into their compilation process.
[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 program that computes the sum of the integers from 1 to 100:
letrec sum n = if equal n 1
then 1
else (let f x = n + x in f (sum (n - 1))) in
sum 100
(The word letrec 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:
letrec 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:
letrec f w x = w + x in
letrec 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 ...)))
