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

Эта статья требует дополнительных ссылок для проверки . Пожалуйста, помогите улучшить эту статью , добавив цитаты из надежных источников . Материал, не полученный от источника, может быть оспорен и удален. Найти источники:  «Let expression»  -  новости  · газеты  · книги  · ученый  · JSTOR ( март 2017 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения )

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

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

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

Выражение let присутствует во многих функциональных языках, чтобы разрешить локальное определение выражения для использования при определении другого выражения. Let-выражение присутствует в некоторых функциональных языках в двух формах; пусть или "пусть рек". Пусть rec является расширением простого выражения let, которое использует комбинатор с фиксированной точкой для реализации рекурсии .

История [ править ]

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

Языки Scheme , ^[2] ML и, совсем недавно, Haskell ^[3] унаследовали выражения let от LCF.

Императивные языки с отслеживанием состояния, такие как ALGOL и Pascal, по сути, реализуют выражение let для реализации ограниченного объема функций в блочных структурах. ^{[ необходима цитата ]}

Тесно связанное предложение where вместе с его рекурсивным вариантом where rec появилось уже в книге Питера Ландина « Механическое вычисление выражений» . ^[4]

Описание [ править ]

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

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

Выражение let бывает четырех основных форм:

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

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

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

Определение [ править ]

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

${\displaystyle (\lambda f.z)\ (\lambda x.y)}$

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

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

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

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

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

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

где E и F имеют тип Boolean.

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

${\displaystyle {\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, которое используется в функциональном языке.

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

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

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

Вывод [ править ]

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

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

тогда

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

Используя правило подстановки,

${\displaystyle {\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 ,

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

Пусть где K - новая переменная. тогда,${\displaystyle L\ X=(X=K)}$

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

Так,

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

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

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

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

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

так,

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

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

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

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

Нет лифтинга из логического [ править ]

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

${\displaystyle 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)}$

становится,

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

и используя,

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

${\displaystyle (\exists xG\land \neg F)=\neg \ (\exists xG\land F)}$

${\displaystyle =(\exists x\neg G\lor \neg F)}$

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

${\displaystyle 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))}$

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

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

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

Присоединение к let выражениям [ править ]

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

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

тогда это может быть получено,

${\displaystyle 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))}$

так,

${\displaystyle 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)}$

Законы, касающиеся лямбда-исчисления и let-выражений [ править ]

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

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

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

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

Комбинатор с фиксированной точкой [ править ]

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

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

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

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

Используя правило сокращения эта,

${\displaystyle f\ x=y\equiv f=\lambda x.y}$

дает,

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

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

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

дает,

${\displaystyle \lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x))}$

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

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

Рекурсивное выражение let [ править ]

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

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

Взаимно рекурсивное выражение let [ править ]

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

Несколько значений [ править ]

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

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

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

${\displaystyle (\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} y\in Y\operatorname {in} y)}$

${\displaystyle =\operatorname {let} x\in X\land y\in Y\operatorname {in} x\ y}$

${\displaystyle =\operatorname {let} (x,y)\in X\times Y\operatorname {in} x\ y}$

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

${\displaystyle (\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} x\in X\operatorname {in} x)}$

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

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

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

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

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

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

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

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

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

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

Преобразование из лямбда в выражения let [ править ]

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

1. ${\displaystyle \operatorname {de-lambda} [V]\equiv V}$
2. ${\displaystyle \operatorname {de-lambda} [M\ N]\equiv \operatorname {de-lambda} [M]\ \operatorname {de-lambda} [N]}$
3. ${\displaystyle \operatorname {de-lambda} [F=\lambda P.E]\equiv \operatorname {de-lambda} [F\ P=E]}$
4. ${\displaystyle \operatorname {de-lambda} [E=F]\equiv \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]}$
5. ${\displaystyle \operatorname {de-lambda} [(\lambda F.E)L]\equiv \operatorname {let-combine} [\operatorname {let} F:\operatorname {de-lambda} [F=L]\operatorname {in} E]}$
6. ${\displaystyle 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. ${\displaystyle 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. ${\displaystyle \operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} F]\equiv \operatorname {let} V:E\operatorname {in} F}$

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

Пример [ править ]

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

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

конвертируется в,

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

