Лямбда лифтинг

Лямбда-лифтинг — это метапроцесс , который реструктурирует компьютерную программу так, что функции определяются независимо друг от друга в глобальной области видимости . Индивидуальный «лифт» преобразует локальную функцию в глобальную. Это двухэтапный процесс, состоящий из;

Устранение свободных переменных в функции путем добавления параметров.
Перемещение функций из ограниченной области в более широкую или глобальную.

Термин «лямбда-лифтинг» был впервые введен Томасом Джонссоном примерно в 1982 году и исторически рассматривался как механизм реализации языков функционального программирования . Он используется в сочетании с другими методами в некоторых современных компиляторах .

Лямбда-подъем — это не то же самое, что преобразование замыкания. Он требует всех сайтов вызовов настройки (добавления дополнительных аргументов к вызовам) и не вводит замыкание для поднятого лямбда-выражения. Напротив, преобразование замыкания не требует настройки сайтов вызовов, но вводит замыкание для лямбда-выражения, отображающего свободные переменные в значения.

Этот метод можно использовать для отдельных функций при рефакторинге кода , чтобы сделать функцию пригодной для использования за пределами области, в которой она была написана. Лямбда-подъемы также можно повторять, чтобы преобразовать программу. Повторяющиеся подъемы можно использовать для преобразования программы, написанной с использованием лямбда-исчисления , в набор рекурсивных функций без лямбда-выражений. Это демонстрирует эквивалентность программ, написанных с помощью лямбда-исчисления, и программ, написанных как функции. ^[1] Однако это не демонстрирует правильность лямбда-исчисления для вывода, поскольку эта-редукция, используемая в лямбда-подъеме, является шагом, который вводит проблемы мощности в лямбда-исчисление, поскольку оно удаляет значение из переменной без предварительной проверки того, что существует только одно значение, удовлетворяющее условиям переменной (см. парадокс Карри ).

Лямбда-подъем требует много времени для компилятора. Эффективная реализация лямбда-лифтинга $O(n^{2})$ о времени обработки компилятором. ^[2]

В нетипизированном лямбда-исчислении , где основными типами являются функции, подъем может изменить результат бета-редукции лямбда-выражения. Полученные функции будут иметь одно и то же значение в математическом смысле, но не считаются одной и той же функцией в нетипизированном лямбда-исчислении. См. также интенсиональное и экстенсиональное равенство .

Операция, обратная подъему лямбды, — это понижение лямбды . ^[3]

Удаление лямбда-выражений может ускорить компиляцию программ для компилятора, а также повысить эффективность получаемой программы за счет уменьшения количества параметров и размера кадров стека. Однако это затрудняет повторное использование функции. Отброшенная функция привязана к своему контексту и может использоваться в другом контексте только в том случае, если она была сначала поднята.

Алгоритм

Следующий алгоритм представляет собой один из способов лямбда-подъема произвольной программы на языке, который не поддерживает замыкания как объекты первого класса :

Переименуйте функции так, чтобы каждая функция имела уникальное имя.
Замените каждую свободную переменную дополнительным аргументом включающей функции и передавайте этот аргумент при каждом использовании функции.
Замените каждое определение локальной функции, не имеющей свободных переменных, идентичной глобальной функцией.
Повторяйте шаги 2 и 3, пока все свободные переменные и локальные функции не будут удалены.

Если в языке есть замыкания как объекты первого класса, которые можно передавать в качестве аргументов или возвращать из других функций, замыкание должно быть представлено структурой данных, которая фиксирует привязки свободных переменных.

Пример

Следующая программа OCaml вычисляет сумму целых чисел от 1 до 100:

let rec sum n =
  if n = 1 then
    1
  else
    let f x =
      n + x in
    f (sum (n - 1)) in
sum 100

( let rec заявляет sum как функция, которая может вызывать сама себя.) Функция f, которая добавляет аргумент sum к сумме чисел, меньших, чем аргумент, является локальной функцией. В рамках определения f n является свободной переменной. Начните с преобразования свободной переменной в параметр:

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

