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

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

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

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

Выражение let присутствует во многих функциональных языках, чтобы обеспечить локальное определение выражения для использования при определении другого выражения. Выражение let присутствует в некоторых функциональных языках в двух формах; пусть или «дайте запись». Let Rec — это расширение простого выражения let, которое использует комбинатор с фиксированной точкой для реализации рекурсии .

История

Даны Скотт Язык LCF был этапом в эволюции лямбда-исчисления в современные функциональные языки. В этом языке появилось выражение let, которое с тех пор появилось в большинстве функциональных языков.

языков Схема , ML и, в последнее время, Haskell унаследовали выражения let от LCF.

Императивные языки с сохранением состояния, такие как АЛГОЛ и Паскаль, по существу реализуют выражение let для реализации ограниченного объема функций в блочных структурах.

Близко связанное предложение « where » вместе с его рекурсивным вариантом « where Rec » появилось уже в Питера Ландина книге «Механическая оценка выражений » .

Описание

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

Пусть выражение	Где пункт
Позволять $a=3$ и $b=4$ в ${\sqrt {a^{2}+b^{2}}}$	${\sqrt {a^{2}+b^{2}}}$ где $a=3$ и $b=4$

В обоих случаях вся конструкция представляет собой выражение, значение которого равно 5. Как и в случае if-then-else, тип, возвращаемый выражением, не обязательно является логическим.

Выражение let существует в 4 основных формах:

Форма	И	Рекурсивный	Определение/ограничение	Описание
Простой	Нет	Нет	Определение	Простое нерекурсивное определение функции.
Рекурсивный	Нет	Да	Определение	Определение рекурсивной функции (реализуется с помощью Y-комбинатора ).
Взаимный	Да	Да	Определение	Определение взаимно рекурсивной функции.
Математический	Да	Да	Ограничение	Математическое определение, поддерживающее общее логическое условие let.

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

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

Терминология, синтаксис и семантика варьируются от языка к языку. В Scheme let let используется для простой формы, а Rec — для рекурсивной формы. В ML let отмечает только начало блока объявлений, а fun отмечает начало определения функции. В Haskell пусть может быть взаимно рекурсивным, и компилятор определяет, что необходимо.

Определение

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

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

эквивалентно определению функции $f$ к $f\ x=y$ в выражении $z$, которое можно записать как выражение let ;

$\operatorname {let} f\ x=y\operatorname {in} z$

Выражение let можно понять как выражение естественного языка. Выражение let представляет собой замену значения переменной. Правило замены описывает последствия равенства как замены.

Пусть определение в математике

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

$(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F$

где E и F имеют логический тип.

Выражение let позволяет применить замену к другому выражению. Эту замену можно применять в ограниченной области, к подвыражению. Естественное использование выражения let применяется к ограниченной области действия (так называемое удаление лямбда-выражений ). Эти правила определяют, как может быть ограничена область действия;

${\begin{cases}x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)\\x\in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=(\operatorname {let} x:G\operatorname {in} E)\ F\\x\not \in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ F\end{cases}}$

где F не имеет типа Boolean . Из этого определения можно вывести следующее стандартное определение выражения let, используемое в функциональном языке.

$x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x:x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y$

Для простоты маркер, определяющий экзистенциальную переменную, $x:$, будет опущено в выражении, если это ясно из контекста.

$x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y$

Вывод

Чтобы получить этот результат, сначала предположим, что

$x\not \in \operatorname {FV} (L)$

затем

${\begin{aligned}L\ (\operatorname {let} x:x=y\operatorname {in} z)&\iff (\operatorname {let} x:x=y\operatorname {in} L\ z)\\&\iff x=y\land L\ z\end{aligned}}$

Используя правило замены,

${\begin{aligned}&\iff x=y\land (L\ z)[x:=y]\\&\iff x=y\land (L[x:=y]\ z[x:=y])\\&\iff x=y\land L\ z[x:=y]\\&\implies L\ z[x:=y]\end{aligned}}$

так что для всех L ,

$L\operatorname {let} x:x=y\operatorname {in} z\implies L\ z[x:=y]$

Позволять $L\ X=(X=K)$ где K — новая переменная. затем,

