Misplaced Pages

Revision as of 07:39, 4 November 2013

Lambda lifting 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.

Lambda lifting is not the same as closure conversion. Lambda lifting requires all call sites to be adjusted (adding extra arguments to calls) and does not introduce a closure for the lifted lambda expression. In contrast, closure conversion does not require call sites to be adjusted but does introduce a closure for the lambda expression mapping free variables to values.

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, the closure will need to be represented by a data structure that captures the bindings of the free variables.

Example

The following OCaml program 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 lambda abstraction which is a sub expression of a lambda expression and replaces it by a function call (application) to a function that it creates. The free variables in the sub expression are the parameters to the function call. The process is similar to refactoring out code and putting it in a function. Lambda Lifts may be repeated until the expression has no lambda abstractions.

The purpose of lambda lifting

Lambda lifting converts a program with lambda expressions into a program with function calls only. Function calls may be implemented using a stack based implementation, which is simple and efficient.

However a stack based implementation must be strict. A functional language is normally implemented using a lazy strategy, which delays calculation until the value is needed. The lazy implementation strategy gives flexibility to the programmer.

Also Lamba lifting is O(n 2) on processing time for the compiler.

Lambda lifting gives a direct translation of a Lambda calculus program into a functional program. At first site this would indicate the soundness of Lambda calculus as a deductive system. However this is not the case as the eta reduction used in Lambda lifting is the step that introduces cardinality problems into the Lambda calculus, because it removes the value from the variable, without first checking that there is only one value that satisfies the conditions on the variable.

Lambda lifting is useful in understanding the relationship between function definitions and lambda expressions.

Lamba-Lift transform of a lambda expression to functions

This meta-function lambda-lift-tran transforms any lambda expression into a set of functions defined without lambda abstractions. For example,

${\displaystyle \operatorname {lambda-lift-tran} \equiv \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p}$

A meta-function is a function that takes a program as a parameter. The program is data for the meta-program. The program and the meta program are at different meta-levels.

The following conventions will be used to distinguish program from the meta program,

• Square brackets will be used to represent function application in the meta program.
• Capital letters will be used for variables in the meta program. Lower case letters represent variables in the program.
• ${\displaystyle \equiv }$ will be used for equals in the meta 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 the function 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 the lambda-lift meta function, described in the next section,

• ${\displaystyle \operatorname {lambda-lift-tran} =\operatorname {lambda-process} ]}$
• ${\displaystyle {\text{if }}\operatorname {candidate-prefix-lambda} {\text{ then }}}$

${\displaystyle \operatorname {lambda-process} =\operatorname {lambda-process} ]}$

${\displaystyle {\text{ else }}}$

${\displaystyle \operatorname {lambda-process} =L}$

Rules for Lambda lifting

The lambda-lift meta function performs a single lambda lift, which takes an expression and replaces it with a function call.

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 H). Make sure that the name identified by H has not been used.
• Add parameters to H, for all the free variables in S, to create an expression G (see make-call).

The lambda lift is the substitution of an expression for function application, along with the addition of a definition for the function.

${\displaystyle \operatorname {lambda-lift} \equiv \operatorname {let} F\land \operatorname {de-lambda} \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.

In the above rule G is the function application that is substituted for the expression S. It is defined by,

${\displaystyle G=\operatorname {make-call} ]}$

where H is the function name, and FV returns a set of variables that are free in the expression. H must be a new variable, i.e. a name not already used in the lambda expression,

${\displaystyle H\not \in \operatorname {vars} }$

where ${\displaystyle \operatorname {vars} }$ is a meta function that returns the set of variables used in E.

For example,

${\displaystyle F=true}$

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

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

${\displaystyle G=p\ f}$

${\displaystyle \operatorname {de-lambda} \equiv p\ f\ x=f\ (x\ x)}$

gives,

${\displaystyle \operatorname {lambda-lift} \equiv \operatorname {let} p\ f\ x=f\ (x\ x)\operatorname {in} \lambda f.(p\ f)\ (p\ f)}$

Constructing the call

