Lambda lifting

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) );
    }
}

Conversion without lifting

The let expression, is useful in describing lifting and dropping, and in describing the relationship between recursive equations and lambda expressions. The "let" expression is present in many functional languages to allow the local definition of expression, for use in defining another expression. The "let" expression may be generalized slightly to allow equations to be used in defining the local expression. A let expression then looks like,

$\operatorname {let} f:E\operatorname {in} L$

where,

f is a variable name, where f has a local scope.

E is a Boolean expression.

L is a Lambda expression.

The following rules describe the equivalence of lambda and let expressions,

Name	Law
lambda-param	$f\ x=y\equiv f=\lambda x.y$
lambda-let	$\operatorname {let} f:f=E\operatorname {in} L\equiv \lambda f.L\ E)$ (where f is a variable name).
let-let	$f\not \in FV(F)\to (\operatorname {let} f:f=e\land F\operatorname {in} L\equiv \operatorname {let} F\operatorname {in} \operatorname {let} f:f=e\operatorname {in} L)$ (where f is a variable name).

Meta-functions will be given that describe the conversion between lambda and let expressions. 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.
• $\equiv$ will be used for equals in the meta program.

For simplicity the first rule given that matches will be applied.

Conversion from Lambda to Let expressions

The following rules describe how to convert from a Lambda expression to a let expresion, without altering the structure.

1. $\operatorname {de-lambda} [(\lambda F.E)L]\equiv \operatorname {let-combine} [\operatorname {let} F:\operatorname {de-lambda} [F=L]\operatorname {in} E]$
2. $V\not \in \operatorname {FV} [\lambda F.E]\to \operatorname {de-lambda} [\lambda F.E]\equiv \operatorname {let-combine} [\operatorname {let} V:\operatorname {de-lambda} [V\ F=E]\operatorname {in} V]$
3. $\operatorname {de-lambda} [M\ N]\equiv \operatorname {de-lambda} [M]\ \operatorname {de-lambda} [N]$
4. $\operatorname {de-lambda} [V]\equiv V$
5. $\operatorname {de-lambda} [F=\lambda P.E]\equiv \operatorname {de-lambda} [F\ P=E]$
6. $\operatorname {de-lambda} [E=F]\equiv \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]$
7. $V\neq W\to \operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]\equiv \operatorname {let} V,W:E\land F\operatorname {in} G$
8. $\operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} F]\equiv \operatorname {let} V:E\operatorname {in} F$

For example the Y combinator,

$\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$

Rule	Lambda Expression
2	$\operatorname {de-lambda} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]$
6, 3	$\operatorname {let} p:\operatorname {de-lambda} [p\ f=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\operatorname {in} p$
2	$\operatorname {let} p:p\ f=\operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\operatorname {in} p$
1	$\operatorname {let} p:p\ f=\operatorname {let} x:\operatorname {de-lambda} [x=\lambda q.f\ (q\ q)]\operatorname {in} f\ (x\ x)\operatorname {in} p$
5	$\operatorname {let} p:p\ f=\operatorname {let} x:\operatorname {de-lambda} [x\ q=f\ (q\ q)]\operatorname {in} f\ (x\ x)\operatorname {in} p$
6, 3	$\operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)\operatorname {in} p$

Conversion from Let to Lambda expressions

These rule reverse the conversion described above. They convert from a let expression to a Lambda expresion, without altering the structure. Not all let expressions may be converted using these rules.