$(\operatorname {let} x:x=y\operatorname {in} z)=K\implies z[x:=y]=K$

Так,

$\operatorname {let} x:x=y\operatorname {in} z=z[x:=y]$

Но из математической интерпретации бета-редукции,

$(\lambda x.z)\ y=z[x:=y]$

Здесь, если y является функцией переменной x, это не тот же самый x, что и в z. Возможно применение альфа-переименования. Итак, мы должны иметь,

$x\not \in \operatorname {FV} (y)$

так,

$x\not \in \operatorname {FV} (y)\implies \operatorname {let} x:x=y\operatorname {in} z=(\lambda x.z)\ y$

Этот результат представляется на функциональном языке в сокращенной форме, где смысл однозначен;

$x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y$

Здесь переменная x неявно признается как частью уравнения, определяющего x, так и переменной в кванторе существования.

Никакого подъема из логического значения

Противоречие возникает, если E определяется формулой $E=\neg$. В этом случае,

$x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)$

становится,

$\operatorname {let} x:G\operatorname {in} \neg F=\neg \ (\operatorname {let} x:G\operatorname {in} F)$

и используя,

$(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F$

$(\exists xG\land \neg F)=\neg \ (\exists xG\land F)$

$=(\exists x\neg G\lor \neg F)$

Это неверно, если G ложно. Чтобы избежать этого противоречия, F не может иметь логический тип. Для логического значения F правильная формулировка правила отбрасывания использует импликацию вместо равенства:

$x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies (\operatorname {let} x:G\operatorname {in} E\ F\to E\ (\operatorname {let} x:G\operatorname {in} F))$

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

$(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F$

применяется только в том случае, если F является логическим. Сочетание двух правил создает противоречие, поэтому, если одно правило выполняется, другое — нет.

Объединение выражений let

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

$(\exists v\cdots \exists w\exists xE\land F)\iff \operatorname {let} v,\ldots ,w,x:E\operatorname {in} F$

тогда его можно вывести,

$x\not \in FV(E)\implies (\exists v\cdots \exists w\exists xE\land F)\iff (\exists v\cdots \exists w(E\land \exists xF))$

так,

$x\not \in FV(E)\implies (\operatorname {let} v,\ldots ,w,x:E\land F\operatorname {in} L\equiv \operatorname {let} v,\ldots ,w:E\operatorname {in} \operatorname {let} x:F\operatorname {in} L)$

Законы, связанные с лямбда-исчислением

Сокращение Eta дает правило для описания лямбда-абстракций. Это правило вместе с двумя полученными выше законами определяет связь между лямбда-исчислением и выражениями let.

Имя	Закон
Эта-редукционная эквивалентность	$f\ x=y\equiv f=\lambda x.y$
Let-лямбда-эквивалентность	$f\notin FV(E)\implies (\operatorname {let} f:f=E\operatorname {in} L\equiv (\lambda f.L)\ E)$ (где $f$ это имя переменной.)
Пусть комбинация	$x\notin FV(E)\implies (\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)$

Пусть определение определено из лямбда-исчисления

Чтобы избежать потенциальных проблем, связанных с математическим определением , Дана Скотт изначально определила выражение let из лямбда-исчисления. Это можно рассматривать как восходящее или конструктивное определение выражения let , в отличие от нисходящего или аксиоматического математического определения.

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

$(\operatorname {let} _{s}x=y\operatorname {in} z)\equiv (\lambda x.z)\ y$

Затем определение простого выражения let было расширено, чтобы обеспечить возможность рекурсии с использованием комбинатора с фиксированной точкой .

Комбинатор с фиксированной точкой

Комбинатор с фиксированной точкой может быть представлен выражением

$\lambda f.\operatorname {let} x=f\ x\operatorname {in} x$

Это представление может быть преобразовано в лямбда-терм. Лямбда-абстракция не поддерживает ссылку на имя переменной в прикладном выражении, поэтому x необходимо передать в качестве параметра x .

$\lambda f.\operatorname {let} x\ x=f\ (x\ x)\operatorname {in} x\ x$

Используя правило эта-редукции,

$f\ x=y\equiv f=\lambda x.y$

дает,

$\lambda f.\operatorname {let} x=\lambda x.f\ (x\ x)\operatorname {in} x\ x$

Выражение let может быть выражено как лямбда-абстракция, используя:

$n\not \in FV(E)\to (\operatorname {let} n=E\operatorname {in} L\equiv (\lambda n.L)\ E)$

дает,

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

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

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

Рекурсивное выражение let

Рекурсивное выражение let, называемое «let Rec», определяется с помощью комбинатора Y для рекурсивных выражений let.

$(\operatorname {let\ rec} x=y\operatorname {in} z)\equiv (\lambda x.z)\ (Y\ (\lambda x.y))$

Взаиморекурсивное выражение let

Затем этот подход обобщается для поддержки взаимной рекурсии. Взаимно рекурсивное выражение let может быть составлено путем перестановки выражения для удаления любых условий и. Это достигается путем замены нескольких определений функций одним определением функции, которое устанавливает список переменных, равный списку выражений. Версия комбинатора Y, называемая Y *. поливариатическим комбинатором с фиксированной точкой затем используется для одновременного вычисления фиксированной точки всех функций. Результатом является взаимно рекурсивная реализация выражения let .

Несколько значений

Выражение let может использоваться для представления значения, которое является членом набора.

$\operatorname {let} x\in X\operatorname {in} x$

При применении функции одного выражения let к другому,

${\begin{aligned}&(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} y\in Y\operatorname {in} y)\\&=\operatorname {let} x\in X\land y\in Y\operatorname {in} x\ y\\&=\operatorname {let} (x,y)\in X\times Y\operatorname {in} x\ y\end{aligned}}$

Но для применения выражения let к самому себе применяется другое правило.

${\begin{aligned}&(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} x\in X\operatorname {in} x)\\&=\operatorname {let} x\in X\operatorname {in} x\ x\end{aligned}}$

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

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

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