The function call G is constructed by adding parameters for each variable in the free variable set (represented by V), to the function H,

• ${\displaystyle X\in V\to \operatorname {make-call} \equiv \operatorname {make-call} \ X}$
• ${\displaystyle \operatorname {make-call} \equiv H}$

For example,

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

${\displaystyle \operatorname {FV} (S)=\{f\}}$

${\displaystyle G\equiv \operatorname {make-call} ]\equiv \operatorname {make-call} \equiv \operatorname {make-call} \ f\equiv p\ f}$

Eta reductions to remove lambda abstractions in lifted expressions

An eta reduction is ,

${\displaystyle \operatorname {eta-redex} =f}$

If you assume that the eta-redex of an expression equals the expression, this can be rearranged as,

${\displaystyle f\ x=y\iff f=\lambda x.y}$

The de-lambda meta function applies eta-reductions to remove lambda abstractions. It is defined by,

${\displaystyle \operatorname {de-lambda} \equiv \operatorname {de-lambda} }$

${\displaystyle \operatorname {de-lambda} \equiv K=E}$ if E is not a lamba abstraction

For example,

${\displaystyle \operatorname {de-lambda} \equiv \operatorname {de-lambda} \equiv p\ f\ x=f\ (x\ x)}$

Candidate prefix lambda for lifting

The candidate-prefix-lambda is a meta function that returns a lambda abstraction within an expression whose body does not contain any lambda abstractions. The lambda abstraction may have a number of parameters, as they can be removed by the de-lambda meta function defined previously.

The rules are described below,

• ${\displaystyle \operatorname {candidate-prefix-lambda} =\operatorname {lambda-prefix} }$
• ${\displaystyle {\text{if }}\operatorname {lambda-prefix} \equiv R{\text{ then }}}$

${\displaystyle \operatorname {lambda-prefix} }$

${\displaystyle {\text{ else }}}$

${\displaystyle \operatorname {lambda-prefix} }$

• ${\displaystyle {\text{if }}\operatorname {lambda-prefix} {\text{ then }}}$

${\displaystyle \operatorname {lambda-prefix} }$

${\displaystyle {\text{ else }}}$

${\displaystyle \operatorname {lambda-prefix} \iff \operatorname {lambda-prefix} }$

• ${\displaystyle \neg \operatorname {lambda-prefix} }$ where x is a variable.

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\ }$

Because ${\displaystyle p}$ is a global function, the result could also have been written,

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

This would be generated if there was a change to make-call so that only free variables that are not global are added as parameters. More sophisticated versions of the lambda lifting algorithm exist that have processing time O(n 2), and derive the minimum set of parameters required.

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

Any "let" expression with function definitions may be transformed into Lambda calculus, and then beta and eta reductions may be performed to restructure them to remove the effect of the lambda lift.

Conversion between let and lambda expression

A let expression may be converted back into a lambda expression by repeated application of the lambda-param and the lambda-equiv law,

Name	Law
lambda-param	${\displaystyle f\ x=y\equiv f=\lambda x.y}$
lambda-equiv	${\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)}$ (where f is a variable name).

These two laws may be used to convert the function expression back into lambda calculus. The resulting lambda expression keeps the restructuring performed by the lambda lift. All the lambda abstractions are applied to a core expression which is free of lambda abstractions.

Beta and Eta reductions may then be applied to undo the effect of the lambda lift.

Lamba-abstract transform of a function definition to lambda expression

This meta-function lambda-abstract transforms an expression defined using functions with a let expression to a lambda expression. The transformation works when the let condition is structured like a series of functions, but does not work for arbitrary expressions.

For example,

${\displaystyle \operatorname {lambda-abstract} \equiv (\lambda q.(\lambda p.q\ p)\ \lambda f.\lambda x.f\ (x\ x))\ \lambda p.\lambda f.(p\ f)\ (p\ f)}$

First the lambda expression for each function name is found. Then the function name is replaced by the expression in the body of the let.

• ${\displaystyle \operatorname {lambda-abstract} =\operatorname {lambda-convert} ]]}$

Split into separate lets,

