Lambda lifting

Lambda lifting is a meta-process that restructures a computer program so that functions are defined independently of each other in a global scope. An individual "lift" transforms a local function into a global function. It is a two step process, consisting of;

• Eliminating free variables in the function by adding parameters.
• Moving functions from a restricted scope to broader or global scope.

The term "lambda lifting" was first introduced by Thomas Johnsson around 1982 and was historically considered as a mechanism for implementing functional programming languages. It is used in conjunction with other techniques in some modern compilers.

Lambda lifting is not the same as closure conversion. It 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 technique may be used on individual functions, in code refactoring, to make a function usable outside the scope in which it was written. Lambda lifts may also be repeated, in order to transform the program. Repeated lifts may be used to convert a program written in lambda calculus into a set of recursive functions, without lambdas. This demonstrates the equivalence of programs written in lambda calculus and programs written as functions. However it does not demonstrate the soundness of lambda calculus for deduction, 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 (see Curry's paradox).

Lambda lifting is expensive on processing time for the compiler. An efficient implementation of lambda lifting is $O(n^{2})$ on processing time for the compiler.

In the untyped lambda calculus, where the basic types are functions, lifting may change the result of beta reduction of a lambda expression. The resulting functions will have the same meaning, in a mathematical sense, but are not regarded as the same function in the untyped lambda calculus. See also intensional versus extensional equality.

The reverse operation to lambda lifting is lambda dropping.

Lambda dropping 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 it 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.

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 a parameter:

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

Lambda lifting and closure are both methods for implementing block structured programs. It implements block structure by eliminating it. All functions are lifted to the global level. Closure conversion provides a "closure" which links the current frame to other frames. Closure conversion takes less compile time.

Recursive functions, and block structured programs, with or without lifting, may be implemented using a stack based implementation, which is simple and efficient. However a stack frame based implementation must be strict (eager). The stack frame based implementation requires that the life of functions be last-in, first-out (LIFO). That is, the most recent function to start its calculation must be the first to end.

Some functional languages (such as Haskell) are implemented using lazy evaluation, which delays calculation until the value is needed. The lazy implementation strategy gives flexibility to the programmer. Lazy evaluation requires delaying the call to a function until a request is made to the value calculated by the function. One implementation is to record a reference to a "frame" of data describing the calculation, in place of the value. Later when the value is required, the frame is used to calculate the value, just in time for when it is needed. The calculated value then replaces the reference.

The "frame" is similar to a stack frame, the difference being that it is not stored on the stack. Lazy evaluation requires that all the data required for the calculation be saved in the frame. If the function is "lifted", then the frame needs only record the function pointer, and the parameters to the function. Some modern languages use garbage collection in place of stack based allocation to manage the life of variables. In a managed, garbage collected environment, a closure records references to the frames from which values may be obtained. In contrast a lifted function has parameters for each value needed in the calculation.

Let expressions and lambda calculus

The Let expression is useful in describing lifting and dropping, and in describing the relationship between recursive equations and lambda expressions. Most functional languages have let expressions. Also, block structured programming languages like ALGOL and Pascal are similar in that they too allow the local definition of a function for use in a restricted scope.

The let expression used here is a fully mutually recursive version of let rec, as implemented in many functional languages.

Let expressions are related to Lambda calculus. Lambda calculus has a simple syntax and semantics, and is good for describing Lambda lifting. It is convenient to describe lambda lifting as a translations from lambda to a let expression, and lambda dropping as the reverse. This is because let expressions allow mutual recursion, which is, in a sense, more lifted than is supported in lambda calculus. Lambda calculus does not support mutual recursion and only one function may be defined at the outermost global scope.

Conversion rules which describe translation without lifting are given in the Let expression article.

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

${\begin{array}{l|l}{\textbf {Name}}&{\textbf {Law}}\\\hline {\text{Eta-reduction equivalence}}&f\ x=y\equiv f=\lambda x.y\\{\text{Let-Lambda equivalence}}&f\not \in FV(E)\to (\operatorname {let} f:f=E\operatorname {in} L\equiv (\lambda f.L)\ E)\ {\text{(where }}f{\text{ is a variable name.)}}\\{\text{Let combination}}&x\not \in FV(E)\to (\operatorname {let} v,...,w,x:E\land F\operatorname {in} L\equiv \operatorname {let} v,...,w:E\operatorname {in} \operatorname {let} x:F\operatorname {in} L)\\\end{array}}$

Meta-functions will be given that describe lambda lifting and dropping. 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.
• $\_$ represents a dummy variable, or an unknown value.

For simplicity the first rule given that matches will be applied. The rules also assume that the lambda expressions have been pre-processed so that each lambda abstraction has a unique name.

The substitution operator is used extensively. The expression $L[G:=S]$ means substitute every occurrence of G in L by S and return the expression. The definition used is extended to cover the substitution of expressions, from the definition given on the Lambda calculus page. The matching of expressions should compare expressions for alpha equivalence (renaming of variables).

Lambda lifting in lambda calculus

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.

Lambda lifts may be used on individual functions, in code refactoring, to make a function usable outside the scope in which it was written. Such lifts may also be repeated, until the expression has no lambda abstractions, in order to transform the program.

Lambda lift

A lift is given a sub-expression within an expression to lift to the top of that expression. The expression may be part of a larger program. This allows control of where the sub-expression is lifted to. The lambda lift operation used to perform a lift within a program is,

$\operatorname {lambda-lift-op} [S,L,P]=P[L:=\operatorname {lambda-lift} [S,L]]$

The sub expression may be either a lambda abstraction, or a lambda abstraction applied to a parameter.

Two types of lift 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

An anonymous lift takes a lambda abstraction (called S). 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 the lambda abstraction S for a function application, along with the addition of a definition for the function.

$\operatorname {lambda-lift} [S,L]\equiv \operatorname {let} V:\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} [V,\operatorname {FV} [S]]$