Правила преобразования между лямбда-исчислением и выражениями let

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

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

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

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

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

Преобразование из лямбда-выражений в let

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

1. $\operatorname {de-lambda} [V]\equiv V$
2. $\operatorname {de-lambda} [M\ N]\equiv \operatorname {de-lambda} [M]\ \operatorname {de-lambda} [N]$
3. $\operatorname {de-lambda} [F=\lambda P.E]\equiv \operatorname {de-lambda} [F\ P=E]$
4. $\operatorname {de-lambda} [E=F]\equiv \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]$
5. $\operatorname {de-lambda} [(\lambda F.E)L]\equiv \operatorname {let-combine} [\operatorname {let} F:\operatorname {de-lambda} [F=L]\operatorname {in} E]$
6. $V\not \in \operatorname {FV} [\lambda F.E]\to \operatorname {de-lambda} [\lambda F.E]\equiv \operatorname {let-combine} [\operatorname {let} V:\operatorname {de-lambda} [V\ F=E]\operatorname {in} V]$
7. $V\neq W\to \operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]\equiv \operatorname {let} V,W:E\land F\operatorname {in} G$
8. $\operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} F]\equiv \operatorname {let} V:E\operatorname {in} F$

Правило 6 создает уникальную переменную V в качестве имени функции.

Пример

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

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

преобразуется в,

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

