Misplaced Pages

Revision as of 11:30, 17 July 2013

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 contexts into a fixed set of top-level functions with an extra parameter replacing each local variable. By eliminating the need for run-time access-links, this may reduce the run-time cost of handling implicit scope. Many functional programming language implementations use lambda lifting during compilation.

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

The reverse operation is called lambda dropping.

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 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

The following is the same example, this time written in JavaScript:

// Initial version
function sum (n) {
    function f (x) {
        return n + x;
    }
    if (n == 1) {
        return 1;
    }
    else {
        return f( sum(n - 1) );
    }
}
// After converting the free variable n to a formal parameter w
function sum (n) {
    function f (w, x) {
        return w + x;
    }
    if (n == 1) {
        return 1;
    }
    else {
        return f( n, sum(n - 1) );
    }
}
// After lifting function f into the global scope
function f (w, x) {
    return w + x;
}
function sum (n) {
    if (n == 1) {
        return 1;
    }
    else {
        return f( n, sum(n - 1) );
    }
}

Lambda Lifting in Lambda calculus

This section describes lambda lifting in more detail, and describes the process when used in Lambda Calculus. Lambda lifting may be used to convert a program written in Lambda Calculus into a functional program, without lambdas. This demonstrates the equivalence of programs written in Lambda Calculus and programs written as functions.

Each Lambda Lift takes a sub expression of a lambda expression and replaces it by a function call (application) to a function that it creates. The process is similar to refactoring out some code and putting it in a function. Lambda Lifts may be repeated until the lambda expression is completely converted.

Rules for Lambda Lifting

This section describes how to lift and export one lambda expression to a function definition.

The lift is given a sub-expression (called S) to be lifted. For S;

• Create a name for the function that will replace S (called f). Make sure that the name identified by f has not been used.
• Add parameters to f, for all the free variables in S, to create an expression g (see make-call).

The lift is also given a "let" expression, A "let" expression is an expression used in functional languages to represent a number of conditions that are true in interpreting an expression. It is used here to represent conditions true on a lambda expression. For example,

${\displaystyle \operatorname {let} F\operatorname {in} L}$

where

• F is function definitions.
• L is a lambda expression.

The lambda-lift is implemented in the rule below.

${\displaystyle (f\not \in \operatorname {vars} )\land (g=\operatorname {make-call} ])\to (\operatorname {lambda-lift} =\operatorname {let} F\land g=S\operatorname {in} L)}$

The new lambda expression has S substituted for g. Note that L means substitution of S for g in L. The function definitions has the function definition g = S added.

The two rules below show how to construct a function call (or application) out of a function name f by adding parameters for each variable in the free variable set (represented by V),

• ${\displaystyle x\in V\to \operatorname {make-call} =\operatorname {make-call} \ x}$
• ${\displaystyle \operatorname {make-call} =f}$

The set of variables already used in ${\displaystyle \operatorname {let} F\operatorname {in} L}$ is represented by,

${\displaystyle \operatorname {vars} }$

The expression S will usually have leading lambdas. These may be moved to the other side of the equation as parameters using the rule;

• ${\displaystyle (f=\lambda x.y)\equiv (fx=y)}$

Lamba-Lift transform of a lambda expression to functions

This section describes the process of performing a sequence of lifts to convert any lambda expression into an equivalent functional program.

Calling lambda-lift-tran on a lambda expression gives you a functional program in the form,

• let M in N

where M is a series of function definitions, and N is the expression representing the value returned.

The processing of transforming the lambda expression is a series of lifts. Each lift has,

1. A sub expression chosen for it by candidate-prefix-lambda. The sub expression should be chosen so that it may be converted into an equation with no lambdas.
2. The lift is performed by a call to lambda-lift as described in the previous section,

• ${\displaystyle \operatorname {lambda-lift-tran} =\operatorname {lambda-lift-process} ]}$
• ${\displaystyle \operatorname {candidate-prefix-lambda} \to \operatorname {lambda-lift-process} =\operatorname {lambda-lift-process} ]}$
• ${\displaystyle \neg \operatorname {candidate-prefix-lambda} \to \operatorname {lambda-lift-process} =L}$