where V is the function name. It must be a new variable, i.e. a name not already used in the lambda expression,

$V\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.

Example for anonymous lift.

For example, ${\begin{aligned}F&=true\\L&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\S&=\lambda x.f\ (x\ x)\\G&=p\ f\end{aligned}}$ $\operatorname {de-lambda} [p\ f=\lambda x.f\ (x\ x)]\equiv p\ f\ x=f\ (x\ x)$ See de-lambda in Conversion from lambda to let expressions. The result is, $\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$

Example of call construction.
$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$

Named lift

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

$\operatorname {lambda-lift} [(\lambda V.E)\ S,L]\equiv \operatorname {let} V:\operatorname {de-lambda} [G=S]\operatorname {in} L[(\lambda V.E)\ S:=E[V:=G]]$

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

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

Example for named lift.

For example, ${\begin{aligned}V&=x\\E&=f\ (x\ x)\\S&=(\lambda x.f\ (x\ x))\\L&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\G&=x\ f\end{aligned}}$ $E[V:=G]=f\ (x\ x)[x:=x\ f]=f\ ((x\ f)\ (x\ f))$ $L[(\lambda V.E)\ F:=E[V:=G]]=L[(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)):=f\ ((x\ f)\ (x\ f))]=\lambda f.f\ ((x\ f)\ (x\ f))$ $\operatorname {de-lambda} [x\ f=\lambda y.f\ (y\ y)]\equiv x\ f\ y=f\ (y\ y)$ See de-lambda in Conversion from lambda to let expressions. The result is, gives, $\operatorname {lambda-lift} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)),\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\equiv \operatorname {let} x\ f\ y=f\ (y\ y)\operatorname {in} \lambda f.(x\ f)\ (x\ f)$

Lambda-lift transformation

A lambda lift transformation takes a lambda expression and lifts all lambda abstractions to the top of the expression. The abstractions are then translated into recursive functions, which eliminates the lambda abstractions. The result is a functional program in the form,

• $\operatorname {let} M\operatorname {in} N$

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

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 de-let meta function may then be used to convert the result back into lambda calculus.

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

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

• A sub expression chosen for it by the function lift-choice. 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,

${\begin{cases}\operatorname {lambda-lift-tran} [L]=\operatorname {drop-params-tran} [\operatorname {merge-let} [\operatorname {lambda-apply} [L]]]\\\operatorname {lambda-apply} [L]=\operatorname {lambda-process} [\operatorname {lift-choice} [L],L]\\\operatorname {lambda-process} [\operatorname {none} ,L]=L\\\operatorname {lambda-process} [S,L]=\operatorname {lambda-apply} [\operatorname {lambda-lift} [S,L]]\end{cases}}$

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

${\begin{cases}\operatorname {merge-let} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]=\operatorname {merge-let} [\operatorname {let} V,W:E\land F\operatorname {in} G]\\\operatorname {merge-let} [E]=E\end{cases}}$

Then Parameter dropping is applied to remove parameters that are not necessary in the "let" expression. The let expression allows the function definitions to refer to each other directly, whereas lambda abstractions are strictly hierarchical, and a function may not directly refer to itself.

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. Lambda abstractions applied to a parameter have a dual interpretation as either a let expression defining a function, or as defining an anonymous function. Both interpretations are valid.

These two predicates are needed for both definitions.

lambda-free - An expression containing no lambda abstractions.

${\begin{cases}\operatorname {lambda-free} [\lambda F.X]=\operatorname {false} \\\operatorname {lambda-free} [V]=\operatorname {true} \\\operatorname {lambda-free} [M\ N]=\operatorname {lambda-free} [M]\land \operatorname {lambda-free} [N]\end{cases}}$

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

${\begin{cases}\operatorname {lambda-anon} [\lambda F.X]=\operatorname {lambda-free} [X]\lor \operatorname {lambda-anon} [X]\\\operatorname {lambda-anon} [V]=\operatorname {false} \\\operatorname {lambda-anon} [M\ N]=\operatorname {false} \end{cases}}$

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. $\operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X$
2. $\operatorname {lift-choice} [\lambda F.X]=\operatorname {lift-choice} [X]$
3. $\operatorname {lift-choice} [M]\neq \operatorname {none} \to \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [M]$
4. $\operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [N]$
5. $\operatorname {lift-choice} [V]=\operatorname {none}$

For example,

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

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

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

Rule	function type	choice
2	anon	$\operatorname {lift-choice} [\lambda f.(p\ f)\ (p\ f)]$
2		$\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 $(\lambda F.M)\ N$ where M is lambda free and N is lambda free or an anonymous function.

${\begin{array}{l}\operatorname {lambda-named} [(\lambda F.M)\ N]=\operatorname {lambda-free} [M]\land \operatorname {lambda-anon} [N]\\\operatorname {lambda-named} [\lambda F.X]=\operatorname {false} \\\operatorname {lambda-named} [V]=\operatorname {false} \end{array}}$

lift-choice

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

1. $\operatorname {lambda-named} [X]\lor \operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X$
2. $\operatorname {lift-choice} [\lambda F.X]=\operatorname {lift-choice} [X]$
3. $\operatorname {lift-choice} [M]\neq \operatorname {none} \to \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [M]$
4. $\operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [N]$
5. $\operatorname {lift-choice} [V]=\operatorname {none}$

For example,

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

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

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

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

Examples

For example, the Y combinator,

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

is lifted as,

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

and after Parameter dropping,

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

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

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

Lifting named and anonymous functions

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

If lifting anonymous functions only, the Y combinator is,

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

and after Parameter dropping,

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

As a lambda expression,

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

Lifting anonymous functions only

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

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

Execution

Apply function to K,

${\begin{cases}\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))\\\end{cases}}$

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 parameters to functions. Reducing the number of parameters makes functions easier to comprehend.