Правило	showЛямбда-выражение
6	show$\operatorname {de-lambda} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]$ $V\not \in \operatorname {FV} [\lambda F.E]\to \operatorname {de-lambda} [\lambda F.E]$ $V=p,F=f,E=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$ $\operatorname {let-combine} [\operatorname {let} V:\operatorname {de-lambda} [V\ F=E]\operatorname {in} V]$
4	show$\operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\operatorname {in} p]$ $\operatorname {de-lambda} [p\ f=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]$ $\operatorname {de-lambda} [E=F]$ $E=p\ f,F=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$ $\operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]$ $\operatorname {de-lambda} [p\ f]=\operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]$ $\operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\operatorname {in} p]$
5	show$\operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\operatorname {in} p]$ $\operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]$ $\operatorname {de-lambda} [(\lambda F.E)L]$ $F=x,E=f\ (x\ x),L=(\lambda x.f\ (x\ x))$ $\operatorname {let-combine} [\operatorname {let} F:\operatorname {de-lambda} [F=L]\operatorname {in} E]$ $\operatorname {let-combine} [\operatorname {let} x:\operatorname {de-lambda} [x=\lambda x.f\ (x\ x)]\operatorname {in} f\ (x\ x)]$
3	show$\operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {let-combine} [\operatorname {let} x:\operatorname {de-lambda} [x=\lambda x.f\ (x\ x)]\operatorname {in} f\ (x\ x)]\operatorname {in} p]$ $\operatorname {de-lambda} [x=\lambda x.f\ (x\ x)]$ $\operatorname {de-lambda} [F=\lambda P.E]$ $F=x,P=x,E=f\ (x\ x)$ $\operatorname {de-lambda} [F\ P=E]$ $\operatorname {de-lambda} [x\ x=f\ (x\ x)]$
8	show$\operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {let-combine} [\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)]\operatorname {in} p]$ $\operatorname {let-combine} [\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)]$ $\operatorname {let-combine} [Y]$ $Y=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)$ $Y$ $\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)$
8	show$\operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)\operatorname {in} p]$ $\operatorname {let-combine} [Y]$ $Y=\operatorname {let} p:\operatorname {de-lambda} [p\ f=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)]\operatorname {in} p$ $Y$ $\operatorname {let} p:p\ f=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)\operatorname {in} p$
4	show$\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)\operatorname {in} p$ $\operatorname {de-lambda} [x\ x=f\ (x\ x)]$ $\operatorname {de-lambda} [E=F]$ $E=x\ x,F=f\ (x\ x)$ $\operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]$ $\operatorname {de-lambda} [x\ x]=\operatorname {de-lambda} [f\ (x\ x)]$
2	show$\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {let} x:\operatorname {de-lambda} [x\ x]=\operatorname {de-lambda} [f\ (x\ x)]\operatorname {in} f\ (x\ x)\operatorname {in} p$ $\operatorname {de-lambda} [x\ x],\operatorname {de-lambda} [f\ (x\ x)]$ $\operatorname {de-lambda} [p\ f],\operatorname {de-lambda} [M_{1}\ N_{1}],\operatorname {de-lambda} [M_{2}\ N_{2}],$ $M_{1}=p,N_{1}=f,M_{2}=x,N_{2}=x,M_{3}=f,N_{3}=x\ x$ $\operatorname {de-lambda} [M_{1}]\ \operatorname {de-lambda} [N_{1}],\operatorname {de-lambda} [M_{2}]\ \operatorname {de-lambda} [N_{2}],\operatorname {de-lambda} [M_{3}]\ \operatorname {de-lambda} [N_{3}]$ $\operatorname {de-lambda} [p]\ \operatorname {de-lambda} [f],\operatorname {de-lambda} [x]\ \operatorname {de-lambda} [x],\operatorname {de-lambda} [f]\ \operatorname {de-lambda} [x]\ \operatorname {de-lambda} [x]$
1	show$\operatorname {let} p:\operatorname {de-lambda} [p]\ \operatorname {de-lambda} [f]=\operatorname {let} x:\operatorname {de-lambda} [x]\ \operatorname {de-lambda} [x]=\operatorname {de-lambda} [f]\ (\operatorname {de-lambda} [x]\ \operatorname {de-lambda} [x])\operatorname {in} f\ (x\ x)]\operatorname {in} p$ $\operatorname {de-lambda} [V]$ $V$
	$\operatorname {let} p:p\ f=\operatorname {let} x:x\ x=f\ (x\ x)\operatorname {in} f\ (x\ x)]\operatorname {in} p$

Преобразование let в лямбда-выражения

Эти правила отменяют описанное выше преобразование. Они преобразуют выражение let в лямбда-выражение без изменения структуры. Не все выражения let можно преобразовать с использованием этих правил. Правила предполагают, что выражения уже упорядочены так, как если бы они были сгенерированы de-lambda .