1. $\operatorname {de-let} [\operatorname {let} F:G\operatorname {in} F]\equiv \operatorname {get-lambda} [F,G]=$
2. $\operatorname {de-let} [\operatorname {let} F:G\operatorname {in} E]\equiv (\lambda F.\operatorname {de-let} [E])\ \operatorname {get-lambda} [F,G]=$
3. $\operatorname {de-let} [\lambda V.E]\equiv \lambda V.\operatorname {de-let} [E]$
4. $\operatorname {de-let} [M\ N]\equiv \operatorname {de-let} [M]\ \operatorname {de-let} [N]$
5. $\operatorname {de-let} [V]\equiv V$
6. $\operatorname {get-lambda} [F,G\ V=E]=\operatorname {get-lambda} [F,G=\lambda V.E]$
7. $\operatorname {get-lambda} [F,F=E]=\operatorname {de-let} [E]$
8. $W\not \in \operatorname {FV} [E]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\operatorname {in} G]\equiv \operatorname {de-let} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]$

For example the let expression obtained from the Y combinator,

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

Rule	Lambda Expression
1	$\operatorname {de-let} [\operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)\operatorname {in} p]$
6	$\operatorname {get-lambda} [p,p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)]$
7	$\operatorname {get-lambda} [p,p=\lambda f.\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)]$
3	$\operatorname {de-let} [\lambda f.\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)]$
2, 4, 5	$\lambda f.\operatorname {de-let} [\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)]$
6	$\lambda f.(\lambda x.f\ (x\ x))\ \operatorname {get-lambda} [x,x\ q=f\ (q\ q)]$
7	$\lambda f.(\lambda x.f\ (x\ x))\ \operatorname {get-lambda} [x,x=\lambda q.f\ (q\ q)]$
3, 4, 5	$\lambda f.(\lambda x.f\ (x\ x))\ \operatorname {de-let} [\lambda q.f\ (q\ q)]$
	$\lambda f.(\lambda x.f\ (x\ x))\ (\lambda q.f\ (q\ q))$

For a second example take the lifted version of the Y combinator, derived in Lambda Lifting

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

Rule	Lambda Expression
8	$\operatorname {de-let} [\operatorname {let} p,q:p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p]$
2	$\operatorname {de-let} [\operatorname {let} p:p\ f\ x=f\ (x\ x)\operatorname {in} \operatorname {let} q:q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p]$
6, 7	$(\lambda p.\operatorname {de-let} [\operatorname {let} q:q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p])\ \operatorname {get-lambda} [p,p\ f\ x=f\ (x\ x)]$
2, 4, 5	$(\lambda p.\operatorname {de-let} [\operatorname {let} q:q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p])\ \lambda f.\lambda x.f\ (x\ x)$
6, 7	$(\lambda p.(\lambda q.q\ p)\ \operatorname {get-lambda} [q,q\ p\ f=(p\ f)\ (p\ f)])\ \lambda f.\lambda x.f\ (x\ x)$
	$(\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)$

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 an efficient implementation of 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,

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

The algorithm described here regards every abstraction as an anonymous function. This transformation names the anonymous function and lifts. Alternative approaches are possible. A lambda abstraction applied to an expression may be regarded as a local function definition.

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.
• $\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,

• $\operatorname {lambda-lift-tran} [L]=\operatorname {lambda-process} [\operatorname {let} \operatorname {true} \operatorname {in} L]]$
• ${\text{if }}\operatorname {candidate-prefix-lambda} [S,L]{\text{ then }}$

$\operatorname {lambda-process} [L]=\operatorname {lambda-process} [\operatorname {lambda-lift} [S,L]]$

${\text{ else }}$

$\operatorname {lambda-process} [L]=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.

$\operatorname {lambda-lift} [S,\operatorname {let} F\operatorname {in} L]\equiv \operatorname {let} F\land \operatorname {de-lambda} [G=S]\operatorname {in} L[S:=G]$

The new lambda expression has S substituted for G. Note that L[S:=G] 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,

$G=\operatorname {make-call} [H,\operatorname {FV} [S]]$

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,

$H\not \in \operatorname {vars} [\operatorname {let} F\operatorname {in} L]$

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

For example,

$F=true$

$L=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$

$S=\lambda x.f\ (x\ x)$

$G=p\ f$

$\operatorname {de-lambda} [p\ f=\lambda x.f\ (x\ x)]\equiv p\ f\ x=f\ (x\ x)$