Правило	Лямбда-выражение
6	${\displaystyle \operatorname {de-lambda} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]}$ ${\displaystyle V\not \in \operatorname {FV} [\lambda F.E]\to \operatorname {de-lambda} [\lambda F.E]}$ ${\displaystyle V=p,F=f,E=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$ ${\displaystyle \operatorname {let-combine} [\operatorname {let} V:\operatorname {de-lambda} [V\ F=E]\operatorname {in} V]}$
4	${\displaystyle \operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\operatorname {in} p]}$ ${\displaystyle \operatorname {de-lambda} [p\ f=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]}$ ${\displaystyle \operatorname {de-lambda} [E=F]}$ ${\displaystyle E=p\ f,F=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$ ${\displaystyle \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]}$ ${\displaystyle \operatorname {de-lambda} [p\ f]=\operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]}$ ${\displaystyle \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	${\displaystyle \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]}$ ${\displaystyle \operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]}$ ${\displaystyle \operatorname {de-lambda} [(\lambda F.E)L]}$ ${\displaystyle F=x,E=f\ (x\ x),L=(\lambda x.f\ (x\ x))}$ ${\displaystyle \operatorname {let-combine} [\operatorname {let} F:\operatorname {de-lambda} [F=L]\operatorname {in} E]}$ ${\displaystyle \operatorname {let-combine} [\operatorname {let} x:\operatorname {de-lambda} [x=\lambda x.f\ (x\ x)]\operatorname {in} f\ (x\ x)]}$
3	${\displaystyle \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]}$ ${\displaystyle \operatorname {de-lambda} [x=\lambda x.f\ (x\ x)]}$ ${\displaystyle \operatorname {de-lambda} [F=\lambda P.E]}$ ${\displaystyle F=x,P=x,E=f\ (x\ x)}$ ${\displaystyle \operatorname {de-lambda} [F\ P=E]}$ ${\displaystyle \operatorname {de-lambda} [x\ x=f\ (x\ x)]}$
8	${\displaystyle \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]}$ ${\displaystyle \operatorname {let-combine} [\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)]}$ ${\displaystyle \operatorname {let-combine} [Y]}$ ${\displaystyle Y=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)}$ ${\displaystyle Y}$ ${\displaystyle \operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)}$
8	${\displaystyle \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]}$ ${\displaystyle \operatorname {let-combine} [Y]}$ ${\displaystyle 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}$ ${\displaystyle Y}$ ${\displaystyle \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	${\displaystyle \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}$ ${\displaystyle \operatorname {de-lambda} [x\ x=f\ (x\ x)]}$ ${\displaystyle \operatorname {de-lambda} [E=F]}$ ${\displaystyle E=x\ x,F=f\ (x\ x)}$ ${\displaystyle \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]}$ ${\displaystyle \operatorname {de-lambda} [x\ x]=\operatorname {de-lambda} [f\ (x\ x)]}$
2	${\displaystyle \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}$ ${\displaystyle \operatorname {de-lambda} [x\ x],\operatorname {de-lambda} [f\ (x\ x)]}$ ${\displaystyle \operatorname {de-lambda} [p\ f],\operatorname {de-lambda} [M_{1}\ N_{1}],\operatorname {de-lambda} [M_{2}\ N_{2}],}$ ${\displaystyle M_{1}=p,N_{1}=f,M_{2}=x,N_{2}=x,M_{3}=f,N_{3}=x\ x}$ ${\displaystyle \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}]}$ ${\displaystyle \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	${\displaystyle \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}$ ${\displaystyle \operatorname {de-lambda} [V]}$ ${\displaystyle V}$
	${\displaystyle \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. ${\displaystyle \operatorname {get-lambda} [F,G\ V=E]=\operatorname {get-lambda} [F,G=\lambda V.E]}$
2. ${\displaystyle \operatorname {get-lambda} [F,F=E]=\operatorname {de-let} [E]}$
3. ${\displaystyle \operatorname {de-let} [\lambda V.E]\equiv \lambda V.\operatorname {de-let} [E]}$
4. ${\displaystyle \operatorname {de-let} [M\ N]\equiv \operatorname {de-let} [M]\ \operatorname {de-let} [N]}$
5. ${\displaystyle \operatorname {de-let} [V]\equiv V}$
6. ${\displaystyle 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. ${\displaystyle 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. ${\displaystyle 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. ${\displaystyle 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. ${\displaystyle 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. ${\displaystyle \operatorname {lambda-form} [G\ V=E]=\operatorname {lambda-form} [G=\lambda V.E]}$
   2. ${\displaystyle \operatorname {lambda-form} [E\land F]=\operatorname {lambda-form} [E]\land \operatorname {lambda-form} [F]}$
   3. ${\displaystyle \operatorname {lambda-form} [V=E]=V=E}$...... где V - переменная.
2. lift-vars - получает набор переменных, которым требуется X в качестве параметра, потому что в выражении X является свободной переменной.
   1. ${\displaystyle X\in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{V\}}$
   2. ${\displaystyle X\not \in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{\}}$
   3. ${\displaystyle \operatorname {lift-vars} [X,E\land F]=\operatorname {lift-vars} [X,E]\cup \operatorname {lift-vars} [X.F]}$
3. sub-vars - для каждой переменной в наборе замените ее на переменную, примененную к X в выражении. Это делает X переменной, передаваемой в качестве параметра, вместо того, чтобы быть свободной переменной в правой части уравнения.
   1. ${\displaystyle \operatorname {sub-vars} [E,\{V\}\cup S,X]=\operatorname {sub-vars} [E[V:=V\ X],S,X]}$
   2. ${\displaystyle \operatorname {sub-vars} [E,\{\},X]=E}$
4. de-let - Поднять каждое условие в E, чтобы X не была свободной переменной в правой части уравнения.
   1. ${\displaystyle 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]}$

${\displaystyle \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]]}$

Примеры [ править ]

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

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

конвертируется в,

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda q.f\ (q\ q))}$

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