1. $\operatorname {get-lambda} [F,G\ V=E]=\operatorname {get-lambda} [F,G=\lambda V.E]$
2. $\operatorname {get-lambda} [F,F=E]=\operatorname {de-let} [E]$
3. $\operatorname {de-let} [\lambda V.E]\equiv \lambda V.\operatorname {de-let} [E]$
4. $\operatorname {de-let} [M\ N]\equiv \operatorname {de-let} [M]\ \operatorname {de-let} [N]$
5. $\operatorname {de-let} [V]\equiv V$
6. $V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} V]\equiv \operatorname {get-lambda} [V,E]$
7. $V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]\equiv (\lambda V.\operatorname {de-let} [L])\ \operatorname {get-lambda} [V,E]$
8. $W\not \in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\ \operatorname {in} G]\equiv \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} \operatorname {let} W:F\ \operatorname {in} G]$
9. $V\in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ V=\operatorname {get-lambda} [V,E][V:=V\ V]\ \operatorname {in} L[V:=V\ V]]$
10. $W\in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\ \operatorname {in} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ W=\operatorname {get-lambda} [V,E][V:=V\ W]\ \operatorname {in} \operatorname {let} W:F[V:=V\ W]\ \operatorname {in} L[V:=V\ W]]$

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

Правил 8 и 10 достаточно для двух взаимно рекурсивных уравнений в выражении let . Однако они не будут работать для трех и более взаимно рекурсивных уравнений. В общем случае требуется дополнительный уровень циклов, что немного усложняет метафункцию. Следующие правила заменяют правила 8 и 10 при реализации общего случая. Правила 8 и 10 оставлены, чтобы сначала можно было изучить более простой случай.

1. лямбда-форма — преобразует выражение в комбинацию выражений, каждое из которых имеет вид переменная = выражение .
   1. $\operatorname {lambda-form} [G\ V=E]=\operatorname {lambda-form} [G=\lambda V.E]$
   2. $\operatorname {lambda-form} [E\land F]=\operatorname {lambda-form} [E]\land \operatorname {lambda-form} [F]$
   3. $\operatorname {lambda-form} [V=E]=V=E$ ...... где V — переменная.
2. lift-vars — Получите набор переменных, которым требуется X в качестве параметра, поскольку в выражении X является свободной переменной.
   1. $X\in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{V\}$
   2. $X\not \in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{\}$
   3. $\operatorname {lift-vars} [X,E\land F]=\operatorname {lift-vars} [X,E]\cup \operatorname {lift-vars} [X.F]$
3. подпеременные — для каждой переменной в наборе замените ее на переменную, примененную к X в выражении. Это делает X переменной, передаваемой в качестве параметра, а не свободной переменной в правой части уравнения.
   1. $\operatorname {sub-vars} [E,\{V\}\cup S,X]=\operatorname {sub-vars} [E[V:=V\ X],S,X]$
   2. $\operatorname {sub-vars} [E,\{\},X]=E$
4. de-let — Устранить каждое условие в E , чтобы X не было свободной переменной в правой части уравнения.
   1. ${\begin{aligned}L&=\operatorname {lambda-form} [E]\land S=\operatorname {lift-vars} [X,L]\to \operatorname {de-let} [\operatorname {let} V\ldots W,X:E\land F\ \operatorname {in} G]\\&\equiv \operatorname {de-let} [\operatorname {let} V\ldots W:\operatorname {sub-vars} [L,S,X]\ \operatorname {in} \operatorname {let} \operatorname {sub-vars} [\operatorname {lambda-form} [F],S,X]\ \operatorname {in} \operatorname {sub-vars} [G,S,X]]\end{aligned}}$

Примеры

Например, выражение let , полученное из комбинатора Y ,

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

преобразуется в,

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