gives,

$\operatorname {lambda-lift} [\lambda x.f\ (x\ x),\operatorname {let} true\operatorname {in} \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\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,

• $X\in V\to \operatorname {make-call} [H,V]\equiv \operatorname {make-call} [H,V\cap \neg \{X\}]\ X$
• $\operatorname {make-call} [H,\{\}]\equiv H$

For example,

$S=\lambda x.f\ (x\ x)$

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

$G\equiv \operatorname {make-call} [p,\operatorname {FV} [S]]\equiv \operatorname {make-call} [p,\{f\}]\equiv \operatorname {make-call} [p,\{\}]\ f\equiv p\ f$

Eta reductions to remove lambda abstractions in lifted expressions

An eta reduction is ,

$\operatorname {eta-redex} [\lambda x.(f\ x)]=f$

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

$f\ x=y\iff f=\lambda x.y$

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

$\operatorname {de-lambda} [F=\lambda X.Y]\equiv \operatorname {de-lambda} [F\ X=Y]$

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

For example,

$\operatorname {de-lambda} [p\ f=\lambda x.f\ (x\ x)]\equiv \operatorname {de-lambda} [p\ f\ x=f\ (x\ x)]\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,

• $\operatorname {candidate-prefix-lambda} [S,L]=\operatorname {lambda-prefix} [S,L,\_]$
• ${\text{if }}\operatorname {lambda-prefix} [S,Y,R]\equiv R{\text{ then }}$

$\operatorname {lambda-prefix} [\lambda X.Y,\lambda X.Y,true]$

${\text{ else }}$

$\operatorname {lambda-prefix} [S,\lambda X.Y,false]$

• ${\text{if }}\operatorname {lambda-prefix} [S,X,R]{\text{ then }}$

$\operatorname {lambda-prefix} [S,X\ Y,false]$

${\text{ else }}$

$\operatorname {lambda-prefix} [T,Y,R]\iff \operatorname {lambda-prefix} [T,X\ Y,false]$

• $\neg \operatorname {lambda-prefix} [\_,X,false]$ where x is a variable.

Example

For example the Y combinator,

$\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$

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

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

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

And the result is,

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

Because $p$ is a global function, the result could also have been written,

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

$K$

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

So,

• $(\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))=K\ ((\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))))\$

or

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

Lambda dropping is making the scope of functions smaller and using the context from the reduced scope to reduce the number of variables. Reducing the number of variables makes functions easier to comprehend.

Lambda dropping also may make the compilation of programs quicker for the compiler, and may also increase the efficiency of the resulting program, by reducing the number of parameters, and reducing the size of stack frames.

However Lambda dropping also makes a function harder to re-use. A dropped function is tied to its context, and can only be used in a different context if it is first lifted.

In the Lambda Lifting section, a meta function for first lifting and then converting the resulting lambda expression into recursive equation was described. The Lamda Drop meta function performs the reverse by first converting recursive equations to lambda abstractions, and then dropping the resulting lambda expression, into the smallest scope which covers all references to the lambda abstraction.

Rules used in Lambda dropping

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	$f\ x=y\equiv f=\lambda x.y$
lambda-equiv	$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).

Converting equations to lambda expressions

This meta-function lambda-abstract-tran 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.

The lambda-lift-tran meta function described earlier creates "let" expressions where each function definition has no free variables. lambda-abstract-tran needs functions with no free variables to work correctly.

For example,

$\operatorname {lambda-abstract-tran} [\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p]\equiv (\lambda q.(\lambda p.q\ p)\ (\lambda f.\lambda x.f\ (x\ x)))\ (\lambda p.\lambda f.(p\ f)\ (p\ f))$

lambda-abstract-tran is defined as,

• $\operatorname {lambda-abstract-tran} [E]=\operatorname {lambda-convert} [\operatorname {lambda-process} [\operatorname {lambda-preprocess} [E]]]$

