Лямбда көтеру: Бағдарлама құрылымын өзгерту әдісі

Globalization meta process
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 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.

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.

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.

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

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

where is a meta function that returns the set of variables used in E.

Example for anonymous lift. For example,

See de lambda in Conversion from lambda to let expressions. The result is,

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. lambda anon An anonymous function. An expression like where X is lambda free.