Затем поднимите f в глобальную функцию:

let rec f w x =
  w + x
and sum n =
  if n = 1 then
    1
  else
    f n (sum (n - 1)) in
sum 100

Ниже приведен тот же пример, на этот раз написанный на 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));
}

Лямбда-лифтинг против замыканий

Лямбда-подъем и закрытие — оба метода реализации блочно-структурированных программ. Он реализует блочную структуру, устраняя ее. Все функции подняты на глобальный уровень. Преобразование замыкания обеспечивает «замыкание», которое связывает текущий кадр с другими кадрами. Преобразование замыкания занимает меньше времени компиляции.

Рекурсивные функции и программы с блочной структурой, с подъемом или без него, могут быть реализованы с использованием реализации на основе стека , которая является простой и эффективной. Однако реализация на основе стекового фрейма должна быть строгой (нетерпеливой) . Реализация на основе стекового фрейма требует, чтобы функции функционировали по принципу «последним пришел — первым вышел» (LIFO). То есть самая последняя функция, начавшая вычисление, должна завершиться первой.

Некоторые функциональные языки (например, Haskell ) реализованы с использованием ленивых вычислений , которые откладывают вычисления до тех пор, пока не потребуется значение. Стратегия ленивой реализации дает программисту гибкость. Ленивая оценка требует задержки вызова функции до тех пор, пока не будет сделан запрос значения, рассчитанного функцией. Одна из реализаций заключается в записи ссылки на «кадр» данных, описывающих вычисление, вместо значения. Позже, когда значение потребуется, кадр используется для его вычисления как раз тогда, когда оно необходимо. Вычисленное значение затем заменяет эталонное значение.

«Кадр» похож на кадр стека , с той разницей, что он не хранится в стеке. Ленивая оценка требует, чтобы все данные, необходимые для расчета, были сохранены в кадре. Если функция «снята», то в кадр нужно записать только указатель функции и параметры функции. Некоторые современные языки используют сборку мусора вместо распределения на основе стека для управления временем существования переменных. В управляемой среде со сбором мусора замыкание записывает ссылки на кадры, из которых можно получить значения. Напротив, расширенная функция имеет параметры для каждого значения, необходимого для расчета.

Пусть выражения и лямбда-исчисление

Выражение Let полезно при описании подъема и опускания, а также при описании взаимосвязи между рекурсивными уравнениями и лямбда-выражениями. В большинстве функциональных языков есть выражения let. Кроме того, языки блочного программирования, такие как ALGOL и Pascal, схожи в том, что они также допускают локальное определение функции для использования в ограниченной области .

Использованное здесь выражение let представляет собой полностью взаимно рекурсивную версию let Rec , реализованную во многих функциональных языках.

Пусть выражения относятся к лямбда-исчислению . Лямбда-исчисление имеет простой синтаксис и семантику и хорошо подходит для описания лямбда-подъема. Удобно описывать подъем лямбды как перевод лямбда -выражения в let , а опускание лямбды — как обратный. Это связано с тем, что выражения let допускают взаимную рекурсию, что в некотором смысле более сложно, чем поддерживается в лямбда-исчислении. Лямбда-исчисление не поддерживает взаимную рекурсию, и в самой внешней глобальной области видимости может быть определена только одна функция.

Правила преобразования , описывающие перевод без поднятия, приведены в статье Выражение Let .

Следующие правила описывают эквивалентность лямбда-выражений и выражений let:

Имя	Закон
Эта-редукционная эквивалентность	$f\ x=y\equiv f=\lambda x.y$
Let-лямбда-эквивалентность	$f\notin FV(E)\to (\operatorname {let} f:f=E\operatorname {in} L\equiv (\lambda f.L)\ E)\ {\text{(where }}f{\text{ is a variable name.)}}$
Пусть комбинация	$x\notin FV(E)\to (\operatorname {let} v,\dots ,w,x:E\land F\operatorname {in} L\equiv \operatorname {let} v,\dots ,w:E\operatorname {in} \operatorname {let} x:F\operatorname {in} L)$