Lambda abstract performs three separate processing steps; pre-process, process, and convert. These steps are described below,

Pre-process - Split into separate lets,

• $\operatorname {lambda-preprocess} [\operatorname {let} A\land B\operatorname {in} E]=\operatorname {let} A\operatorname {in} \operatorname {lambda-preprocess} [A,\operatorname {let} B\operatorname {in} E]$
• $\operatorname {lambda-preprocess} [\operatorname {let} A\operatorname {in} E]=\operatorname {let} A\operatorname {in} E$

After lambda-preprocess the result for the example is,,

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

Process - Turn functions into lambdas,

• $\operatorname {lambda-process} [\operatorname {let} true\operatorname {in} E]=\operatorname {lambda-process} [E]$
• $\operatorname {lambda-process} [\operatorname {let} G=S\operatorname {in} E]=\operatorname {let} \operatorname {abstract} [G=S]\operatorname {in} \operatorname {lambda-process} [E]$
• $\operatorname {lambda-process} [E]=E$ ..... Use this case when E is not a let expression.

After lambda-process,

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

Convert - Turn lets into lambdas,

• $\operatorname {lambda-convert} [\operatorname {let} F=S\operatorname {in} E]=(\lambda F.E)\ (\operatorname {lambda-convert} [S])$
• $\operatorname {lambda-convert} [E]=E$ ..... Use this case when E is not a let expression.

Then after lambda-abstract-tran,

$(\lambda p.(\lambda q.q\ p)\ (\lambda p.\lambda f.(p\ f)\ (p\ f)))\ (\lambda f.\lambda x.f\ (x\ x))$

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

$\operatorname {abstract} [FX=Y]\equiv \operatorname {abstract} [F=\lambda X.Y]$

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

For example,

$\operatorname {abstract} [p\ f\ x=f\ (x\ x)]\equiv \operatorname {abstract} [p\ f=\lambda x.f\ (x\ x)]\equiv \operatorname {abstract} [p=\lambda f.\lambda x.f\ (x\ x)]\equiv \lambda f.\lambda x.f\ (x\ x)$

Abstraction Sinking

Abstraction sinking is moving abstractions so that they have the smallest scope that covers the references to the abstraction variable. Lambda-drop-tran converts recursive equations to lambda expression, and then sinks the resulting abstractions.

$\operatorname {lambda-drop-tran} [L]=\operatorname {drop-params-tran} [\operatorname {sink-tran} [\operatorname {rename} [\operatorname {lambda-abstract-tran} [L]]]]$

rename is a meta function to give all the abstractions distinct names. This step is important because in the renaming steps, the name will be used to identify an abstraction.

sink-tran sinks each abstraction, starting from the innermost,

$\operatorname {sink-tran} [(\lambda X.B)\ Y]=\operatorname {sink} [(\lambda X.\operatorname {sink-tran} [B])\ \operatorname {sink-tran} [Y]]]$

$\operatorname {sink-tran} [\lambda X.B]=\lambda X.\operatorname {sink-tran} [B]$

$\operatorname {sink-tran} [M\ N]=\operatorname {sink-tran} [M]\ \operatorname {sink-tran} [M]$

$\operatorname {sink-tran} [V]=V$

Sinking is moving a lambda abstraction inwards as far as possible such that it is still outside all references to the variable.

Application - 4 cases.

$X\not \in \operatorname {FV} [G]\land X\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda X.G\ H)\ Y]=G\ H$

$X\not \in \operatorname {FV} [G]\land X\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda X.G\ H)\ Y]=G\ \operatorname {sink} [(\lambda X.H)\ Y]$

$X\in \operatorname {FV} [G]\land X\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda X.G\ H)\ Y]=(\operatorname {sink} [(\lambda X.G)\ Y])\ H$

$X\in \operatorname {FV} [G]\land X\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda X.G\ H)\ Y]=(\lambda X.G\ H)\ Y$

