Misplaced Pages

This is an old revision of this page, as edited by Thepigdog (talk | contribs) at 13:51, 21 November 2013 (→Lambda dropping in Lambda Calculus). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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,

${\displaystyle \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	${\displaystyle f\ x=y\equiv f=\lambda x.y}$
lambda-let	${\displaystyle \operatorname {let} f:f=E\operatorname {in} L\equiv \lambda f.L\ E)}$ (where f is a variable name).
let-let	${\displaystyle 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.
• ${\displaystyle \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. ${\displaystyle \operatorname {de-lambda} \equiv \operatorname {let-combine} \operatorname {in} E]}$
2. ${\displaystyle V\not \in \operatorname {FV} \to \operatorname {de-lambda} \equiv \operatorname {let-combine} \operatorname {in} V]}$
3. ${\displaystyle \operatorname {de-lambda} \equiv \operatorname {de-lambda} \ \operatorname {de-lambda} }$
4. ${\displaystyle \operatorname {de-lambda} \equiv V}$
5. ${\displaystyle \operatorname {de-lambda} \equiv \operatorname {de-lambda} }$
6. ${\displaystyle \operatorname {de-lambda} \equiv \operatorname {de-lambda} =\operatorname {de-lambda} }$
7. ${\displaystyle V\neq W\to \operatorname {let-combine} \equiv \operatorname {let} V,W:E\land F\operatorname {in} G}$
8. ${\displaystyle \operatorname {let-combine} \equiv \operatorname {let} V:E\operatorname {in} F}$

For example the Y combinator,

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

Rule	Lambda Expression
2	${\displaystyle \operatorname {de-lambda} }$
6, 3	${\displaystyle \operatorname {let} p:\operatorname {de-lambda} \operatorname {in} p}$
2	${\displaystyle \operatorname {let} p:p\ f=\operatorname {de-lambda} \operatorname {in} p}$
1	${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:\operatorname {de-lambda} \operatorname {in} f\ (x\ x)\operatorname {in} p}$
5	${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:\operatorname {de-lambda} \operatorname {in} f\ (x\ x)\operatorname {in} p}$
6, 3	${\displaystyle \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. ${\displaystyle \operatorname {de-let} \equiv \operatorname {get-lambda} =}$
2. ${\displaystyle \operatorname {de-let} \equiv (\lambda F.\operatorname {de-let} )\ \operatorname {get-lambda} =}$
3. ${\displaystyle \operatorname {de-let} \equiv \lambda V.\operatorname {de-let} }$
4. ${\displaystyle \operatorname {de-let} \equiv \operatorname {de-let} \ \operatorname {de-let} }$
5. ${\displaystyle \operatorname {de-let} \equiv V}$
6. ${\displaystyle \operatorname {get-lambda} =\operatorname {get-lambda} }$
7. ${\displaystyle \operatorname {get-lambda} =\operatorname {de-let} }$
8. ${\displaystyle W\not \in \operatorname {FV} \to \operatorname {de-let} \equiv \operatorname {de-let} }$

For example the let expression obtained from the Y combinator,

${\displaystyle \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	${\displaystyle \operatorname {de-let} }$
6	${\displaystyle \operatorname {get-lambda} }$
7	${\displaystyle \operatorname {get-lambda} }$
3	${\displaystyle \operatorname {de-let} }$
2, 4, 5	${\displaystyle \lambda f.\operatorname {de-let} }$
6	${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ \operatorname {get-lambda} }$
7	${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ \operatorname {get-lambda} }$
3, 4, 5	${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ \operatorname {de-let} }$
	${\displaystyle \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

${\displaystyle \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	${\displaystyle \operatorname {de-let} }$
2	${\displaystyle \operatorname {de-let} }$
6, 7	${\displaystyle (\lambda p.\operatorname {de-let} )\ \operatorname {get-lambda} }$
2, 4, 5	${\displaystyle (\lambda p.\operatorname {de-let} )\ \lambda f.\lambda x.f\ (x\ x)}$
6, 7	${\displaystyle (\lambda p.(\lambda q.q\ p)\ \operatorname {get-lambda} )\ \lambda f.\lambda x.f\ (x\ x)}$
	${\displaystyle (\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)}$

Lambda Lifting

This section describes lambda lifting in detail. 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.

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 expensive on processing time for the compiler. 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.

In the Untyped Lambda Calculus, where the basic types are functions, lifting may change the result of beta reduction of a lambda expression. This because in the Untyped Lambda Calculus beta reduction of a lifted Lambda expression may give a different result. The resulting functions will have the same meaning, in a mathematical sense, but not be regarded as the same in the Untyped Lambda Calculus.

Lambda lifting is useful in understanding lambda expressions, and the compiler optimization of code.

Lamba-Lift transformation

This section describes a meta-function called lambda-lift-tran that 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}$

The de-let meta function may then be used to convert the result back into Lambda Calculus.

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

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,

• 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.
• The lift is performed by a call to the lambda-lift meta function, described in the next section,

1. ${\displaystyle \operatorname {lambda-lift-tran} =\operatorname {merge-let} ]}$
2. ${\displaystyle \operatorname {lambda-apply} =\operatorname {lambda-process} ,L]]}$
3. ${\displaystyle \operatorname {lambda-process} =L}$
4. ${\displaystyle \operatorname {lambda-process} =\operatorname {lambda-apply} ]}$