• ${\displaystyle \operatorname {lambda-preprocess} =\operatorname {let} A\operatorname {in} \operatorname {lambda-preprocess} }$
• ${\displaystyle \operatorname {lambda-preprocess} =\operatorname {let} A\operatorname {in} E]}$

Turn functions into lambdas,

• ${\displaystyle \operatorname {lambda-process} =\operatorname {lambda-process} }$
• ${\displaystyle \operatorname {lambda-process} =\operatorname {let} \operatorname {abstract} \operatorname {in} \operatorname {lambda-process} }$
• ${\displaystyle \operatorname {lambda-process} =E}$ - E is not a let expression.

Turn lets into lambdas,

• ${\displaystyle \operatorname {lambda-convert} =(\lambda F.E)\ (\operatorname {lambda-convert} )}$
• ${\displaystyle \operatorname {lambda-convert} =E}$ - E is not a let expression.

Note there are some let expressions that cannot be converted into lambda expressions.

Lambda expression for a function

The abstract meta function removes parameters from functions using lambda abstractions. It is defined by,

${\displaystyle \operatorname {abstract} \equiv \operatorname {abstract} }$

${\displaystyle \operatorname {abstract} \equiv K=E}$ if K is a variable.

For example,

${\displaystyle \operatorname {abstract} \equiv \operatorname {abstract} \equiv \operatorname {abstract} \equiv \lambda f.\lambda x.f\ (x\ x)}$

Example

Starting with the function definition of the Y-combinator,

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

Transformation	Expression
	${\displaystyle \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p\ }$
lambda-param * 4	${\displaystyle \operatorname {let} p=\lambda f.\lambda x.f\ (x\ x)\land q=\lambda p.\lambda f.(p\ f)\ (p\ f)\operatorname {in} q\ p}$
lambda-equiv	${\displaystyle \operatorname {let} q=\lambda p.\lambda f.(p\ f)\ (p\ f)\operatorname {in} (\lambda p.q\ p)\ (\lambda f.\lambda x.f\ (x\ x))}$
lambda-equiv	${\displaystyle \operatorname {let} true\operatorname {in} (\lambda q.(\lambda p.q\ p)\ (\lambda f.\lambda x.f\ (x\ x)))\ (\lambda p.\lambda f.(p\ f)\ (p\ f))}$
drop let	${\displaystyle (\lambda q.(\lambda p.q\ p)\ (\lambda f.\lambda x.f\ (x\ x)))\ (\lambda p.\lambda f.(p\ f)\ (p\ f))}$

The expression is now a lambda abstraction for the variable q, applied to a lambda abstraction for the variable q, applied to the expression ${\displaystyle q\ p}$. This expression is still structured with the lambda abstractions lifted to define global variables.

Beta and eta reductions may then be used to return the function to its original structure.

Transformation	Expression
beta-redex	${\displaystyle \lambda p.((\lambda p.\lambda f.(p\ f)\ (p\ f))\ p)\ (\lambda f.\lambda x.f\ (x\ x))}$
eta-redex	${\displaystyle \lambda p.(\lambda f.(p\ f)\ (p\ f))\ (\lambda x.\lambda f.f\ (x\ x))}$
beta-redex	${\displaystyle \lambda f.((\lambda f.\lambda x.f\ (x\ x))\ f)\ ((\lambda f.\lambda x.f\ (x\ x))\ f)}$
eta-redex * 2	${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

Which gives back the Y combinator,

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

See also

• Supercombinator

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.
2. Johnsson, Thomas (1985), "Lambda Lifting: Transforming Programs to Recursive Equations", Conf. on Func. Prog. Languages and Computer Architecture., ACM Press
3. Optimal Lambda Lifting in Quadratic Time, pp. pp 37-56, doi:10.1007/978-3-540-85373-2_3, ISBN 978-3-540-85372-5 {{citation}}: |pages= has extra text (help); Cite has empty unknown parameter: |1= (help); Unknown parameter |booktitle= ignored (help)

External links

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

• Implementation of functional programming languages
• Lambda calculus