Abstraction - Only 1 case as the names of the lambda abstractions have been made distinct by rename.

$X\neq V\to \operatorname {sink} [(\lambda X.\lambda V.W)\ Y]=\lambda V.\operatorname {sink} [(\lambda X.W)\ Y]$

Variable - 2 cases.

$X\neq V\to \operatorname {sink} [(\lambda X.V)\ Y]=V$

$X=V\to \operatorname {sink} [(\lambda X.V)\ Y]=Y$

For the example above, sinking,

$\operatorname {sink-tran} [\lambda p.(\lambda q.q\ p)\ (\lambda p.\lambda f.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))]$

$=\operatorname {sink} [(\lambda p.\operatorname {sink} [(\lambda q.q\ p)\ (\lambda p.\lambda f.(p\ f)\ (p\ f))])\ (\lambda f.\lambda x.f\ (x\ x))]$

$=\operatorname {sink} [(\lambda p.\operatorname {sink} [(\lambda q.q)\ (\lambda p.\lambda f.(p\ f)\ (p\ f)))\ p])\ (\lambda f.\lambda x.f\ (x\ x))]$

$=\operatorname {sink} [(\lambda p.(\lambda p.\lambda f.(p\ f)\ (p\ f)))\ p)\ (\lambda f.\lambda x.f\ (x\ x))]$

$=(\lambda p.\lambda f.(p\ f)\ (p\ f)))\ \operatorname {sink} [(\lambda p.p)\ (\lambda f.\lambda x.f\ (x\ x))]$

$=(\lambda p.\lambda f.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))$

Sinking a second time,

$\operatorname {sink-tran} [(\lambda p.\lambda f.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))]$

$=\operatorname {sink} [(\lambda p.\lambda f.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))]$

$=\lambda f.\operatorname {sink} [(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))]$

$=\lambda f.(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))$

Parameter Dropping

Parameter dropping is optimizing a function for its position in the function. Lambda lifting added parameters that were necessary so that a function can be moved out of its context. In dropping, this process is reversed, and extra parameters that contain variables that were free may be removed.

Dropping a parameter is removing an unnecessary parameter from a function, where the actual parameter being passed in is always the same expression. The free variables of the expression must also be free where the function is defined. In this case the parameter that is dropped is replaced by the expression in the body of the function definition. This makes the parameter unnecessary.

For example, consider,

$(\lambda g.k\ (\lambda n.(g\ m\ p\ n)\ (g\ q\ p\ n))\ (f\ x))\ \lambda x.\lambda o.\lambda y.o\ x\ y$

In this example the actual parameter for the formal parameter o is always p. As p is a free variable in the whole expression, the parameter may be dropped. The actual parameter for the formal parameter y is always n. However n is bound in a lambda abstraction. So this parameter may not be dropped.

The result of dropping the parameter is,

$\operatorname {drop-params-tran} [(\lambda g.k\ (\lambda n.(g\ m\ p\ n)\ (g\ q\ p\ n))\ (f\ x))\ \lambda x.\lambda o.\lambda y.o\ x\ y]$

$\equiv (\lambda g.k\ (\lambda n.(g\ m\ n)\ (g\ q\ n))\ (f\ x))\ \lambda x.\lambda y.p\ x\ y$

For the main example,

$\operatorname {drop-params-tran} [\lambda f.(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))]$

$\equiv \lambda f.(\lambda p.p\ p)\ (\lambda x.f\ (x\ x))$

The definition of drop-params-tran is,

$\operatorname {drop-params-tran} [L]\equiv (\operatorname {drop-params} [L,D,FV[L],[]])$

where,

$\operatorname {build-param-lists} [L,D,\_]$

Build parameter lists

For each abstraction that defines a function, build the information required to make decisions on dropping names. This information consists of information about each parameter; the parameter name, the expression for the actual value, and an indication that all the expressions have the same value.

For example in,