Будут даны метафункции, описывающие подъем и опускание лямбды. Метафункция — это функция, которая принимает программу в качестве параметра. Программа — это данные для метапрограммы. Программа и метапрограмма находятся на разных метауровнях.

Следующие соглашения будут использоваться для того, чтобы отличить программу от метапрограммы:

Квадратные скобки [] будут использоваться для обозначения применения функции в метапрограмме.
Для переменных в метапрограмме будут использоваться заглавные буквы. Строчные буквы обозначают переменные в программе.
$\equiv$ будет использоваться для равенства в метапрограмме.
$\_$ представляет фиктивную переменную или неизвестное значение.

Для простоты первое правило учитывает совпадения. Правила также предполагают, что лямбда-выражения были предварительно обработаны, поэтому каждая лямбда-абстракция имеет уникальное имя.

Оператор замены широко используется. Выражение $L[G:=S]$ означает замену каждого вхождения G в L на S и возврат выражения. Используемое определение расширено и включает замену выражений из определения, данного на странице лямбда-исчисления . Сопоставление выражений должно сравнивать выражения на альфа-эквивалентность (переименование переменных).

Лямбда-подъем в лямбда-исчислении

Каждый лямбда-лифтинг принимает лямбда-абстракцию, которая является подвыражением лямбда-выражения, и заменяет ее вызовом функции (приложением) для создаваемой функции. Свободные переменные в подвыражении являются параметрами вызова функции.

Лямбда-лифты можно использовать для отдельных функций при рефакторинге кода , чтобы сделать функцию пригодной для использования за пределами области, в которой она была написана. Такие подъемы также можно повторять до тех пор, пока в выражении не исчезнут лямбда-абстракции, чтобы преобразовать программу.

Лямбда-лифт

Подъему присваивается подвыражение внутри выражения для подъема на начало этого выражения. Выражение может быть частью более крупной программы. Это позволяет контролировать, куда поднимается подвыражение. Операция лямбда-подъема, используемая для выполнения подъема в программе:

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

Подвыражение может быть либо лямбда-абстракцией, либо лямбда-абстракцией, примененной к параметру.

Возможны два типа подъема.

Анонимный лифт имеет выражение лифта, которое представляет собой только лямбда-абстракцию. Это рассматривается как определение анонимной функции. Для функции необходимо создать имя.

Именованное выражение Lift имеет лямбда-абстракцию, примененную к выражению. Этот подъем рассматривается как именованное определение функции.

Анонимный лифт

Анонимный подъем использует лямбда-абстракцию (называемую S ). Для С ;

Создайте имя для функции, которая заменит S (называемую V ). Убедитесь, что имя, указанное V, не использовалось.
Добавьте параметры в V для всех свободных переменных в S , чтобы создать выражение G (см. make-call ).

Лямбда-лифтинг — это замена лямбда-абстракции S для приложения функции вместе с добавлением определения функции.

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

В новом лямбда-выражении G что L [ S := G ] означает замену S на G в L. заменен на S. Обратите внимание , В определения функций определение функции G = S. добавлено

В приведенном выше правиле G которое заменяется выражением S. — это приложение функции , Это определяется,

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

где V — имя функции. Это должна быть новая переменная, т. е. имя, еще не использованное в лямбда-выражении.

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

где $\operatorname {vars} [E]$ — это метафункция, которая возвращает набор переменных, используемых E. в

Пример анонимного подъема.
For example, ${\begin{aligned}F&=\operatorname {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} \operatorname {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)$

Построение звонка

Вызов функции G создается путем добавления параметров для каждой переменной из набора свободных переменных (представленного V ) к функции 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$

Пример построения звонка.
$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$

Именованный лифт

Именованный лифт аналогичен анонимному лифту, за исключением того, что имя функции V. указывается

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

Что касается анонимного лифта, выражение G строится из V путем применения свободных переменных S . Это определяется,

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

Пример именованного лифта.
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)$

Лямбда-лифт-преобразование