In the Lambda lifting section, a meta function for first lifting and then converting the resulting lambda expression into recursive equation was described. The Lambda 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

Lambda drop

A Lambda drop is applied to an expression which is part of a program. Dropping is controlled by a set of expressions from which the drop will be excluded.

$\operatorname {lambda-drop-op} [L,P,X]=P[L:=\operatorname {drop-params-tran} [\operatorname {sink-test} [L,X]]]$

where,

L is the lambda abstraction to be dropped.

P is the program

X is a set of expressions to be excluded from dropping.

Lambda drop transformation

The lambda drop transformation sinks all abstractions in an expression. Sinking is excluded from expressions in a set of expressions,

$\operatorname {lambda-drop-tran} [L,X]=\operatorname {drop-params-tran} [\operatorname {sink-tran} [\operatorname {de-let} [L,X]]]$

where,

L is the expression to be transformed.

X is a set of sub expressions to be excluded from the dropping.

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

${\begin{cases}\operatorname {sink-tran} [(\lambda N.B)\ Y,X]=\operatorname {sink-test} [(\lambda N.\operatorname {sink-tran} [B])\ \operatorname {sink-tran} [Y],X]\\\operatorname {sink-tran} [\lambda N.B,X]=\lambda N.\operatorname {sink-tran} [B,X]\\\operatorname {sink-tran} [M\ N,X]=\operatorname {sink-tran} [M,X]\ \operatorname {sink-tran} [M,X]\\\operatorname {sink-tran} [V,X]=V\end{cases}}$

Abstraction sinking

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.

${\begin{cases}E\not \in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=G\ H\\E\not \in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=\operatorname {sink-test} [G\ \operatorname {sink-test} [(\lambda E.H)\ Y,X]]\\E\in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=(\operatorname {sink-test} [(\lambda E.G)\ Y,X])\ H\\E\in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=(\lambda E.G\ H)\ Y\end{cases}}$

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

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

Variable - 2 cases.

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

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

Sink test excludes expressions from dropping,

$L\in X\to \operatorname {sink-test} [L,X]=L$

$L\not \in X\to \operatorname {sink-test} [L,X]=\operatorname {sink} [L,X]$

Example

Example of sinking

For example, Rule Expression de-let $\operatorname {sink-tran} [\operatorname {de-let} [\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p]]$ sink-tran $\operatorname {sink-tran} [(\lambda p.(\lambda q.q\ p)\ (\lambda p.\lambda f.(p\ f)\ (p\ f)))\ (\lambda f.\lambda x.f\ (x\ x))]$ Application $\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 q.q\ p)\ (\lambda p.\lambda f.(p\ f)\ (p\ f))]$ $E\in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]$ $E=q,G=q,H=p,Y=(\lambda p.\lambda f.(p\ f)\ (p\ f)),X=\{\}$ $(\operatorname {sink} [(\lambda E.G)\ Y,X])\ H$ $(\operatorname {sink} [(\lambda q.q)\ (\lambda p.\lambda f.(p\ f)\ (p\ f)),X])\ p$ Variable $\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 q.q)\ (\lambda p.\lambda f.(p\ f)\ (p\ f))]$ $E=V\to \operatorname {sink} [(\lambda E.V)\ Y,X]$ $E=q,V=q,Y=(\lambda p.\lambda f.(p\ f)\ (p\ f)),X=\{\}$ $Y$ $(\lambda p.\lambda f.(p\ f)\ (p\ f))$ Application $\operatorname {sink} [(\lambda p.(\lambda p.\lambda f.(p\ f)\ (p\ f))\ p)\ (\lambda f.\lambda x.f\ (x\ x))]$ $E\not \in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]$ $E=p,G=(\lambda p.\lambda f.(p\ f)\ (p\ f)),H=p,Y=(\lambda f.\lambda x.f\ (x\ x))$ $\operatorname {sink} [G\ \operatorname {sink} [(\lambda E.H)\ Y,X]]$ Variable $\operatorname {sink} [(\lambda p.\lambda f.(p\ f)\ (p\ f))\ \operatorname {sink-test} [(\lambda p.p)\ (\lambda f.\lambda x.f\ (x\ x)),X]]$ $\operatorname {sink} [(\lambda p.p)\ (\lambda f.\lambda x.f\ (x\ x)),X]$ $E=V\to \operatorname {sink} [(\lambda E.V)\ Y,X]$ $E=p,V=p,Y=(\lambda f.\lambda x.f\ (x\ x)),X=\{\}$ $Y$ $(\lambda f.\lambda x.f\ (x\ x))$ Abstraction $\operatorname {sink} [(\lambda p.\lambda f.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))]$ $V\neq W\to \operatorname {sink} [(\lambda V.\lambda W.E)\ Y,X]$ $V=p,W=f,E=(p\ f)\ (p\ f),Y=(\lambda f.\lambda x.f\ (x\ x))$ $\lambda W.\operatorname {sink} [(\lambda V.E)\ Y,X]$ Application $\lambda f.\operatorname {sink} [(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x)),X]$ $\operatorname {sink} [(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x)),X]$ $E\in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]$ $E=p,G=(p\ f),H=(p\ f),Y=(\lambda f.\lambda x.f\ (x\ x))$ $(\lambda E.G\ H)\ Y$ $(\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 are 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 m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \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 m,p,q.(\lambda g.\lambda n.n\ (g\ m\ p\ n)\ (g\ q\ p\ n))\ \lambda x.\lambda o.\lambda y.o\ x\ y$

$\equiv \lambda m,p,q.(\lambda g.\lambda n.n\ (g\ m\ n)\ (g\ q\ n))\ \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-list} [L,D,V,\_]$

Build parameter lists

For each abstraction that defines a function, build the information required to make decisions on dropping names. This information describes 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 m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \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, g there is parameter list.

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