$(\lambda g.k\ (\lambda n.(g\ m\ p\ n)\ (g\ q\ p\ n))\ (f\ x))\ \lambda x.\lambda o.\lambda y.o\ x\ y$

the parameters to the function g are,

Formal Parameter	All Same Value	Actual parameter expression
x	false	_
o	true	p
y	true	n

Each abstraction is renamed with a unique name, and the parameter list is associated with the name of the abstraction. For example, for g there is the parameter list;

$D[g]=[[x,\operatorname {false} ,\_],[o,\operatorname {true} ,p],[y,\operatorname {true} ,n]]$

build-param-lists builds all the lists for an expression, by traversing the expression.

Abstraction - A lambda expression of the form $(\lambda N.S)\ L$ is analyzed to extract the names of parameters for the function.

$\operatorname {build-param-lists} [(\lambda N.S)\ L,D,R]\equiv \operatorname {build-param-lists} [B,D,R]\land \operatorname {build-list} [L,D[N]]$

Locate the name and start building the parameter list for the name, filling in the formal parameter names. Also receive any actual parameter list from the body of the expression, and return it as the actual parameter list from this expression

$\operatorname {build-list} [\lambda P.B,[X,\_,\_]::L]\equiv \operatorname {param-list} [B,L]$

$\operatorname {param-list} [B,[]]\equiv \operatorname {build-param-lists} [B,R]$

Variable - A call to a function.

$\operatorname {build-param-lists} [N,D,D[N]]$

For a function name or parameter start populating actual parameter list by outputting the parameter list for this name.

Application - An application (function call) is processed to extract parameter information.

$\operatorname {build-param-lists} [E\ P,D,R]\equiv \operatorname {build-param-lists} [E,D,T]\land \operatorname {build-param-lists} [P,D,K]$

$\land (T=[F,S,A]::R\land S\implies \operatorname {equate} [A,P]\land V[F]=A\land K=D[F]\lor T=[]\land R=[])$

Retrieve the parameter lists for the expression, and the parameter. Retrieve a parameter record from the parameter list from the expression, and check that the current parameter value matches this parameter. Record the value for the parameter name for use later in checking.

$\operatorname {equate} [A,N]\equiv A=V[N]\lor A=N$ ... if N is a variable.

$\operatorname {equate} [A,E]\equiv A=E$ ... otherwise.

The logic for equate is used in this more difficult example,

$\lambda f.(\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x))$

has the parameter x dropped to become,

$\lambda f.(\lambda q.f\ (q\ q))\ (\lambda q.f\ (q\ q))$

	function	param 1	param 2
Abstract	p	p	x
Application 1	p	p	f
Application 2	q	q	x

q in the second call has the value of p. For the second parameter, f and x are the same value. This is picked up by using the condition, $A=V[N]$. The condition $K=D[F]$ supports the functions q and p sharing the same parameter list, which is also needed in this example.

Retrieving the "same value" indicator from the parameter lists is a little unusual. The same value indicator is never set to true. It is only set to false if all the values cannot be matched. The value is retrieved by using S to build a set of the Boolean values allowed for S. If true is a member then all the values for this parameter are equal, and the parameter may be dropped.

$\operatorname {ask} [T,S]\equiv T\in \{X:X=S\}$

Drop parameters

Abstraction - Two cases; abstraction with application, abstraction aloe

Abstraction with application. Drop the actual parameters in the body of the abstraction, based on the parameter lists. Also drop lambda abstractions for the parameters in the application of the abstraction.

$\operatorname {drop-params} [(\lambda N.S)\ L,D,V,R]\equiv (\lambda N.\operatorname {drop-params} [S,D,F,R])\ \operatorname {drop-formal} [D[N],L,F,[]]$

where,

$F=FV((\lambda N.S)\ L)$

Abstraction alone. Use this case only if there is no application. Drop parameters in the body of the abstraction based on the parameter lists.

$\operatorname {drop-params} [(\lambda N.S),D,V,R]\equiv (\lambda N.\operatorname {drop-params} [S,D,F,R])$