Преобразование лямбда-лифта принимает лямбда-выражение и поднимает все лямбда-абстракции в начало выражения. Затем абстракции преобразуются в рекурсивные функции , что устраняет лямбда-абстракции. В результате получается функциональная программа в виде,

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

где M — серия определений функций, а N — выражение, представляющее возвращаемое значение.

Например,

\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

Затем можно использовать метафункцию de-let для преобразования результата обратно в лямбда-исчисление.

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

Обработка преобразования лямбда-выражения представляет собой серию подъемов. Каждый лифт имеет,

Подвыражение, выбранное для него функциейlift -choice . Подвыражение следует выбирать так, чтобы его можно было преобразовать в уравнение без лямбда-выражений.
Подъем выполняется путем вызова метафункции лямбда-лифт , описанной в следующем разделе.

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

После установки лифтов квартиры объединяются в одну.

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

Затем удаление параметров применяется , чтобы удалить параметры, которые не нужны в выражении «let». Выражение let позволяет определениям функций напрямую ссылаться друг на друга, тогда как лямбда-абстракции строго иерархичны, и функция не может напрямую ссылаться на себя.

Выбор выражения для лифтинга

Существует два разных способа выбора выражения для подъема. Первый рассматривает все лямбда-абстракции как определяющие анонимные функции. Второй рассматривает лямбда-абстракции, применяемые к параметру, как определение функции. Лямбда-абстракции, применяемые к параметру, имеют двойную интерпретацию: либо как выражение let, определяющее функцию, либо как определяющее анонимную функцию. Обе интерпретации верны.

Эти два предиката необходимы для обоих определений.

без лямбды — выражение, не содержащее лямбда-абстракций.

{\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 x_{1}.\ ...\ \lambda x_{n}.X$ где X не содержит лямбды.

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

Выбор анонимных функций только для подъема

Найдите самую глубокую анонимную абстракцию, чтобы при применении подъема поднятая функция стала простым уравнением. Это определение не распознает лямбда-абстракции с параметром как определяющие функцию. Все лямбда-абстракции считаются определяющими анонимные функции.

Lift-Choice — первый аноним, найденный при обходе выражения, или нет , если функции нет.

$\operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X$
$\operatorname {lift-choice} [\lambda F.X]=\operatorname {lift-choice} [X]$
$\operatorname {lift-choice} [M]\neq \operatorname {none} \to \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [M]$
$\operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [N]$
$\operatorname {lift-choice} [V]=\operatorname {none}$

Например,

Выбор лямбды включен $\lambda f.(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))$ является $\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 f.(p\ f)\ (p\ f)$ является $\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)$

Выбор именованных и анонимных функций для подъема

Найдите самое глубокое именованное или анонимное определение функции, чтобы при применении подъема поднятая функция стала простым уравнением. Это определение распознает лямбда-абстракцию с фактическим параметром как определение функции. Только лямбда-абстракции без приложения считаются анонимными функциями.

лямбда-имя

Именованная функция. Выражение вроде

(\lambda F.M)\ N

где M не содержит лямбда-выражений, а N не содержит лямбда-выражений или анонимную функцию.

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

выбор лифта

Первая анонимная или именованная функция, найденная при обходе выражения, или нет, если функции нет.

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

Например,

Выбор лямбды включен $\lambda f.(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))$ является $(\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 f.f\ ((x\ f)\ (x\ f))$ является $\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))$

Примеры

Например, комбинатор Y ,

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

поднимается как,

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

и после удаления параметра ,

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

В качестве лямбда-выражения (см. Преобразование let в лямбда-выражения ),

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

Поднятие именованных и анонимных функций
	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\}$

Если поднимаются только анонимные функции, комбинатор Y:

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

и после удаления параметра ,

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

В качестве лямбда-выражения

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

Поднятие только анонимных функций
	Lambda Expression	Function	From	To	Variables
