Lambda Lifting Article Index for
Lambda
Website Links For
Lambda
 

Information About

Lambda Lifting





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.


EXAMPLE

Consider the following program that computes the sum of numbers 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 ...)))


EXTERNAL LINKS