Введение
Метапроцесс глобализации
Лямбда-лифтинг — это метапроцесс, реструктурирующий компьютерную программу таким образом, чтобы функции определялись независимо друг от друга в глобальной области видимости. Отдельный «лифт» преобразует локальную функцию в глобальную. Это двухэтапный процесс, состоящий из:
Устранения свободных переменных в функции путем добавления параметров. Перемещения функций из ограниченной области видимости в более широкую или глобальную. Термин «лямбда-лифтинг» был впервые введен Томасом Джонсоном около 1982 года и исторически рассматривался как механизм реализации функциональных языков программирования. Он используется в сочетании с другими техниками в некоторых современных компиляторах. Лямбда-лифтинг не тождественен преобразованию в замыкание. Он требует корректировки всех мест вызова (добавления дополнительных аргументов к вызовам) и не создает замыкание для преобразованной лямбда-функции. В отличие от этого, преобразование в замыкание не требует корректировки мест вызова, но создает замыкание для лямбда-выражения, сопоставляющее свободные переменные со значениями. Данную технику можно применять к отдельным функциям в процессе рефакторинга кода, чтобы сделать функцию доступной вне области, в которой она была написана. Лямбда-лифты также могут повторяться для преобразования программы. Многократные лифты могут использоваться для преобразования программы, написанной в лямбда-исчислении, в набор рекурсивных функций без использования лямбда-выражений. Это демонстрирует эквивалентность программ, написанных в лямбда-исчислении, и программ, написанных в виде функций. Однако это не доказывает корректность лямбда-исчисления для дедукции, поскольку эта-редукция, используемая в лямбда-лифтинге, является шагом, который вносит проблемы кардинальности в лямбда-исчисление, поскольку она удаляет значение из переменной, не проверяя сначала, что существует только одно значение, удовлетворяющее условиям на переменную (см. парадокс Карри). Лямбда-лифтинг требует значительных затрат времени обработки для компилятора. Эффективная реализация лямбда-лифтинга требует оптимизации времени обработки для компилятора. В нетипизированном лямбда-исчислении, где базовыми типами являются функции, лифтинг может изменить результат бета-редукции лямбда-выражения. Полученные функции будут иметь одинаковое значение в математическом смысле, но не будут считаться одной и той же функцией в нетипизированном лямбда-исчислении. См. также интенсиональное и экстенсиональное равенство. Обратной операцией к лямбда-лифтингу является лямбда-удаление. Лямбда-удаление может ускорить компиляцию программ для компилятора, а также повысить эффективность результирующей программы за счет уменьшения количества параметров и уменьшения размера стековых фреймов. Однако это затрудняет повторное использование функции. Удаленная функция привязана к своему контексту и может использоваться в другом контексте только после предварительного лифтинга.
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.
Подъем Ламбды против закрытия
Подъем лямбда-выражений и замыкания — это оба метода реализации программ с блочной структурой. Он реализует блочную структуру, устраняя её. Все функции поднимаются на глобальный уровень. Преобразование в замыкание обеспечивает "замыкание", которое связывает текущий контекст с другими контекстами. Преобразование в замыкание требует меньше времени компиляции. Рекурсивные функции и программы с блочной структурой, с подъемом или без него, могут быть реализованы с использованием реализации на основе стека, которая проста и эффективна. Однако реализация на основе стекового фрейма должна быть строгой (неотложной). Реализация на основе стекового фрейма требует, чтобы время жизни функций соответствовало принципу "последним пришел — первым ушел" (LIFO). То есть, функция, последняя начавшая вычисление, должна первой его завершить. Некоторые функциональные языки (например, Haskell) реализуются с использованием ленивых вычислений, которые откладывают вычисление до тех пор, пока значение не потребуется. Стратегия ленивой реализации предоставляет программисту гибкость. Ленивые вычисления требуют отсрочки вызова функции до тех пор, пока не будет сделан запрос на значение, вычисленное этой функцией. Один из способов реализации — сохранять ссылку на "контекст" данных, описывающий вычисление, вместо самого значения. Позже, когда значение потребуется, контекст используется для вычисления значения непосредственно перед его использованием. Вычисленное значение затем заменяет ссылку. "Контекст" похож на стековый фрейм, но отличается тем, что он не хранится в стеке. Ленивые вычисления требуют сохранения всех данных, необходимых для вычисления, в контексте. Если функция "поднята", то в контексте нужно сохранять только указатель на функцию и параметры этой функции. Некоторые современные языки используют сборку мусора вместо выделения памяти на основе стека для управления временем жизни переменных. В управляемой среде со сборкой мусора замыкание хранит ссылки на контексты, из которых могут быть получены значения. В отличие от этого, поднятая функция имеет параметры для каждого значения, необходимого для вычисления.
Подъем Ламбды в Ламбда-калькуле
Каждый лямбда-лифт берёт лямбда-абстракцию, являющуюся подвыражением лямбда-выражения, и заменяет её вызовом функции (применением) к функции, которую он создаёт. Свободные переменные в подвыражении становятся параметрами этого вызова функции. Лямбда-лифты могут применяться к отдельным функциям в процессе рефакторинга кода, чтобы сделать функцию доступной для использования за пределами области её определения. Эти преобразования могут повторяться до тех пор, пока выражение не избавится от всех лямбда-абстракций, что позволяет преобразовать программу.
Анонимный подъемник
Анонимный лифт принимает лямбда-абстракцию (обозначаемую S). Для S:
Создайте имя для функции, которая заменит S (обозначаемую V). Убедитесь, что имя, обозначаемое V, не использовалось ранее. Добавьте параметры к V для всех свободных переменных в S, чтобы создать выражение G (см. make call). Лямбда-лифт – это замена лямбда-абстракции S на применение функции, вместе с добавлением определения этой функции. В новом лямбда-выражении S заменяется на G. Обратите внимание, что L[S:=G] означает замену S на G в L. В определениях функций добавляется определение функции G = S. В указанном правиле G – это применение функции, которое заменяет выражение 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,
где V – имя функции. Оно должно быть новым, то есть именем, которое еще не используется в лямбда-выражении,
где – метафункция, возвращающая множество переменных, используемых в E.
Пример анонимного лифта. Например,
см. de lambda в преобразовании из лямбда-выражений в let-выражения. В результате,
Выбор выражения для подъема
Существует два различных способа, которыми выражение может быть выбрано для подъема. Первый рассматривает все лямбда-абстракции как определение анонимных функций. Второй рассматривает лямбда-абстракции, применяемые к параметру, как определение функции. Лямбда-абстракции, применяемые к параметру, имеют двойную интерпретацию: либо как выражение `let`, определяющее функцию, либо как определение анонимной функции. Обе интерпретации допустимы. Эти два предиката необходимы для обоих определений. `lambda free` – выражение, не содержащее лямбда-абстракций. `lambda anon` – анонимная функция. Выражение, такое как, где X не содержит лямбда-абстракций.