build-param-lists builds all the lists for an expression, by traversing the expression. It has four parameters;

• The lambda expression being analyzed.
• The table parameter lists for names.
• The table of values for parameters.
• The returned parameter list, which is used internally by the

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

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

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

${\begin{cases}\operatorname {build-list} [\lambda P.B,D,V,[X,\_,\_]::L]\equiv \operatorname {build-list} [B,D,V,L]\\\operatorname {build-list} [B,D,V,[]]\equiv \operatorname {build-param-lists} [B,D,V,\_]\end{cases}}$

Variable - A call to a function.

$\operatorname {build-param-lists} [N,D,V,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 actual parameter details.

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

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

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.

${\begin{cases}\operatorname {equate} [A,N]\equiv A=N\lor (\operatorname {def} [V[N]]\land A=V[N])&{\text{if }}N{\text{ is a variable.}}\\\operatorname {equate} [A,E]\equiv A=E&{\text{otherwise.}}\end{cases}}$

The above logic is quite subtle in the way that it works. 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} [S]\equiv S\in \{X:X=S\}$

Similarly, def uses set theory to query if a variable has been given a value;

$\operatorname {def} [F]\equiv |\{X:X=F\}|$

Let - Let expression.

$\operatorname {build-param-list} [\operatorname {let} V:E\operatorname {in} L,D,V,\_]\equiv \operatorname {build-param-list} [E,D,V,\_]\land \operatorname {build-param-list} [L,D,V,\_]$

And - For use in "let".

$\operatorname {build-param-lists} [E\land F,D,V,\_]\equiv \operatorname {build-param-lists} [E,D,V,\_]\land \operatorname {build-param-lists} [F,D,V,\_]$

Examples

For example, building the parameter lists for,

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

gives,

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

and the parameter o is dropped to give,

$\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ n)\ (g\ q\ n)))\ \lambda x.\lambda y.p\ x\ y$