After the lifts are applied the lets are combined together into a single let.

${\displaystyle \operatorname {merge-let} =\operatorname {merge-let} }$

${\displaystyle \operatorname {merge-let} =E}$

Choosing the expression for lifting

There are two different ways that an expression may be selected for lifting. The first treats all lambda abstractions as defining anonymous functions. The second, treats lambda abstractions which are applied to a parameter as defining a function.

These two predicates are needed for both definitions.

lambda-free - An expression containing no lambda abstractions.

${\displaystyle \operatorname {lambda-free} =\operatorname {false} }$

${\displaystyle \operatorname {lambda-free} =\operatorname {true} }$

${\displaystyle \operatorname {lambda-free} =\operatorname {lambda-free} \land \operatorname {lambda-free} }$

lambda-anon - An anonymous function. An expression like ${\displaystyle \lambda x_{1}.\ ...\ \lambda x_{n}.X}$ where X is lambda free.

${\displaystyle \operatorname {lambda-anon} =\operatorname {lambda-free} \lor \operatorname {lambda-anon} }$

${\displaystyle \operatorname {lambda-anon} =\operatorname {false} }$

${\displaystyle \operatorname {lambda-anon} =\operatorname {false} }$

Choosing anonymous functions only for lifting

Search for the deepest anonymous abstraction, so that when the lift is applied the function lifted will become a simple equation. This definition does not recognize a lambda abstractions with a parameter as defining a function. All lambda abstractions are regarded as defining anonymous functions.

lift-choice - The first anonymous found in traversing the expression or none if there is no function.

1. ${\displaystyle \operatorname {lambda-anon} \to \operatorname {lift-choice} =X}$
2. ${\displaystyle \operatorname {lift-choice} =\operatorname {lift-choice} }$
3. ${\displaystyle \operatorname {lift-choice} \neq \operatorname {none} \to \operatorname {lift-choice} =\operatorname {lift-choice} }$
4. ${\displaystyle \operatorname {lift-choice} =\operatorname {lift-choice} }$
5. ${\displaystyle \operatorname {lift-choice} =\operatorname {none} }$

For example,

Lambda choice on ${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))}$ is ${\displaystyle \lambda x.f\ (x\ x)}$

Rule	function type	choice
2		${\displaystyle \operatorname {lift-choice} }$
3		${\displaystyle \operatorname {lift-choice} }$
1	anon	${\displaystyle \operatorname {lift-choice} }$
		${\displaystyle \lambda x.f\ (x\ x)}$

Lambda choice on ${\displaystyle \lambda f.(p\ f)\ (p\ f)}$ is ${\displaystyle \lambda f.(p\ f)\ (p\ f)}$

Rule	function type	choice
2	anon	${\displaystyle \operatorname {lift-choice} }$
2		${\displaystyle \lambda f.(p\ f)\ (p\ f)}$

Choosing named and anonymous functions for lifting

Search for the deepest named or anonymous function definition, so that when the lift is applied the function lifted will become a simple equation. This definition recognizes a lambda abstraction with an actual parameter as defining a function. Only lambda abstractions without an application are treated as anonymous functions.

lambda-named - A named function. An expression like ${\displaystyle (\lambda F.M)\ N}$ where M is lambda free and N is lambda free or an anonymous function.

${\displaystyle \operatorname {lambda-named} =\operatorname {false} }$

${\displaystyle \operatorname {lambda-named} =\operatorname {false} }$

${\displaystyle \operatorname {lambda-named} =\operatorname {lambda-free} \land (\operatorname {lambda-anon} }$

lift-choice - The first anonymous or named function found in traversing the expression or none if there is no function.

1. ${\displaystyle \operatorname {lambda-named} \lor \operatorname {lambda-anon} \to \operatorname {lift-choice} =X}$
2. ${\displaystyle \operatorname {lift-choice} =\operatorname {lift-choice} }$
3. ${\displaystyle \operatorname {lift-choice} \neq \operatorname {none} \to \operatorname {lift-choice} =\operatorname {lift-choice} }$
4. ${\displaystyle \operatorname {lift-choice} =\operatorname {lift-choice} }$
5. ${\displaystyle \operatorname {lift-choice} =\operatorname {none} }$

For example,

Lambda choice on ${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))}$ is ${\displaystyle (\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))}$