Candidate prefix lambda for lifting

The expression to be lifted must be chosen so that the equation created may be converted into an equation without lambdas using the rule,

• ${\displaystyle (f=\lambda x.y)\equiv (fx=y)}$

The expression may have any number of lamdas prefixed at the start, but in the body of the expression, must have no lambda abstractions. This is achieved by looking for the deepest lambda prefix in the expression.

The rules are described below,

• ${\displaystyle \operatorname {candidate-prefix-lambda} ]=\operatorname {lambda-prefix} }$

to be completed

Conversion between let and lambda expression

A let expression may be converted back into a lambda expression by repeated application of the following law,

${\displaystyle f\not \in FV(F)\to (\operatorname {let} f=e\land F\operatorname {in} L\equiv \operatorname {let} F\operatorname {in} \lambda f.L\ e)}$

The result has the lift restructure, but the restructure is within the Lambda Calculus.

Example

For example the Y combinator,

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

	Lambda Expression	Function	From	To	Variables
1	${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$	true	${\displaystyle \lambda x.f\ (x\ x)}$	${\displaystyle p\ f}$	${\displaystyle \{x,f\}}$
2	${\displaystyle (\lambda f.(\lambda x.f\ (x\ x))(\lambda x.f\ (x\ x)))}$	${\displaystyle p\ f=\lambda x.f\ (x\ x)}$			${\displaystyle \{x,f,p\}}$
3	${\displaystyle \lambda f.(p\ f)\ (p\ f)}$	${\displaystyle p\ f\ x=f\ (x\ x)}$	${\displaystyle \lambda f.(p\ f)\ (p\ f)}$	${\displaystyle q\ p}$	${\displaystyle \{x,f,p\}}$
4	${\displaystyle \lambda f.(p\ f)\ (p\ f)}$	${\displaystyle p\ f\ x=f\ (x\ x)\land q\ p=\lambda f.(p\ f)\ (p\ f)}$			${\displaystyle \{x,f,p,q\}}$
5	${\displaystyle q\ p}$	${\displaystyle p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)}$			${\displaystyle \{x,f,p,q\}}$

The first sub expression to be chosen for lifting is ${\displaystyle \lambda x.f\ (x\ x)}$. This transforms the lambda expression into ${\displaystyle \lambda f.(p\ f)\ (p\ f)}$ and creates the equation ${\displaystyle p\ f\ x=f(x\ x)}$.

The second sub expression to be chosen for lifting is ${\displaystyle \lambda f.(p\ f)\ (p\ f)}$. This transforms the lambda expression into ${\displaystyle q\ p}$ and creates the equation ${\displaystyle q\ p\ f=(p\ f)\ (p\ f)}$.

And the result is,

${\displaystyle \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p\ }$

Execution

Apply function to,

${\displaystyle K}$

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\ K}$	${\displaystyle \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p\ \ K}$
${\displaystyle (\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))}$	${\displaystyle \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} p\ K\ (p\ K)}$
${\displaystyle K\ ((\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))))\ }$	${\displaystyle \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=p\ f\ (p\ f)\operatorname {in} K\ (p\ K\ (p\ K))}$

So,

• ${\displaystyle (\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))=K\ ((\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))))\ }$

or

• ${\displaystyle p\ K\ (p\ K)=K\ (p\ K\ (p\ K))}$

The Y-Combinator calls its paramter (function) repeatedly on itself. The value is defined if the function has a fixed point. But the function will never terminate.

Lambda dropping in Lambda Calculus

References

1. Attention: This template ({{cite doi}}) is deprecated. To cite the publication identified by doi:10.1145/258994.259007, please use {{cite journal}} (if it was published in a bona fide academic journal, otherwise {{cite report}} with |doi=10.1145/258994.259007 instead.

See also

• Supercombinator

External links

• Lambda Lifting: Transforming Programs to Recursive Equations
• Explanation on Stack Overflow, with a JavaScript example

• Implementation of functional programming languages
• Lambda calculus