Variable.

$\operatorname {drop-params} [N,D,V,D[N]]\equiv N$

Application - Two cases; parameter dropped or not dropped. Use this case only when the function expression E is not an abstraction.

$(\operatorname {ask} [\operatorname {true} ,S]\land FV[A]\subset V)\to \operatorname {drop-params} [E\ P,D,V,R]\equiv \operatorname {drop-params} [E,[F,S,A]::R,T]$

$\neg (\operatorname {ask} [\operatorname {true} ,S]\land FV[A]\subset V)\to \operatorname {drop-params} [E\ P,D,V,R]\equiv \operatorname {drop-params} [E,[F,S,A]::R,T]\ \operatorname {drop-params} [P,K]$

Drop formal parameters

drop-formal removes formal parameters, based on the contents of the parameter lists. Its parameters are,

• The parameter list,
• The function definition (lambda abstraction).
• The free variables from the function definition.

drop-formal has 2 cases; parameter dropped, parameter not dropped.

1. $(\operatorname {ask} [\operatorname {true} ,S]\land FV[A]\subset V)\to \operatorname {drop-formal} [[F,S,A]::Z,\lambda F.Y,V]\equiv \operatorname {drop-formal} [[F,S,A]::Z,Y[F:=A],V]$
2. $\neg (\operatorname {ask} [\operatorname {true} ,S]\land FV[A]\subset V)\to \operatorname {drop-formal} [[F,S,A]::Z,\lambda F.Y,V]\equiv \lambda F.\operatorname {drop-formal} [[F,S,A]::Z,Y,V]$
3. $\operatorname {drop-formal} [Z,Y,V]\equiv Y$

Which can be explained as,

1. If all the actual parameters have the same value, and all the free variables of that value are available for definition of the function then drop the parameter, and replace the old parameter with it's value.
2. else do not drop the parameter.
3. else return the body of the function.

For example,

$Z=[[x,\operatorname {false} ,\_],[o,\operatorname {true} ,p],[y,\operatorname {true} ,n]]$

$V=\{k,m,p,q,f,x\}$

Rule	Condition	Expression
2	$\neg (\operatorname {false} )$	$\operatorname {drop-formal} [Z,\lambda x.\lambda o.\lambda y.o\ x\ y,V]$
1	$\operatorname {true} \land \{p\}\subset \{k,m,p,q,f,x\}$	$\lambda x.\operatorname {drop-formal} [Z,\lambda o.\lambda y.o\ x\ y,V]$
2	$\neg (\operatorname {true} \land \{n\}\subset \{k,m,p,q,f,x\}$)	$\lambda x.\operatorname {drop-formal} [Z,(\lambda y.o\ x\ y)[o:=p],V]$
3		$\lambda x.\lambda y.\operatorname {drop-formal} [Z,p\ x\ y,V]$
		$\lambda x.\lambda y.p\ x\ y$

Example

Starting with the function definition of the Y-combinator,

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

Transformation	Expression
	$\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p$
lambda-preprocess	$\operatorname {let} p\ f\ x=f\ (x\ x)\operatorname {in} \operatorname {let} q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p$
lambda-process	$\operatorname {let} p=\lambda f.\lambda x.f\ (x\ x)\operatorname {in} \operatorname {let} q=\lambda p.\lambda f.(p\ f)\ (p\ f)\operatorname {in} q\ p$
lambda-convert	$(\lambda q.(\lambda p.q\ p)\ (\lambda f.\lambda x.f\ (x\ x)))\ (\lambda p.\lambda f.(p\ f)\ (p\ f))$
sink-tran	$(\lambda p.\lambda f.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))$
sink-tran	$\lambda f.(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))$
drop-param	$\lambda f.(\lambda p.p\ p)\ (\lambda x.f\ (x\ x))$
beta-redex	$\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\$

Which gives back the Y combinator,

$\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$

See also

• Supercombinator

External links

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