1	$\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$	true	$\lambda x.f\ (x\ x)$	$p\ f$	$\{x,f\}$
2	$(\lambda f.(\lambda x.f\ (x\ x))(\lambda x.f\ (x\ x)))[\lambda x.f\ (x\ x):=p\ f]$	$p\ f=\lambda x.f\ (x\ x)$			$\{x,f,p\}$
3	$\lambda f.(p\ f)\ (p\ f)$	$p\ f\ x=f\ (x\ x)$	$\lambda f.(p\ f)\ (p\ f)$	$q\ p$	$\{x,f,p\}$
4	$\lambda f.(p\ f)\ (p\ f)[\lambda f.(p\ f)\ (p\ f):=q\ p]$	$p\ f\ x=f\ (x\ x)\land q\ p=\lambda f.(p\ f)\ (p\ f)$			$\{x,f,p,q\}$
5	$q\ p$	$p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)$			$\{x,f,p,q\}$

Первое подвыражение, которое будет выбрано для подъема, — это $\lambda x.f\ (x\ x)$ . Это преобразует лямбда-выражение в $\lambda f.(p\ f)\ (p\ f)$ и создает уравнение $p\ f\ x=f(x\ x)$ .

Второе подвыражение, которое следует выбрать для подъема, — это $\lambda f.(p\ f)\ (p\ f)$ . Это преобразует лямбда-выражение в $q\ p$ и создает уравнение $q\ p\ f=(p\ f)\ (p\ f)$ .

И результат:

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

Удивительно, но этот результат проще, чем результат, полученный при поднятии именованных функций.

Исполнение

Примените функцию к $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}}

Так,

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

или

p\ K\ (p\ K)=K\ (p\ K\ (p\ K))

Y-Комбинатор неоднократно вызывает свой параметр (функцию) сам для себя. Значение определяется, если функция имеет фиксированную точку . Но функция никогда не завершится.

Выпадение лямбды в лямбда-исчислении

Падение лямбды ^[4] уменьшает область действия функций и использует контекст из уменьшенной области, чтобы уменьшить количество параметров функций. Уменьшение количества параметров упрощает понимание функций.

В разделе, посвященном подъему лямбда , была описана метафункция для первого подъема, а затем преобразования полученного лямбда-выражения в рекурсивное уравнение. Мета-функция Lambda Drop выполняет обратное, сначала преобразуя рекурсивные уравнения в лямбда-абстракции, а затем помещая полученное лямбда-выражение в наименьшую область видимости, охватывающую все ссылки на лямбда-абстракцию.

Удаление лямбды выполняется в два этапа:

Лямбда падение

Отбрасывание Lambda применяется к выражению, которое является частью программы. Удаление контролируется набором выражений, из которых удаление будет исключено.

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

где,

L — это лямбда-абстракция, которую нужно отбросить.

P — программа

X — набор выражений, которые необходимо исключить из удаления.

Преобразование капли лямбда

Преобразование лямбда-отбрасывания погружает все абстракции в выражение. Погружение исключено из выражений в наборе выражений,

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

где,

L — выражение, которое необходимо преобразовать.

X — это набор подвыражений, которые необходимо исключить из удаления.

«sink-tran» поглощает каждую абстракцию, начиная с самой внутренней,

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

Абстракция тонет

Погружение перемещает лямбда-абстракцию внутрь, насколько это возможно, так, чтобы она все еще находилась за пределами всех ссылок на переменную.

Заявление – 4 случая.

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

Абстракция . Используйте переименование, чтобы гарантировать, что все имена переменных различны.

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

Переменная – 2 случая.

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

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

Тест стока исключает отбрасывание выражений,

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

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

Пример

Пример затопления

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

Удаление параметров

Удаление параметра — это оптимизация функции по ее положению в функции. Лямбда-лифтинг добавил параметры, необходимые для того, чтобы функцию можно было вывести из контекста. При удалении этот процесс обратный, и дополнительные параметры, содержащие свободные переменные, могут быть удалены.

Удаление параметра — это удаление ненужного параметра из функции, при этом фактический передаваемый параметр всегда представляет собой одно и то же выражение. Свободные переменные выражения также должны быть свободными там, где определена функция. В этом случае отброшенный параметр заменяется выражением в теле определения функции. Это делает параметр ненужным.