Rule	function type	choice
2		${\displaystyle \operatorname {lift-choice} }$
1	named	${\displaystyle \operatorname {lift-choice} }$
		${\displaystyle (\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))}$

Lambda choice on ${\displaystyle \lambda f.f\ ((x\ f)\ (x\ f))}$ is ${\displaystyle \lambda f.f\ ((x\ f)\ (x\ f))}$

Rule	function type	choice
1	anon	${\displaystyle \operatorname {lift-choice} }$
		${\displaystyle \lambda f.f\ ((x\ f)\ (x\ f))}$

Lifting

Two types of lifting are possible.

• Anonymous lift
• Named lift

An anonymous lift has a lift expression which is a lambda abstraction only. It is regarded as defining an anonymous function. A name must be created for the function.

A named lift expression has a lambda abstraction applied to an expression. This lift is regarded as a named definition of a function.

Anonymous Lift

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 V). Make sure that the name identified by V has not been used.
• Add parameters to V, 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 V is the function name. It must be a new variable, i.e. a name not already used in the lambda expression,

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

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

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

Named Lift

The named lift is similar to the anonymous lift except that the function name V is provided.

${\displaystyle \operatorname {lambda-lift} \equiv \operatorname {let} V:\operatorname {de-lambda} \operatorname {in} L]}$

As for the anonymous lift, the expression G is constructed from V by applying the free variables of S. It is defined by,

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

Example - Lifting named and anonymous functions

For example the Y combinator,

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

Lifting named and anonymous functions

	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))\ (\lambda x.f\ (x\ x))}$	${\displaystyle x\ f}$	${\displaystyle \{x,f\}}$
2	${\displaystyle (\lambda f.(\lambda x.f\ (x\ x))(\lambda x.f\ (x\ x)))}$ ${\displaystyle }$	${\displaystyle x\ f=\lambda y.f\ (y\ y)}$			${\displaystyle \{x,f,p\}}$
3	${\displaystyle \lambda f.f\ ((x\ f)\ (x\ f))}$	${\displaystyle x\ f\ y=f\ (y\ y)}$	${\displaystyle \lambda f.f\ ((x\ f)\ (x\ f))}$	${\displaystyle q\ x}$	${\displaystyle \{x,f,p\}}$
4	${\displaystyle \lambda f.f\ ((x\ f)\ (x\ f))}$	${\displaystyle x\ f\ y=f\ (y\ y)\land q\ x=\lambda f.f\ ((x\ f)\ (x\ f))}$			${\displaystyle \{x,f,p,q\}}$
5	${\displaystyle q\ x}$	${\displaystyle x\ f\ y=f\ (y\ y)\land q\ x\ f=f\ ((x\ f)\ (x\ f))}$			${\displaystyle \{x,f,p,q\}}$

Example - Lifting anonymous functions only

Lifting anonymous functions only

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

Surprisingly this result is simpler than the one obtained from lifting named functions.

As a lambda expression (see Conversion from Let to Lambda expressions),

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

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

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

Lambda dropping is performed in two steps,

• Sinking
• Parameter dropping

The Lambda-drop-tran implements Lambda dropping. It is defined as,

${\displaystyle \operatorname {lambda-drop-tran} =\operatorname {drop-params-tran} ]]}$

Abstraction Sinking

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

${\displaystyle \operatorname {sink-tran} =\operatorname {sink} )\ \operatorname {sink-tran} ]]}$

${\displaystyle \operatorname {sink-tran} =\lambda X.\operatorname {sink-tran} }$

${\displaystyle \operatorname {sink-tran} =\operatorname {sink-tran} \ \operatorname {sink-tran} }$

${\displaystyle \operatorname {sink-tran} =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.

${\displaystyle X\not \in \operatorname {FV} \land X\not \in \operatorname {FV} \to \operatorname {sink} =G\ H}$

${\displaystyle X\not \in \operatorname {FV} \land X\in \operatorname {FV} \to \operatorname {sink} =G\ \operatorname {sink} }$

${\displaystyle X\in \operatorname {FV} \land X\not \in \operatorname {FV} \to \operatorname {sink} =(\operatorname {sink} )\ H}$

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

Abstraction. Use renaming to insure that the variable names are all distinct.

${\displaystyle X\neq V\to \operatorname {sink} =\lambda V.\operatorname {sink} }$

Variable - 2 cases.

${\displaystyle X\neq V\to \operatorname {sink} =V}$

${\displaystyle X=V\to \operatorname {sink} =Y}$