Build parameter list for $\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y$
Build parameter list example
$\operatorname {build-param-list} [\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y,D,V,\_]$ Rule Expression Abstraction $\operatorname {build-param-list} [\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y,D,V,\_]$ Abstraction $\operatorname {build-param-list} [(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y,D,V,\_]$ $\operatorname {build-param-lists} [n\ (g\ m\ p\ n)\ (g\ q\ p\ n),D,V,R]\land \operatorname {build-list} [\lambda x.\lambda o.\lambda y.o\ x\ y,D,V,D[g]]$ $\operatorname {build-list} [\lambda x.\lambda o.\lambda y.o\ x\ y,D,V,D[g]]$ Rule Expression Add param $\operatorname {build-list} [\lambda x.\lambda o.\lambda y.o\ x\ y,D,V,D[g]]\land D[g]=L_{1}$ Add param $\operatorname {build-list} [\lambda o.\lambda y.o\ x\ y,D,V,L_{1}]\land D[g]=[x,\_,\_]::L_{1}$ Add param $\operatorname {build-list} [\lambda y.o\ x\ y,D,V,L_{2}]\land D[g]=[x,\_,\_]::[o,\_,\_]::L_{2}$ End list $\operatorname {build-list} [o\ x\ y,D,V,L_{3}]\land D[g]=[x,\_,\_]::[o,\_,\_]::[y,\_,\_]::L_{3}$ $\operatorname {build-param-lists} [o\ x\ y,D,V,[]]\land D[g]=[x,\_,\_]::[o,\_,\_]::[y,\_,\_]::[]$ $\operatorname {build-param-lists} [n\ (g\ m\ p\ n)\ (g\ q\ p\ n),D,V,R]$ Rule Expression Application $\operatorname {build-param-lists} [n\ (g\ m\ p\ n)\ (g\ q\ p\ n),D,V,R]$ Application $\operatorname {build-param-lists} [n\ (g\ m\ p\ n),D,V,T_{1}]\land \operatorname {build-param-lists} [g\ q\ p\ n,D,V,K_{1}]$ $\land ((T_{1}=[F_{1},S_{1},A_{1}]::R$ $\land (S_{1}\implies (\operatorname {equate} [A_{1},g\ q\ p\ n]\land V[F_{1}]=g\ q\ p\ n))\land D[F_{1}]=K_{1})$ Variable $\operatorname {build-param-lists} [n,D,V,T_{2}]\land \operatorname {build-param-lists} [g\ m\ p\ n,D,V,K_{2}]\land \operatorname {build-param-lists} [g\ q\ p\ n,D,V,K_{1}]$ $\land ((T_{2}=[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::R$ $\land (S_{1}\implies (\operatorname {equate} [A_{1},g\ q\ p\ n]\land V[F_{1}]=g\ q\ p\ n))\land D[F_{1}]=K_{1})$ $\land (S_{2}\implies (\operatorname {equate} [A_{2},g\ m\ p\ n]\land V[F_{2}]=g\ m\ p\ n))\land D[F_{2}]=K_{2})$ Variable $\operatorname {build-param-lists} [g\ m\ p\ n,D,V,K_{2}]\land \operatorname {build-param-lists} [g\ q\ p\ n,D,V,K_{1}]$ $\land ((D[n]=[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::R$ $\land (S_{1}\implies (\operatorname {equate} [A_{1},g\ q\ p\ n]\land V[F_{1}]=g\ q\ p\ n))\land D[F_{1}]=K_{1})$ $\land (S_{2}\implies (\operatorname {equate} [A_{2},g\ m\ p\ n]\land V[F_{2}]=g\ m\ p\ n))\land D[F_{2}]=K_{2})$ Gives, $D[n]=[\_,\_,g\ m\ p\ n]::[\_,\_,g\ q\ p\ n]::R$ $\operatorname {build-param-lists} [g\ m\ p\ n,D,V,K_{2}]$ Rule Expression application $\operatorname {build-param-lists} [g\ m\ p\ n,D,V,K_{2}]$ $\operatorname {build-param-lists} [g\ m\ p,D,V,T_{3}]\land \operatorname {build-param-lists} [n,D,V,K_{3}]$ $\land ((T_{3}=[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},n]\land V[F_{3}]=n))\land D[F_{3}]=D[n])$ application, Variable $\operatorname {build-param-lists} [g\ m,D,V,T_{4}]\land \operatorname {build-param-lists} [p,D,V,K_{4}]$ $\land T_{4}=[\_,S_{4},A_{4}]::[\_,S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},n]\land V[F_{3}]=n))\land D[F_{3}]=D[n])$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[F_{4}]=p))\land D[F_{4}]=D[p]$ application, Variable $\operatorname {build-param-lists} [g,D,V,T_{5}]\land \operatorname {build-param-lists} [m,D,V,K_{5}]$ $\land T_{5}=[F_{5},S_{5},A_{5}]::[F_{4},S_{4},A_{4}]::[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},n]\land V[F_{3}]=n))\land D[F_{3}]=D[n])$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[F_{4}]=p))\land D[F_{4}]=D[p]$ $\land (S_{5}\implies (\operatorname {equate} [A_{5},m]\land V[F_{5}]=m))\land D[F_{5}]=D[m]$ Variable $D[g]=[x,S_{5},A_{5}]::[o,S_{4},A_{4}]::[y,S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},n]\land V[y]=n))\land D[y]=D[n])$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[o]=p))\land D[o]=D[p]$ $\land (S_{5}\implies (\operatorname {equate} [A_{5},m]\land V[x]=m))\land D[x]=D[m]$ $\operatorname {build-param-lists} [g\ q\ p\ n,D,V,K_{1}]$ Rule Expression application $\operatorname {build-param-lists} [g\ q\ p\ n,D,V,K_{1}]$ $\operatorname {build-param-lists} [g\ q\ p,D,V,T_{6}]\land \operatorname {build-param-lists} [n,D,V,K_{6}]$ $\land ((T_{6}=[F_{6},S_{6},A_{6}]::K_{1}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},n]\land V[F_{6}]=n))\land D[F_{6}]=D[n])$ application, Variable $\operatorname {build-param-lists} [g\ q,D,V,T_{7}]\land \operatorname {build-param-lists} [p,D,V,K_{7}]$ $\land T_{7}=[\_,S_{7},A_{7}]::[\_,S_{6},A_{6}]::K_{1}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},n]\land V[F_{6}]=n))\land D[F_{6}]=D[n])$ $\land (S_{7}\implies (\operatorname {equate} [A_{7},p]\land V[F_{7}]=p))\land D[F_{7}]=D[p]$ application, Variable $\operatorname {build-param-lists} [g,D,V,T_{8}]\land \operatorname {build-param-lists} [m,D,V,K_{8}]$ $\land T_{8}=[F_{8},S_{8},A_{8}]::[F_{7},S_{7},A_{7}]::[F_{6},S_{6},A_{6}]::K_{1}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},n]\land V[F_{6}]=n))\land D[F_{6}]=D[n])$ $\land (S_{7}\implies (\operatorname {equate} [A_{7},p]\land V[F_{7}]=p))\land D[F_{7}]=D[p]$ $\land (S_{8}\implies (\operatorname {equate} [A_{8},q]\land V[F_{8}]=q))\land D[F_{8}]=D[q]$ Variable $D[g]=[x,S_{8},A_{8}]::[o,S_{6},A_{7}]::[y,S_{6},A_{6}]::K_{1}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},n]\land V[y]=n))\land D[y]=D[n])$ $\land (S_{7}\implies (\operatorname {equate} [A_{7},p]\land V[o]=p))\land D[o]=D[p]$ $\land (S_{8}\implies (\operatorname {equate} [A_{8},q]\land V[x]=q))\land D[x]=D[q]$ As there are no definitions for, $V[n],V[p],V[q],V[m]$, then equate can be simplified to, $\operatorname {equate} [A,N]\equiv A=N\lor (\operatorname {def} [V[N]]\land A=V[N])\equiv A=N$ By removing expressions not needed, $D[g]=[x,S_{5},A_{5}]::[o,S_{4},A_{4}]::[y,S_{3},A_{3}]::K_{2}$ $\land S_{3}\implies A_{3}=n$ $\land S_{4}\implies A_{4}=p$ $\land S_{5}\implies A_{5}=m$ $D[g]=[x,S_{8},A_{8}]::[o,S_{6},A_{7}]::[y,S_{6},A_{6}]::K_{1}$ $\land S_{6}\implies A_{6}=n$ $\land S_{7}\implies A_{7}=p$ $\land S_{8}\implies A_{8}=q$ By comparing the two expressions for $D[g]$, get, $S_{5}=S_{8},A_{5}=A_{8},S_{4}=S_{7},A_{4}=A_{7},S_{3}=S_{6},A_{3}=A_{6}$ If $S_{3}$ is true; $n=A_{3}=A_{6}=n$ If $S_{3}$ is false there is no implication. So $S_{3}=\_$ which means it may be true or false. If $S_{4}$ is true; $p=A_{4}=A_{7}=p$ If $S_{5}$ is true; $m=A_{5}=A_{8}=q$ So $S_{5}$ is false. The result is, $D[g]=[x,\operatorname {false} ,\_]::[o,\_,p]::[y,\_,n]::\_$ $\operatorname {build-param-lists} [o\ x\ y,D,V,L]$ Rule Expression application $\operatorname {build-param-lists} [o\ x\ y,D,V,L]$ application $\operatorname {build-param-lists} [o\ x,D,V,T_{9}]\land \operatorname {build-param-lists} [y,D,V,K_{9}]$ $\land T_{9}=[F_{9},S_{9},A_{9}]::L$ $\land (S_{9}\implies (\operatorname {equate} [A_{9},y]\land V[F_{9}]=A_{9})\land K_{9}=D[F_{9}]$ variable $\operatorname {build-param-lists} [o,D,V,T_{10}]\land \operatorname {build-param-lists} [x,D,V,K_{10}]\land \operatorname {build-param-lists} [y,D,V,K_{10}]$ $\land T_{10}=[F_{10},S_{10},A_{10}]::[F_{9},S_{9},A_{9}]::L$ $\land (S_{9}\implies (\operatorname {equate} [A_{9},y]\land V[F_{9}]=A_{9})\land K_{9}=D[F_{9}]$ $\land (S_{10}\implies (\operatorname {equate} [A_{10},y]\land V[F_{10}]=A_{10})\land K_{10}=D[F_{10}]$ $\land D[o]=[F_{10},S_{10},A_{10}]::[F_{9},S_{9},A_{9}]::L$ $\land (S_{9}\implies (\operatorname {equate} [A_{9},y]\land V[F_{9}]=A_{9})\land K_{9}=D[F_{9}]$ $\land (S_{10}\implies (\operatorname {equate} [A_{10},y]\land V[F_{10}]=A_{10})\land K_{10}=D[F_{10}]$ By similar arguments as used above get, $D[o]=[\_,\_,x]::[\_,\_,y]::\_$ and from previously, $D[g]=[[x,\operatorname {false} ,\_],[o,\operatorname {true} ,p],[y,\operatorname {true} ,n]]$ $D[n]=[[\_,\_,(g\ m\ p\ n)],[\_,\_,(g\ q\ p\ n)]]$ $D[m]=\_$ $D[p]=\_$ $D[q]=\_$

Another example is,

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

Here x is equal to f. The parameter list mapping is,

$D[p]=[[q,\_,p],[x,\_,f]]$

and the parameter x is dropped to give,

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

Build parameter list for $\lambda f.((\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x))$

The logic in equate is used in this more difficult example. $\operatorname {build-param-list} [\lambda f.((\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x)),D,V,\_]$ Rule Expression Abstraction $\operatorname {build-param-list} [\lambda f.((\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x)),D,V,\_]$ Abstraction $\operatorname {build-param-list} [(\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x)),D,V,\_]$ $\operatorname {build-param-lists} [f\ (p\ p\ f),D,\_]\land \operatorname {build-list} [\lambda q.\lambda x.x\ (q\ q\ x),D,D[p]]$ $\operatorname {build-param-lists} [f\ (p\ p\ f),D,\_]\land \operatorname {build-list} [\lambda q.\lambda x.x\ (q\ q\ x),D,D[p]]$ $\operatorname {build-list} [\lambda q.\lambda x.x\ (q\ q\ x),D,D[p]]$ Rule Expression Add param $\operatorname {build-list} [\lambda q.\lambda x.x\ (q\ q\ x),D,D[p]]\land D[p]=L_{1}$ Add param $\operatorname {build-list} [\lambda x.x\ (q\ q\ x),D,L_{2}]\land D[p]=[q,\_,\_]::L_{2}$ End list $\operatorname {build-list} [x\ (q\ q\ x),D,L_{3}]\land D[p]=[q,\_,\_]::[x,\_,\_]::L_{3}$ $\operatorname {build-param-lists} [x\ (q\ q\ x),D,[]]\land D[p]=[q,\_,\_]::[x,\_,\_]::[]$ $\operatorname {build-param-lists} [\lambda p.f\ (p\ p\ f),D,V,T_{1}]$ Rule Expression Abstraction $\operatorname {build-param-lists} [\lambda p.f\ (p\ p\ f),D,V,T_{1}]$ Application $\operatorname {build-param-lists} [f\ (p\ p\ f),D,V,T_{1}]$ Name $\operatorname {build-param-lists} [f,D,V,T_{2}]\land \operatorname {build-param-lists} [p\ p\ f,D,V,K_{2}]$ $\land T_{2}=[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_$ $\land (S_{2}\implies (\operatorname {equate} [A_{2},p\ p\ f]\land V[F_{2}]=A_{2}))\land D[F_{2}]=K_{2}$ Name $\operatorname {build-param-lists} [p\ p\ f,D,V,K_{2}]$ $\land D[f]=[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_$ $\land (S_{2}\implies (\operatorname {equate} [A_{2},p\ p\ f]\land V[F_{2}]=A_{2}))\land D[F_{2}]=K_{2}$ Name $\operatorname {build-param-lists} [p\ p,D,V,T_{3}]\land \operatorname {build-param-lists} [f,D,V,K_{3}]$ $\land T_{3}=[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[F_{3}]=A_{3}))\land D[F_{3}]=K_{3}$ Application $\operatorname {build-param-lists} [p\ p,D,V,T_{3}]$ $\land T_{3}=[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{2}\implies (\operatorname {equate} [A_{2},p\ p\ f]\land V[F_{2}]=A_{2}))\land D[F_{2}]=K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[F_{3}]=A_{3}))\land D[F_{3}]=D[f]$ Name $\operatorname {build-param-lists} [p,D,V,T_{4}]\land \operatorname {build-param-lists} [p,D,V,K_{4}]$ $\land T_{4}=[F_{4},S_{4},A_{4}]::[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[F_{3}]=A_{3}))\land D[F_{3}]=D[f]$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[F_{4}]=A_{4}))\land D[F_{4}]=K_{4}$ $D[p]=[F_{4},S_{4},A_{4}]::[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[F_{3}]=A_{3}))\land D[F_{3}]=D[f]$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[F_{4}]=A_{4}))\land D[F_{4}]=D[p]$ $\operatorname {build-param-lists} [x\ (q\ q\ x)),D,V,\_]$ Rule Expression Abstraction $\operatorname {build-param-lists} [\lambda q.\lambda x.x\ (q\ q\ x)),D,V,\_]$ Application $\operatorname {build-param-lists} [x\ (q\ q\ x)),D,V,K_{1}]$ Name $\operatorname {build-param-lists} [x,D,V,T_{5}]\land \operatorname {build-param-lists} [q\ q\ x,D,V,K_{5}]$ $\land T_{5}=[F_{5},S_{5},A_{5}]::\_$ $\land (S_{5}\implies (\operatorname {equate} [A_{5},q\ q\ x]\land V[F_{5}]=A_{5}))\land D[F_{5}]=K_{5}$ Name $\operatorname {build-param-lists} [q\ q\ x,D,V,K_{5}]$ $\land D[x]=[F_{5},S_{5},A_{5}]::\_$ $\land (S_{5}\implies (\operatorname {equate} [A_{5},q\ q\ x]\land V[F_{5}]=A_{5}))\land D[F_{5}]=K_{5}$ Name $\operatorname {build-param-lists} [q\ q,D,V,T_{6}]\land \operatorname {build-param-lists} [x,D,V,K_{6}]$ $\land T_{6}=[F_{6},S_{6},A_{6}]::K_{5}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=K_{6}$ Application $\operatorname {build-param-lists} [q\ q,D,V,T_{6}]$ $\land T_{6}=[F_{6},S_{6},A_{6}]::K_{5}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=D[x]$ Name $\operatorname {build-param-lists} [q,D,V,T_{7}]\land \operatorname {build-param-lists} [q,D,V,K_{7}]$ $\land T_{7}=[F_{7},S_{7},A_{7}]::[F_{6},S_{6},A_{6}]::K_{5}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=D[x]$ $\land (S_{7}\implies (\operatorname {equate} [A_{7},q]\land V[F_{7}]=A_{7}))\land D[F_{7}]=K_{7}$ Name $\operatorname {build-param-lists} [q,D,V,K_{7}]$ $\land D[q]=[F_{7},S_{7},A_{7}]::[F_{6},S_{6},A_{6}]::K_{5}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=D[x]$ $\land (S_{7}\implies (\operatorname {equate} [A_{7},q]\land V[F_{7}]=A_{7}))\land D[F_{7}]=D[q]$ After collecting the results together, $D[p]=[q,\_,\_]::[x,\_,\_]::L_{3}$ $D[p]=[F_{4},S_{4},A_{4}]::[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[F_{3}]=A_{3}))\land D[F_{3}]=D[f]$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[F_{4}]=A_{4}))\land D[F_{4}]=D[p]$ $D[q]=[F_{7},S_{7},A_{7}]::[F_{6},S_{6},A_{6}]::K_{5}$ $(S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=D[x]$ $(S_{7}\implies (\operatorname {equate} [A_{7},q]\land V[F_{7}]=A_{7}))\land D[F_{7}]=D[q]$ From the two definitions for $D[p]$; $F_{4}=q$ $F_{3}=x$ so $D[p]=[q,S_{4},A_{4}]::[x,S_{3},A_{3}]::K_{2}$ $(S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[x]=A_{3}))\land D[x]=D[f]$ $(S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[q]=A_{4}))\land D[q]=D[p]$ Using $D[q]=D[p]$ and $D[p]=[F_{7},S_{7},A_{7}]::[F_{6},S_{6},A_{6}]::K_{5}$ $(S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=D[x]$ $(S_{7}\implies (\operatorname {equate} [A_{7},q]\land V[F_{7}]=A_{7}))\land D[F_{7}]=D[q]$ by comparing with the above, $F_{7}=q,F_{6}=x,A_{3}=A_{6},A_{4}=A_{7},S_{3}=S_{6},S_{4}=S_{7}$ so, $V[x]=A_{3}$ $V[q]=A_{4}$ in, $S_{3}\implies A_{3}=f$ $S_{3}\implies (A_{3}=x\lor A_{3}=v[x])$ reduces to, $S_{3}\implies A_{3}=f$ also, $S_{4}\implies A_{4}=p$ $S_{4}\implies (A_{4}=q\lor A_{4}=v[q])$ reduces to, $S_{4}\implies A_{4}=p$ So the parameter list for p is effectively; $D[p]=[q,\_,p]::[x,\_,f]::\_$

Drop parameters

Use the information obtained by Build parameter lists to drop actual parameters that are no longer required. drop-params has the parameters,

• The lambda expression in which the parameters are to be dropped.
• The mapping of variable names to parameter lists (built in Build parameter lists).
• The set of variables free in the lambda expression.
• The returned parameter list. A parameter used internally in the algorithm.

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

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

where,

$F=FV[\lambda N.S]$

Variable

$\operatorname {drop-params} [N,D,V,D[N]]\equiv 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

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

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

Let - Let expression.

$\operatorname {drop-params} [\operatorname {let} V:E\operatorname {in} L]\equiv \operatorname {let} V:\operatorname {drop-params} [E,D,FV[E],[]]\operatorname {in} \operatorname {drop-params} [L,D,FV[L],[]]$

And - For use in "let".

$\operatorname {drop-params} [E\land F,D,V,\_]\equiv \operatorname {drop-params} [E,D,V,\_]\land \operatorname {drop-params} [F,D,V,\_]$

Drop parameters from applications

$\lambda g.\lambda n.n\ (g\ m\ p\ n)\ (g\ q\ p\ n)$ Condition Expression $\operatorname {drop-param} [\lambda g.\lambda n.n\ (g\ m\ p\ n)\ (g\ q\ p\ n),D,\{p,q,m\},\_]$ $\lambda g.\operatorname {drop-param} [\lambda n.n\ (g\ m\ p\ n)\ (g\ q\ p\ n),D,\{p,q,m\},\_]$ $\neg (\operatorname {def} [F_{1}]\land ...)$ $\lambda g.\lambda n.\operatorname {drop-param} [n\ (g\ m\ p\ n),D,\{p,q,m\},[F_{1},S_{1},A_{1}]::\_]\ \operatorname {drop-param} [(g\ q\ p\ n),D,\{p,q,m\},\_]$ $\neg (\operatorname {def} [F_{2}]\land ...)$ $\lambda g.\lambda n.\operatorname {drop-param} [n\ ,D,\{p,q,m\},[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_]\ \operatorname {drop-param} [(g\ m\ p\ n),D,\{p,q,m\},\_]\ \operatorname {drop-param} [(g\ q\ p\ n),D,\{p,q,m\},\_]$ $D[n]=[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_]$ $\lambda g.\lambda n.n\ \operatorname {drop-param} [(g\ m\ p\ n),D,\{p,q,m\},\_]\ \operatorname {drop-param} [(g\ q\ p\ n),D,\{p,q,m\},\_]$ From the results of building parameter lists; $D[n]=[[\_,\_,(g\ m\ p\ n)],[\_,\_,(g\ q\ p\ n)]]$ so, $F_{1}=\_$ $F_{2}=\_$ so, $\operatorname {def} [F_{1}]=\operatorname {false}$ $\operatorname {def} [F_{2}]=\operatorname {false}$ $\operatorname {drop-param} [(g\ m\ p\ n),D,\{p,q,m\},\_]$ Condition Expanded Expression $V=\{p,q,m\}$ $\operatorname {drop-param} [(g\ m\ p\ n),D,V,\_]$ $FV(A_{1})\not \subset \{p,q,m\}$ $n\not \subset \{p,q,m\}$ $\operatorname {drop-params} [g\ m\ p,D,V,[F_{1},S_{1},A_{1}]::\_]\ \operatorname {drop-params} [n,D,V,\_]$ $\operatorname {def} [F_{2}]\land \operatorname {ask} [S_{2}]\land FV[A_{2}]\subset V$ $\operatorname {def} [y]\land \operatorname {ask} [\_]\land FV[p]\subset \{p,q,m\}$ $\operatorname {drop-params} [g\ m,D,V,[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_]\ \operatorname {drop-params} [n,D,V,\_]$ $\neg \operatorname {ask} [S_{3}]$ $\neg \operatorname {ask} [\operatorname {false} ]$ $\operatorname {drop-params} [g,D,V,[F_{3},S_{3},A_{3}]::[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_]\ \operatorname {drop-params} [m,D,V,\_]\ \operatorname {drop-params} [n,D,V,\_]$ $D[g]=[[x,\operatorname {false} ,\_],[o,\_,p],[y,\_,n]]$ $=[F_{3},S_{3},A_{3}]::[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_]$ $F_{3}=x,S_{3}=\operatorname {false} ,A_{3}=\_$ $F_{2}=o,S_{2}=\_,A_{2}=p$ $F_{1}=y,S_{1}=\_,A_{1}=n$ $g\ m\ n$ $\operatorname {drop-param} [(g\ q\ p\ n),D,\{p,q,m\},\_]$ Condition Expanded Expression V = \{p, q, m\} $\operatorname {drop-param} [(g\ q\ p\ n),D,V,\_]$ $FV(A_{4})\not \subset V$ $n\not \subset \{p,q,m\}$ $\operatorname {drop-params} [g\ q\ p,D,V,[F_{4},S_{4},A_{4}]::\_]\ \operatorname {drop-params} [n,D,V,\_]$ $\operatorname {def} [F_{5}]\land \operatorname {ask} [S_{5}]\land FV[A_{5}]\subset V$ $\operatorname {def} [o]\land \operatorname {ask} [\_]\land p\subset \{p,q,m\})$ $\operatorname {drop-params} [g\ q,D,V,[F_{5},S_{5},A_{5}]::[F_{4},S_{4},A_{4}]::\_]\ \operatorname {drop-params} [n,D,V,\_]$ $\neg \operatorname {ask} [S-6]$ $\neg \operatorname {ask} [\operatorname {false} ]$ $\operatorname {drop-params} [g,D,V,[F_{6},S_{6},A_{6}]::[F_{5},S_{5},A_{5}]::[F_{4},S_{4},A_{4}]::\_]\ \operatorname {drop-params} [m,D,V,\_]\ \operatorname {drop-params} [n,D,V,\_]$ $D[g]=[[x,\operatorname {false} ,\_],[o,\_,p],[y,\_,n]]$ $=[F_{6},S_{6},A_{6}]::[F_{5},S_{5},A_{5}]::[F_{4},S_{4},A_{4}]::\_]$ $F_{6}=x,S_{6}=\operatorname {false} ,A_{6}=\_$ $F_{5}=o,S_{5}=\_,A_{5}=p$ $F_{4}=y,S_{4}=\_,A_{4}=n$ $g\ q\ n$

Drop formal parameters

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

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

drop-formal is defined as,

1. $(\operatorname {ask} [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],L]$
2. $\neg (\operatorname {ask} [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 its value.
2. else do not drop the parameter.
3. else return the body of the function.

Condition	Expression
$\operatorname {false}$	$\operatorname {drop-formal} [D,\lambda x.\lambda o.\lambda y.o\ x\ y,F]$
$\operatorname {true} \land \{p\}\subset F$	$\lambda x.\operatorname {drop-formal} [D,\lambda o.\lambda y.o\ x\ y,F]$
$\neg (\operatorname {true} \land \{n\}\subset F$)	$\lambda x.\operatorname {drop-formal} [D,(\lambda y.o\ x\ y)[o:=p],F]$
	$\lambda x.\lambda y.\operatorname {drop-formal} [D,p\ x\ y,F]$
	$\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$
abstract * 4	$\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-abstract-tran	$(\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

• Let expression
• Fixed-point combinator
• Lambda calculus
• Deductive lambda calculus
• Supercombinator
• Curry's paradox

External links

• Explanation on Stack Overflow, with a JavaScript example
• Some discussion of let expressions