Правило	showЛямбда-выражение
6	show$\operatorname {de-let} [\operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)\ \operatorname {in} p]$ $\operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} V]$ $V=p,E=p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)$ $\operatorname {get-lambda} [V,E]$
1	show$\operatorname {get-lambda} [p,p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)]$ $\operatorname {get-lambda} [F,G\ V=E]$ $F=p,G=p,V=f,E=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)$ $\operatorname {get-lambda} [F,G=\lambda V.E]$
2	show$\operatorname {get-lambda} [p,p=\lambda f.\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)]$ $\operatorname {get-lambda} [F,F=E]$ $F=p,E=\lambda f.\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)$ $\operatorname {de-let} [E]$
3	show$\operatorname {de-let} [\lambda f.\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)]$ $\operatorname {de-let} [\lambda V.E]$ $V=f,E=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)$ $\lambda V.\operatorname {de-let} [E]$
7	show$\lambda f.\operatorname {de-let} [\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)]$ $\operatorname {de-let} [\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)]$ $V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]$ $V=x,E=x\ q=f\ (q\ q),L=f\ (x\ x)$ $(\lambda V.\operatorname {de-let} [L])\ \operatorname {get-lambda} [V,E]$
4	show$(\lambda x.\operatorname {de-let} [f\ (x\ x)])\ \operatorname {get-lambda} [x,x\ q=f\ (q\ q)]$ $\operatorname {de-let} [f\ (x\ x)]$ $\operatorname {de-let} [M\ N]$ $M=f,N=(x\ x)$ $\operatorname {de-let} [M]\ \operatorname {de-let} [N]$ $\operatorname {de-let} [f]\ \operatorname {de-let} [x\ x]$
4	show$(\lambda x.\operatorname {de-let} [f]\ \operatorname {de-let} [x\ x])\ \operatorname {get-lambda} [x,x\ q=f\ (q\ q)]$ $\operatorname {de-let} [x\ x]$ $\operatorname {de-let} [M\ N]$ $M=x,N=x$ $\operatorname {de-let} [M]\ \operatorname {de-let} [N]$ $\operatorname {de-let} [x]\ \operatorname {de-let} [x]$
5	show$(\lambda x.\operatorname {de-let} [f]\ (\operatorname {de-let} [x]\ \operatorname {de-let} [x]))\ \operatorname {get-lambda} [x,x\ q=f\ (q\ q)]$ $\operatorname {de-let} [V]$ $V$
1	show$(\lambda x.f\ (x\ x))\ \operatorname {get-lambda} [x,x\ q=f\ (q\ q)]$ $\operatorname {get-lambda} [x,x\ q=f\ (q\ q)]$ $\operatorname {get-lambda} [F,G\ V=E]$ $F=x,G=x,V=q,E=f\ (q\ q)$ $\operatorname {get-lambda} [F,G=\lambda V.E]$ $\operatorname {get-lambda} [x,x=\lambda q.f\ (q\ q)]$
2	show$(\lambda x.f\ (x\ x))\ \operatorname {get-lambda} [x,x=\lambda q.f\ (q\ q)]$ $\operatorname {get-lambda} [x,x=\lambda q.f\ (q\ q)]$ $\operatorname {get-lambda} [F,F=E]$ $F=x,E=\lambda q.f\ (q\ q)$ $\operatorname {de-let} [E]$ $\operatorname {de-let} [\lambda q.f\ (q\ q)]$
3	show$(\lambda x.f\ (x\ x))\ \operatorname {de-let} [\lambda q.f\ (q\ q)]$ $\operatorname {de-let} [\lambda q.f\ (q\ q)]$ $\operatorname {de-let} [\lambda V.E]$ $V=q,E=f\ (q\ q)$ $\lambda V.\operatorname {de-let} [E]$ $\lambda q.\operatorname {de-let} [f\ (q\ q)]$
4	show$(\lambda x.f\ (x\ x))\ (\lambda q.\operatorname {de-let} [f\ (q\ q)])$ $\operatorname {de-let} [f\ (q\ q)]$ $\operatorname {de-let} [M_{1}\ N_{1}]$ $M_{1}=f,N_{1}=q\ q$ $\operatorname {de-let} [M_{1}]\ \operatorname {de-let} [N_{1}]$ $\operatorname {de-let} [f]\ \operatorname {de-let} [q\ q]$ $\operatorname {de-let} [M_{2}\ N_{2}]$ $M_{2}=q,N_{2}=q$ $\operatorname {de-let} [q]\ \operatorname {de-let} [q]$
5	show$(\lambda x.f\ (x\ x))\ (\lambda q.\operatorname {de-let} [f]\ (\operatorname {de-let} [q]\ \operatorname {de-let} [q]))$ $\operatorname {de-let} [V]$ ${\displaystyle }$ $V$
	$(\lambda x.f\ (x\ x))\ (\lambda q.f\ (q\ q))$