Например, рассмотрим,

\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

В этом примере фактический параметр формального параметра o всегда равен p . Поскольку p — свободная переменная во всем выражении, параметр можно отбросить. Фактический параметр формального параметра y всегда равен n . Однако n связан с лямбда-абстракцией. Поэтому этот параметр нельзя отбрасывать.

Результатом удаления параметра будет:

\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

Для основного примера

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

Определение drop-params-tran таково:

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

где,

\operatorname {build-param-list} [L,D,V,\_]

Списки параметров сборки

Для каждой абстракции, определяющей функцию, создайте информацию, необходимую для принятия решения об удалении имен. Эта информация описывает каждый параметр; имя параметра, выражение для фактического значения и указание на то, что все выражения имеют одно и то же значение.

Например, в,

\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

параметры функции g :

Формальный параметр	Все одинаковое значение	Фактическое выражение параметра
х	ЛОЖЬ	_
тот	истинный	п
и	истинный	н

Каждая абстракция переименовывается с уникальным именем, а список параметров связывается с именем абстракции. Например, г есть список параметров.

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

build-param-lists создает все списки для выражения, просматривая выражение. Он имеет четыре параметра;

Анализируемое лямбда-выражение.
Параметр table перечисляет имена.
Таблица значений параметров.
Возвращаемый список параметров, который используется внутри

Абстракция — лямбда-выражение формы. $(\lambda N.S)\ L$ анализируется для извлечения имен параметров функции.

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

Найдите имя и начните создавать список параметров для этого имени, заполняя формальные имена параметров. Также получите любой фактический список параметров из тела выражения и верните его как фактический список параметров из этого выражения.

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

Переменная — вызов функции.

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

Для имени функции или параметра начните заполнение фактического списка параметров, выводя список параметров для этого имени.

Приложение . Приложение (вызов функции) обрабатывается для извлечения фактических сведений о параметрах.

\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

Получите списки параметров для выражения и параметра. Получите запись параметра из списка параметров из выражения и проверьте, соответствует ли текущее значение параметра этому параметру. Запишите значение имени параметра для последующего использования при проверке.

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

Приведенная выше логика довольно тонка в том, как она работает. Тот же индикатор значения никогда не имеет значения true. Значение false устанавливается только в том случае, если все значения не могут быть сопоставлены. Значение извлекается с помощью S для создания набора логических значений, разрешенных S. для Если true является членом, то все значения этого параметра равны, и параметр можно удалить.

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

Аналогично, def использует теорию множеств для запроса, присвоено ли переменной значение;

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

Пусть - Пусть выражение.

\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,\_]

И - Для использования в "пусть".

\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,\_]

Примеры

Например, построение списков параметров для,

\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[g]=[[x,\operatorname {false} ,\_],[o,\operatorname {true} ,p],[y,\operatorname {true} ,n]]

и параметр o опускается, чтобы дать:

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

Создайте список параметров для

\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

$\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]=\_

Другой пример:

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

Здесь x равен f. Сопоставление списка параметров:

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

и параметр x опускается, чтобы получить:

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

Создайте список параметров для

\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-params имеет параметры,

Лямбда-выражение, в которое нужно отбросить параметры.
Сопоставление имен переменных со списками параметров (встроенными в списки параметров сборки).
Набор переменных, свободных в лямбда-выражении.
Возвращаемый список параметров. Параметр, используемый внутри алгоритма.

Абстракция

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

где,

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

где,

F=FV[\lambda N.S]

Переменная

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

Для имени функции или параметра начните заполнение фактического списка параметров, выводя список параметров для этого имени.

Приложение . Приложение (вызов функции) обрабатывается для извлечения

(\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,\_]

Пусть - Пусть выражение.

\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],[]]

И - Для использования в "пусть".

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

Удаление параметров из приложений

$\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 удаляет формальные параметры на основе содержимого выпадающих списков. Его параметры:

Выпадающий список,
Определение функции (лямбда-абстракция).
Свободные переменные из определения функции.

дроп-формальный определяется как,

$(\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]$
$\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]$
$\operatorname {drop-formal} [Z,Y,V]\equiv Y$

Что можно объяснить так:

Если все фактические параметры имеют одинаковое значение и все свободные переменные этого значения доступны для определения функции, отбросьте параметр и замените старый параметр его значением.
иначе не удаляйте параметр.
else возвращает тело функции.

Состояние	Выражение
$\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$

Пример

Начиная с определения функции Y-комбинатора,

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

Трансформация	Выражение
	$\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p$
аннотация * 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 q.(\lambda p.q\ p)\ (\lambda f.\lambda x.f\ (x\ x)))\ (\lambda p.\lambda f.(p\ f)\ (p\ f))$
сток-тран	$(\lambda p.\lambda f.(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))$
отбросить параметр	$\lambda f.(\lambda p.p\ p)\ (\lambda x.f\ (x\ x))$
бета-редекс	$\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\$

Что возвращает комбинатор Y ,

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

См. также

Ссылки

^ Джонсон, Томас (1985). «Лямбда-лифтинг: преобразование программ в рекурсивные уравнения». В Жуанно, JP (ред.). Языки функционального программирования и архитектура компьютера. ФПКА 1985 . Конспекты лекций по информатике. Том. 201. Спрингер. CiteSeerX 10.1.1.48.4346 . дои : 10.1007/3-540-15975-4_37 . ISBN 3-540-15975-4 .
^ Морасан, Марко Т.; Шульц, Ульрик П. (2008), «Оптимальный лямбда-лифтинг за квадратичное время», Реализация и применение функциональных языков — переработанные избранные статьи , стр. 37–56, doi : 10.1007/978-3-540-85373-2_3 , ISBN 978-3-540-85372-5
^ Дэнви, О.; Шульц, УП (1997). «Лямбда-отбрасывание» . Уведомления ACM SIGPLAN . 32 (12): 90. дои : 10.1145/258994.259007 .
^ Дэнви, Оливье; Шульц, Ульрик П. (октябрь 2000 г.). «Отбрасывание лямбда-выражений: преобразование рекурсивных уравнений в программы с блочной структурой» (PDF) . Теоретическая информатика . 248 (1–2): 243–287. CiteSeerX 10.1.1.16.3943 . дои : 10.1016/S0304-3975(00)00054-2 . БРИКС-РС-99-27.

Внешние ссылки

Объяснение переполнения стека на примере JavaScript
Слоннегер, Кен; Курц, Барри. «5. Некоторое обсуждение выражений let» (PDF) . Основы языка программирования . Университет Айовы.

[1] Джонсон, Томас (1985). «Лямбда-лифтинг: преобразование программ в рекурсивные уравнения». В Жуанно, JP (ред.). Языки функционального программирования и архитектура компьютера. ФПКА 1985 . Конспекты лекций по информатике. Том. 201. Спрингер. CiteSeerX 10.1.1.48.4346 . дои : 10.1007/3-540-15975-4_37 . ISBN 3-540-15975-4 .

[Optimal_Lambda_Lifting_in_Quadratic_Time-2] Морасан, Марко Т.; Шульц, Ульрик П. (2008), «Оптимальный лямбда-лифтинг за квадратичное время», Реализация и применение функциональных языков — переработанные избранные статьи , стр. 37–56, doi : 10.1007/978-3-540-85373-2_3 , ISBN 978-3-540-85372-5

[3] Дэнви, О.; Шульц, УП (1997). «Лямбда-отбрасывание» . Уведомления ACM SIGPLAN . 32 (12): 90. дои : 10.1145/258994.259007 .

[4] Дэнви, Оливье; Шульц, Ульрик П. (октябрь 2000 г.). «Отбрасывание лямбда-выражений: преобразование рекурсивных уравнений в программы с блочной структурой» (PDF) . Теоретическая информатика . 248 (1–2): 243–287. CiteSeerX 10.1.1.16.3943 . дои : 10.1016/S0304-3975(00)00054-2 . БРИКС-РС-99-27.

[1]

[2]

[3]

[4]