В качестве второго примера возьмем расширенную версию Y-комбинатора :

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

преобразуется в,

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

Правило	showЛямбда-выражение
8	$\operatorname {de-let} [\operatorname {let} p,q:p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p]$
7	$\operatorname {de-let} [\operatorname {let} p:p\ f\ x=f\ (x\ x)\ \operatorname {in} \operatorname {let} q:q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p]$
1, 2	$(\lambda p.\operatorname {de-let} [\operatorname {let} q:q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p])\ \operatorname {get-lambda} [p,p\ f\ x=f\ (x\ x)]$
7, 4, 5	$(\lambda p.\operatorname {de-let} [\operatorname {let} q:q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p])\ \lambda f.\lambda x.f\ (x\ x)$
1, 2	$(\lambda p.(\lambda q.q\ p)\ \operatorname {get-lambda} [q,q\ p\ f=(p\ f)\ (p\ f)])\ \lambda f.\lambda x.f\ (x\ x)$
	$(\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)$

В качестве третьего примера перевод:

$\operatorname {let} x:x\ f=f\ (x\ f)\ \operatorname {in} x$

является,

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

Правило	showЛямбда-выражение
9	$\operatorname {let} x:x\ f=f\ (x\ f)\ \operatorname {in} x$
1	$\operatorname {let} x:x\ x=\operatorname {get-lambda} [x,x\ f=f\ (x\ f)][x:=x\ x]\ \operatorname {in} x[x:=x\ x]$
2	$\operatorname {let} x:x\ x=\operatorname {get-lambda} [x,x=\lambda f.f\ (x\ f)][x:=x\ x]\ \operatorname {in} x\ x$
	$\operatorname {let} x:x\ x=(\lambda f.f\ (x\ f))[x:=x\ x]\ \operatorname {in} x\ x$
7	$\operatorname {let} x:x\ x=\lambda f.f\ (x\ x\ f)\ \operatorname {in} x\ x$
1	$(\lambda x.x\ x)\ \operatorname {get-lambda} [x,x\ x=\lambda f.f\ (x\ x\ f)]$
2	$(\lambda x.x\ x)\ \operatorname {get-lambda} [x,x=\lambda x.\lambda f.f\ (x\ x\ f)]$
	$(\lambda x.x\ x)\ (\lambda x.\lambda f.f\ (x\ x\ f))$

В качестве четвертого примера перевода:

$\operatorname {let} x:x=f\ x\ \operatorname {in} x$

является,

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

это знаменитый комбинатор y .

Правило	showЛямбда-выражение
9	$\operatorname {let} x:x=f\ x\ \operatorname {in} x$
2	$\operatorname {let} x:x\ x=\operatorname {get-lambda} [x,x=f\ x][x:=x\ x]\ \operatorname {in} x[x:=x\ x]$
	$\operatorname {let} x:x\ x=(f\ x)[x:=x\ x]\ \operatorname {in} x\ x$
7	$\operatorname {let} x:x\ x=f\ (x\ x)\ \operatorname {in} x\ x$
1	$(\lambda x.x\ x)\ \operatorname {get-lambda} [x,x\ x=f\ (x\ x)]$
2	$(\lambda x.x\ x)\ \operatorname {get-lambda} [x,x=\lambda x.f\ (x\ x)]$
	$(\lambda x.x\ x)\ (\lambda x.f\ (x\ x))$

Ключевые люди

• Дана Скотт

См. также

• Область применения (информатика)
• Лямбда лифтинг
• Комбинатор с фиксированной точкой
• Лямбда-исчисление
• Парадокс Карри
• Дедуктивное лямбда-исчисление
• Программирование логики ограничений
• Сужение наборов алгебраических значений

Ссылки

Цитируемые работы

• Митчелл, Джон К. (1996). Основы языков программирования . МТИ Пресс. ISBN  978-0-262-13321-0 .
• Плоткин, Г.Д. (декабрь 1977 г.). «LCF рассматривается как язык программирования» . Теоретическая информатика . 5 (3): 223–255. дои : 10.1016/0304-3975(77)90044-5 .