Определение лямбда-исчисления - Lambda calculus definition

Для общего введения см. Лямбда-исчисление.

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

Стандартное определение

Это формальное определение было дано Церковь Алонсо.

Определение

Лямбда-выражения состоят из

• переменные ${\displaystyle v_{1}}$, ${\displaystyle v_{2}}$, ..., ${\displaystyle v_{n}}$, ...
• символы абстракции лямбда '${\displaystyle \lambda }$'и точка'. '
• скобки ( )

Набор лямбда-выражений, ${\displaystyle \Lambda }$, возможно определяется индуктивно:

1. Если ${\displaystyle x}$ переменная, то ${\displaystyle x\in \Lambda }$
2. Если ${\displaystyle x}$ переменная и ${\displaystyle M\in \Lambda }$, тогда ${\displaystyle (\lambda x.M)\in \Lambda }$
3. Если ${\displaystyle M,N\in \Lambda }$, тогда ${\displaystyle (M\ N)\in \Lambda }$

Экземпляры правила 2 известны как абстракции, а экземпляры правила 3 ​​- как приложения.^[1]

Обозначение

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

• Крайние круглые скобки опускаются: ${\displaystyle M\ N}$ вместо ${\displaystyle (M\ N)}$
• Предполагается, что приложения являются левоассоциативными: ${\displaystyle M\ N\ P}$ может быть написано вместо ${\displaystyle ((M\ N)\ P)}$^[2]
• Тело абстракции расширяется как можно правее: ${\displaystyle \lambda x.M\ N}$ средства ${\displaystyle \lambda x.(M\ N)}$ и нет ${\displaystyle (\lambda x.M)\ N}$
• Последовательность абстракций сокращается: ${\displaystyle \lambda x.\lambda y.\lambda z.N}$ сокращенно ${\displaystyle \lambda xyz.N}$^[3][4]

Свободные и связанные переменные

Оператор абстракции, ${\displaystyle \lambda }$, как говорят, связывает свою переменную везде, где она встречается в теле абстракции. Переменные, попадающие в область действия абстракции, называются граница. Все остальные переменные называются свободный. Например, в следующем выражении ${\displaystyle y}$ является связанной переменной и ${\displaystyle x}$ бесплатно: ${\displaystyle \lambda y.x\ x\ y}$. Также обратите внимание, что переменная связана своей «ближайшей» абстракцией. В следующем примере единственное вхождение ${\displaystyle x}$ в выражении связана второй лямбдой: ${\displaystyle \lambda x.y(\lambda x.z\ x)}$

Набор свободные переменные лямбда-выражения, ${\displaystyle M}$, обозначается как ${\displaystyle \operatorname {FV} (M)}$ и определяется рекурсией по структуре терминов следующим образом:

1. ${\displaystyle \operatorname {FV} (x)=\{x\}}$, куда ${\displaystyle x}$ это переменная
2. ${\displaystyle \operatorname {FV} (\lambda x.M)=\operatorname {FV} (M)\backslash \{x\}}$
3. ${\displaystyle \operatorname {FV} (M\ N)=\operatorname {FV} (M)\cup \operatorname {FV} (N)}$^[5]

Выражение, не содержащее свободных переменных, называется закрыто. Замкнутые лямбда-выражения также известны как комбинаторы и эквивалентны терминам в комбинаторная логика.

Снижение

Значение лямбда-выражений определяется тем, как выражения могут быть сокращены.^[6]

Есть три вида сокращения:

• α-преобразование: изменение связанных переменных (альфа);
• β-редукция: применение функций к их аргументам (бета);
• η-редукция: который отражает понятие протяженности (эта).

Мы также говорим о полученных эквивалентностях: два выражения β-эквивалент, если они могут быть β-преобразованы в одно и то же выражение, и α / η-эквивалентность определяется аналогично.

Период, термин редекс, Короче для сводимое выражение, относится к подтерминам, которые могут быть сокращены одним из правил сокращения. Например, ${\displaystyle (\lambda x.M)\ N}$ является β-редексом, выражающим замену ${\displaystyle N}$ за ${\displaystyle x}$ в ${\displaystyle M}$; если ${\displaystyle x}$ не бесплатно в ${\displaystyle M}$, ${\displaystyle \lambda x.M\ x}$ является η-редексом. Выражение, к которому сводится редекс, называется его редукцией; используя предыдущий пример, сокращения этих выражений соответственно ${\displaystyle M[x:=N]}$ и ${\displaystyle M}$.

α-преобразование

Альфа-преобразование, иногда известное как альфа-переименование,^[7] позволяет изменять имена связанных переменных. Например, альфа-преобразование ${\displaystyle \lambda x.x}$ может дать ${\displaystyle \lambda y.y}$. Термины, которые отличаются только альфа-преобразованием, называются α-эквивалент. Часто при использовании лямбда-исчисления α-эквивалентные термины считаются эквивалентными.

Точные правила альфа-преобразования не совсем тривиальны. Во-первых, при альфа-преобразовании абстракции переименовываются только вхождения переменных, которые связаны с той же абстракцией. Например, альфа-преобразование ${\displaystyle \lambda x.\lambda x.x}$ может привести к ${\displaystyle \lambda y.\lambda x.x}$, но это могло нет результат в ${\displaystyle \lambda y.\lambda x.y}$. Последний имеет значение, отличное от оригинала.

Во-вторых, альфа-преобразование невозможно, если оно приведет к захвату переменной другой абстракцией. Например, если мы заменим ${\displaystyle x}$ с ${\displaystyle y}$ в ${\displaystyle \lambda x.\lambda y.x}$, мы получили ${\displaystyle \lambda y.\lambda y.y}$, что совсем не одно и то же.

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

Замена

Замена, письменная ${\displaystyle E[V:=R]}$, - это процесс замены всех свободных вхождений переменной ${\displaystyle V}$ в выражении ${\displaystyle E}$ с выражением ${\displaystyle R}$. Подстановка терминов лямбда-исчисления определяется рекурсией по структуре терминов следующим образом (примечание: x и y - только переменные, а M и N - любое выражение λ).

${\displaystyle {\begin{aligned}x[x:=N]&\equiv N\\y[x:=N]&\equiv y{\text{, if }}x\neq y\end{aligned}}}$

${\displaystyle {\begin{aligned}(M_{1}\ M_{2})[x:=N]&\equiv (M_{1}[x:=N])\ (M_{2}[x:=N])\\(\lambda x.M)[x:=N]&\equiv \lambda x.M\\(\lambda y.M)[x:=N]&\equiv \lambda y.(M[x:=N]){\text{, if }}x\neq y{\text{, provided }}y\notin FV(N)\end{aligned}}}$

Чтобы заменить лямбда-абстракцию, иногда необходимо α-преобразовать выражение. Например, это неверно для ${\displaystyle (\lambda x.y)[y:=x]}$ привести к ${\displaystyle (\lambda x.x)}$, потому что замененный ${\displaystyle x}$ должен был быть свободным, но оказался связанным. Правильная замена в этом случае - ${\displaystyle (\lambda z.x)}$, с точностью до α-эквивалентности. Обратите внимание, что подстановка определена однозначно с точностью до α-эквивалентности.

β-редукция

β-редукция отражает идею применения функции. β-восстановление определяется в терминах замещения: β-восстановление ${\displaystyle ((\lambda V.E)\ E')}$ является ${\displaystyle E[V:=E']}$.

Например, предполагая некоторую кодировку ${\displaystyle 2,7,\times }$, имеем следующую β-редукцию: ${\displaystyle ((\lambda n.\ n\times 2)\ 7)\rightarrow 7\times 2}$.

η-редукция

η-редукция выражает идею протяженность, что в данном контексте состоит в том, что две функции одинаковы если и только если они дают одинаковый результат для всех аргументов. η-редукция преобразует ${\displaystyle \lambda x.(fx)}$ и ${\displaystyle f}$ в любое время ${\displaystyle x}$ не кажется свободным в ${\displaystyle f}$.

Нормализация

Основная статья: Бета нормальная форма

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

Лямбда-выражение, которое не может быть уменьшено ни с помощью β-redex, ни η-redex, находится в нормальной форме. Обратите внимание, что альфа-преобразование может преобразовывать функции. Все нормальные формы, которые могут быть преобразованы друг в друга посредством α-преобразования, считаются равными. См. Основную статью о Бета нормальная форма для подробностей.

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

Стратегия оценки

Дальнейшая информация: Стратегия оценки

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

Полные β-редукции

Любой редекс можно уменьшить в любой момент. По сути, это означает отсутствие какой-либо конкретной стратегии сокращения - в отношении сводимости «все ставки выключены».

Заявочный порядок

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

Большинство языков программирования (включая Lisp, ML и императивные языки, такие как C и Ява ) описываются как "строгие", что означает, что функции, применяемые к ненормализующим аргументам, не являются нормализующими. По сути, это делается с использованием аппликативного порядка, вызывая уменьшение значения (Смотри ниже ), но обычно это называется «нетерпеливой оценкой».

Нормальный порядок

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

Звоните по цене

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

Звоните по имени

В обычном порядке, но внутри абстракций сокращения не выполняются. Например, ${\displaystyle \lambda x.(\lambda x.x)x}$ находится в нормальной форме в соответствии с этой стратегией, хотя и содержит редекс ${\displaystyle (\lambda x.x)x}$.

Звоните по необходимости

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

Аппликативный порядок - это не нормализующая стратегия. Обычный контрпример выглядит следующим образом: определить ${\displaystyle \Omega =\omega \omega }$ куда ${\displaystyle \omega =\lambda x.xx}$. Все это выражение содержит только один редекс, а именно все выражение; его редукция снова ${\displaystyle \Omega }$. Поскольку это единственное доступное сокращение, ${\displaystyle \Omega }$ не имеет нормальной формы (при любой стратегии оценки). Используя аппликативный порядок, выражение ${\displaystyle KI\Omega =(\lambda x.\lambda y.x)(\lambda x.x)\Omega }$ уменьшается первым уменьшением ${\displaystyle \Omega }$ к нормальной форме (так как это крайний правый редекс), но поскольку ${\displaystyle \Omega }$ не имеет нормальной формы, аппликативный порядок не может найти нормальную форму для ${\displaystyle KI\Omega }$.

Напротив, нормальный порядок называется так потому, что он всегда находит нормализующее сокращение, если оно существует. В приведенном выше примере ${\displaystyle KI\Omega }$ уменьшается в обычном порядке до ${\displaystyle I}$, нормальная форма. Недостатком является то, что редексы в аргументах могут быть скопированы, что приведет к дублированию вычислений (например, ${\displaystyle (\lambda x.xx)((\lambda x.x)y)}$ сводится к ${\displaystyle ((\lambda x.x)y)((\lambda x.x)y)}$ используя эту стратегию; теперь есть два редекса, поэтому для полной оценки требуется еще два шага, но если бы аргумент был уменьшен первым, теперь не было бы ни одного).

Положительный компромисс использования аппликативного порядка состоит в том, что он не вызывает ненужных вычислений, если используются все аргументы, потому что он никогда не заменяет аргументы, содержащие редексы, и, следовательно, никогда не нужно их копировать (что может дублировать работу). В приведенном выше примере в аппликативном порядке ${\displaystyle (\lambda x.xx)((\lambda x.x)y)}$ сначала сводится к ${\displaystyle (\lambda x.xx)y}$ а затем в обычном порядке ${\displaystyle yy}$, делая два шага вместо трех.

Наиболее чисто функциональные языки программирования (особенно Миранда и его потомков, включая Haskell), а также языки доказательства средства доказательства теорем, использовать ленивая оценка, что по сути то же самое, что и вызов по необходимости. Это похоже на обычное сокращение порядка, но при вызове по необходимости удается избежать дублирования работы, присущего нормальному уменьшению порядка с использованием обмен. В приведенном выше примере ${\displaystyle (\lambda x.xx)((\lambda x.x)y)}$ сводится к ${\displaystyle ((\lambda x.x)y)((\lambda x.x)y)}$, который имеет два редекса, но при вызове по необходимости они представляются с использованием одного и того же объекта, а не копируются, поэтому, когда один редексируется, другой тоже.

Определение синтаксиса в BNF

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

Имя	BNF	Описание
Абстракция	<выражение> ::= λ <список переменных> . <выражение>	Определение анонимной функции.
Срок подачи заявки	<выражение> ::= <срок подачи заявления>
Заявление	<срок подачи заявления> ::= <срок подачи заявления> <элемент>	Вызов функции.
Элемент	<срок подачи заявления> ::= <элемент>
Переменная	<элемент> ::= <Переменная>	Например. х, у, факт, сумма, ...
Группировка	<элемент> ::= ( <выражение> )	Выражение в скобках.

Список переменных определяется как,

 <список переменных> := <Переменная> | <Переменная>, <список переменных>

Синтаксис переменной, используемой учеными-компьютерщиками,

 <Переменная> ::= <альфа> <расширение> <расширение> ::=  <расширение> ::= <extension-char> <расширение>  <extension-char> ::= <альфа> | <цифра> | _

Иногда математики ограничивают переменную одним буквенным символом. При использовании этого соглашения запятая в списке переменных опускается.

Лямбда-абстракция имеет более низкий приоритет, чем приложение, поэтому;

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

Приложения остаются ассоциативными;

${\displaystyle x\ y\ z=(x\ y)\ z}$

Абстракция с несколькими параметрами эквивалентна нескольким абстракциям одного параметра.

${\displaystyle \lambda x.y.z=\lambda x.\lambda y.z}$

куда,

• x - переменная
• y - список переменных
• z это выражение

Определение в виде математических формул

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

Семантика

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

1. α-преобразование - ${\displaystyle \operatorname {alpha-conv} (a)\to \operatorname {canonym} [A,P]=\operatorname {canonym} [a[A],P]}$
2. β-восстановление - ${\displaystyle \operatorname {beta-redex} [\lambda p.b\ v]=b[p:=v]}$
3. η-редукция - ${\displaystyle x\not \in \operatorname {FV} (f)\to \operatorname {eta-redex} [\lambda x.(f\ x)]=f}$

куда,

• каноним - это переименование лямбда-выражения для присвоения стандартным именам выражений в зависимости от положения имени в выражении.
• Оператор замены, ${\displaystyle b[p:=v]}$ это подмена имени ${\displaystyle p}$ с помощью лямбда-выражения ${\displaystyle v}$ в лямбда-выражении ${\displaystyle b}$.
• Бесплатный набор переменных ${\displaystyle \operatorname {FV} (f)}$ - это набор переменных, не принадлежащих лямбда-абстракции в ${\displaystyle f}$.

Выполнение заключается в выполнении β-редукции и η-редукции для подвыражений в канониме лямбда-выражения до тех пор, пока результатом не станет лямбда-функция (абстракция) в нормальная форма.

Все α-преобразования λ-выражения считаются эквивалентными.

Каноним - канонические имена

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

${\displaystyle {\begin{aligned}\operatorname {canonym} [L,Q]&=\operatorname {canonym} [L,O,Q]\\\operatorname {canonym} [\lambda p.b,M,Q]&=\lambda \operatorname {name} (Q).\operatorname {canonym} [b,M[p:=Q],Q+N]\\\operatorname {canonym} [X\ Y,x,Q]&=\operatorname {canonym} [X,x,Q+F]\ \operatorname {canonym} [Y,x,E+S]\\\operatorname {canonym} [x,M,Q]&=\operatorname {name} (M[x])\end{aligned}}}$

Где N - это строка «N», F - это строка «F», S - это строка «S», + - конкатенация, а «name» преобразует строку в имя.

Операторы карты

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

1. ${\displaystyle O[x]=x}$
2. ${\displaystyle M[x:=y][x]=y}$
3. ${\displaystyle x\neq z\to M[x:=y][z]=M[z]}$

Оператор подстановки

Если L - лямбда-выражение, x - это имя, а y - лямбда-выражение;${\displaystyle L[x:=y]}$ означает заменить x на y в L. Правила таковы,

1. ${\displaystyle (\lambda p.b)[x:=y]=\lambda p.b[x:=y]}$
2. ${\displaystyle (X\,Y)[x:=y]=X[x:=y]\,Y[x:=y]}$
3. ${\displaystyle z=x\to (z)[x:=y]=y}$
4. ${\displaystyle z\neq x\to (z)[x:=y]=z}$

Обратите внимание, что правило 1 необходимо изменить, если оно будет использоваться в неканонически переименованных лямбда-выражениях. Видеть Изменения в операторе подстановки.

Свободные и связанные наборы переменных

Набор свободные переменные лямбда-выражения M обозначается как FV (M). Это набор имен переменных, экземпляры которых не связаны (не используются) в лямбда-абстракции внутри лямбда-выражения. Это имена переменных, которые могут быть связаны с переменными формальных параметров извне лямбда-выражения.

Набор связанные переменные лямбда-выражения M обозначается как BV (M). Это набор имен переменных, экземпляры которых связаны (используются) в лямбда-абстракции внутри лямбда-выражения.

Правила для двух наборов приведены ниже.^[5]

${\displaystyle \mathrm {FV} (M)}$ - Бесплатный набор переменных	Комментарий	${\displaystyle \mathrm {BV} (M)}$ - Связанный набор переменных	Комментарий
${\displaystyle \mathrm {FV} (x)=\{x\}}$	где x - переменная	${\displaystyle \mathrm {BV} (x)=\emptyset }$	где x - переменная
${\displaystyle \mathrm {FV} (\lambda x.M)=\mathrm {FV} (M)\setminus \{x\}}$	Свободные переменные M без x	${\displaystyle \mathrm {BV} (\lambda x.M)=\mathrm {BV} (M)\cup \{x\}}$	Связанные переменные M плюс x.
${\displaystyle \mathrm {FV} (M\ N)=\mathrm {FV} (M)\cup \mathrm {FV} (N)}$	Объедините свободные переменные из функции и параметра	${\displaystyle \mathrm {BV} (M\ N)=\mathrm {BV} (M)\cup \mathrm {BV} (N)}$	Объедините связанные переменные из функции и параметра

Использование;

• Свободный набор переменных, FV используется выше в определение η-редукции.
• Набор связанных переменных, BV, используется в правиле для β-редекс неканонического лямбда-выражения.

Стратегия оценки

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

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

Запуск или оценка лямбда-выражения L является,

${\displaystyle \operatorname {eval} [\operatorname {canonym} [L],Q]}$

куда Q это префикс имени, возможно, пустая строка и оценка определяется как,

${\displaystyle {\begin{aligned}\operatorname {eval} [x\ y]&=\operatorname {eval} [\operatorname {apply} [\operatorname {eval} [x]\ \operatorname {strategy} [y]]]\\\operatorname {apply} [(\lambda x.y)\ z]&=\operatorname {canonym} [\operatorname {beta-redex} [(\lambda x.y)\ z],x]\\\operatorname {apply} [x]&=x{\text{ if x does match the above.}}\\\operatorname {eval} [\lambda x.(f\ x)]&=\operatorname {eval} [\operatorname {eta-redex} [\lambda x.(f\ x)]]\\\operatorname {eval} [L]&=L\\\operatorname {lazy} [X]&=X\\\operatorname {eager} [X]&=\operatorname {eval} [X]\end{aligned}}}$

Тогда стратегия оценки может быть выбрана как:

${\displaystyle {\begin{aligned}\operatorname {strategy} &=\operatorname {lazy} \\\operatorname {strategy} &=\operatorname {eager} \end{aligned}}}$

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

Нормальная форма

Были применены все возможные сокращения. Это результат применения энергичной оценки.

${\displaystyle {\begin{aligned}\operatorname {normal} [(\lambda x.y)\ z]&=\operatorname {false} \\\operatorname {normal} [\lambda x.(f\ x)]&=\operatorname {false} \\\operatorname {normal} [x\ y]&=\operatorname {normal} [x]\land \operatorname {normal} [y]\end{aligned}}}$

Во всех остальных случаях

${\displaystyle \operatorname {normal} [x]=\operatorname {true} }$

Слабая голова нормальной формы

Были применены сокращения функции (головы), но не все сокращения параметра. Это результат, полученный в результате применения ленивых вычислений.

${\displaystyle {\begin{aligned}\operatorname {whnf} [(\lambda x.y)\ z]&=\operatorname {false} \\\operatorname {whnf} [\lambda x.(f\ x)]&=\operatorname {false} \\\operatorname {whnf} [x\ y]&=\operatorname {whnf} [x]\end{aligned}}}$

Во всех остальных случаях

${\displaystyle \operatorname {whnf} [x]=\operatorname {true} }$

Вывод стандарта из математического определения

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

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

Это определение вводит правила, используемые в стандартном определении, и объясняет их с точки зрения определения канонического переименования.

Свободные и связанные переменные

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

Переменные в лямбда-выражении могут быть «связанными» или «свободными». Связанные переменные - это имена переменных, которые уже прикреплены к переменным формальных параметров в выражении.

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

Например, в следующем выражении y - связанная переменная, а x - свободная: ${\displaystyle \lambda y.x\ x\ y}$. Также обратите внимание, что переменная привязана к своей «ближайшей» лямбда-абстракции. В следующем примере единственное вхождение x в выражении связано со второй лямбдой: ${\displaystyle \lambda x.y\ (\lambda x.z\ x)}$

Изменения в операторе подстановки

В определении Оператор замены правило,

• ${\displaystyle (\lambda p.b)[x:=y]=\lambda p.b[x:=y]}$

необходимо заменить на,

1. ${\displaystyle (\lambda x.b)[x:=y]=\lambda x.b}$
2. ${\displaystyle z\neq x\ \to (\lambda z.b)[x:=y]=\lambda z.b[x:=y]}$

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

Например, предыдущие правила были бы неправильно переведены,

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

Новые правила блокируют эту замену, поэтому она остается как,

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

Трансформация

Значение лямбда-выражений определяется тем, как выражения могут быть преобразованы или сокращены.^[6]

Есть три вида трансформации:

• α-преобразование: изменение связанных переменных (альфа);
• β-редукция: применение функций к их аргументам (бета), вызывающие функции;
• η-редукция: который отражает понятие протяженности (эта).

Мы также говорим о полученных эквивалентностях: два выражения β-эквивалент, если они могут быть β-преобразованы в одно и то же выражение, и α / η-эквивалентность определяется аналогично.

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

α-преобразование

Альфа-преобразование, иногда известное как альфа-переименование,^[7] позволяет изменять имена связанных переменных. Например, альфа-преобразование ${\displaystyle \lambda x.x}$ может дать ${\displaystyle \lambda y.y}$. Термины, которые отличаются только альфа-преобразованием, называются α-эквивалент.

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

${\displaystyle (y\not \in FV(b)\land a(\lambda x.b)=\lambda y.b[x:=y])\to \operatorname {alpha-con} (a)}$

Обратите внимание, что подстановка не будет повторяться в теле лямбда-выражений с формальным параметром ${\displaystyle x}$ из-за изменения оператора подстановки, описанного выше.

См. Пример;

α-преобразование	λ-выражение	Канонически названный	Комментарий
	${\displaystyle \lambda z.\lambda y.(z\ y)}$	${\displaystyle \lambda \operatorname {P} .\lambda \operatorname {PN} .(\operatorname {P} \operatorname {PN} )}$	Оригинальные выражения.
правильно переименуйте y в k, (потому что k не используется в теле)	${\displaystyle \lambda z.\lambda k.(z\ k)}$	${\displaystyle \lambda \operatorname {P} .\lambda \operatorname {PN} .(\operatorname {P} \operatorname {PN} )}$	Нет изменений в каноническом переименованном выражении.
наивно переименовать y в z (неправильно, потому что z свободен в ${\displaystyle \lambda y.(z\ y)}$)	${\displaystyle \lambda z.\lambda z.(z\ z)}$	${\displaystyle \lambda \operatorname {P} .\lambda \operatorname {PN} .({\color {Red}\operatorname {PN} }\operatorname {PN} )}$	${\displaystyle z}$ захвачен.

β-редукция (предотвращение захвата)

β-редукция отражает идею применения функции (также называемую вызовом функции) и реализует замену фактического выражения параметра на формальную переменную параметра. β-восстановление определяется в терминах замещения.

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

${\displaystyle (\forall z:z\not \in FV(y)\lor z\not \in BV(b))\to \operatorname {beta-redex} [\lambda x.b\ y]=b[x:=y]}$

Альфа-переименование может использоваться на ${\displaystyle b}$ переименовать имена, которые свободны в ${\displaystyle y}$ но связаны ${\displaystyle b}$, чтобы выполнить предварительное условие для этого преобразования.

См. Пример;

β-редукция	λ-выражение	Канонически названный	Комментарий
	${\displaystyle (\lambda x.\lambda y.(\lambda z.(\lambda x.z\ x)(\lambda y.z\ y))(x\ y))}$	${\displaystyle (\lambda \operatorname {P} .\lambda \operatorname {PN} .(\lambda \operatorname {PNF} .(\lambda \operatorname {PNFNF} .\operatorname {PNF} \operatorname {PNFNF} )(\lambda \operatorname {PNFNS} .\operatorname {PNF} \operatorname {PNFNS} ))(\operatorname {P} \operatorname {PN} ))}$	Оригинальные выражения.
Наивная бета 1,	${\displaystyle (\lambda x.\lambda y.((\lambda x.(x\ y)x)(\lambda y.(x\ y)y)))}$	Канонический ${\displaystyle (\lambda \operatorname {P} .\lambda \operatorname {PN} .((\lambda \operatorname {PNF} .({\color {Blue}\operatorname {P} }\operatorname {PN} )\operatorname {PNF} )(\lambda \operatorname {PNS} .(\operatorname {P} {\color {Blue}\operatorname {PN} })\operatorname {PNS} )))}$ Естественный ${\displaystyle (\lambda \operatorname {P} .\lambda \operatorname {PN} .((\lambda \operatorname {PNF} .({\color {Red}\operatorname {PNF} }\operatorname {PN} )\operatorname {PNF} )(\lambda \operatorname {PNS} .(\operatorname {P} {\color {Red}\operatorname {PNS} )}\operatorname {PNS} )))}$	x (P) и y (PN) были захвачены при замене.
Альфа переименовать внутреннее, x → a, y → b	${\displaystyle (\lambda x.\lambda y.(\lambda z.(\lambda x.z\ a)(\lambda b.z\ b))(x\ y))}$	${\displaystyle (\lambda \operatorname {P} .\lambda \operatorname {PN} .(\lambda \operatorname {PNF} .(\lambda \operatorname {PNFNF} .\operatorname {PNF} \operatorname {PNFNF} )(\lambda \operatorname {PNFNS} .\operatorname {PNF} \operatorname {PNFNS} ))(\operatorname {P} \operatorname {PN} ))}$
Бета 2,	${\displaystyle (\lambda x.\lambda y.((\lambda a.(x\ y)a)(\lambda b.(x\ y)b)))}$	Канонический ${\displaystyle (\lambda \operatorname {P} .\lambda \operatorname {PN} .((\lambda \operatorname {PNF} .(\operatorname {P} \operatorname {PN} )\operatorname {PNF} )(\lambda \operatorname {PNS} .(\operatorname {P} \operatorname {PN} )\operatorname {PNS} )))}$ Естественный ${\displaystyle (\lambda \operatorname {P} .\lambda \operatorname {PN} .((\lambda \operatorname {PNF} .(\operatorname {P} \operatorname {PN} )\operatorname {PNF} )(\lambda \operatorname {PNS} .(\operatorname {P} \operatorname {PN} )\operatorname {PNS} )))}$	x и y не зафиксированы.

${\displaystyle {\begin{array}{r}((\lambda x.z\ x)(\lambda y.z\ y))[z:=(x\ y)]\\((\lambda a.z\ a)(\lambda b.z\ b))[z:=(x\ y)]\end{array}}}$

В этом примере

1. В β-редексе
   1. Свободные переменные: ${\displaystyle \operatorname {FV} (x\ y)=\{x,y\}}$
   2. Связанные переменные: ${\displaystyle \operatorname {BV} ((\lambda x.z\ x)(\lambda y.z\ y))=\{x,y\}}$
2. Наивный β-редекс изменил значение выражения, потому что x и y из фактического параметра были захвачены, когда выражения были подставлены во внутренние абстракции.
3. Альфа-переименование устранило проблему, изменив имена x и y во внутренней абстракции, чтобы они отличались от имен x и y в фактическом параметре.
   1. Свободные переменные: ${\displaystyle \operatorname {FV} (x\ y)=\{x,y\}}$
   2. Связанные переменные: ${\displaystyle \operatorname {BV} ((\lambda a.z\ a)(\lambda b.z\ b))=\{a,b\}}$
4. Затем β-редекс продолжился с предполагаемым значением.

η-редукция

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

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

${\displaystyle x\not \in \mathrm {FV} (f)\to {\text{η-redex}}[\lambda x.(fx)]=f}$

Проблема с использованием η-редекса, когда f имеет свободные переменные, показана в этом примере:

Снижение	Лямбда-выражение	β-редукция
	${\displaystyle (\lambda x.(\lambda y.y\,x)\,x)\,a}$	${\displaystyle \lambda a.a\,a}$
Наивное η-сокращение	${\displaystyle (\lambda y.y\,x)\,a}$	${\displaystyle \lambda a.a\,x}$

Это неправильное использование η-редукции меняет смысл, оставляя Икс в ${\displaystyle \lambda y.y\,x}$ незамещенный.

Рекомендации

1. Барендрегт, Хендрик Питер (1984), Лямбда-исчисление: его синтаксис и семантика, Исследования по логике и основам математики, 103 (Пересмотренное издание), Северная Голландия, Амстердам., ISBN  978-0-444-87508-2, заархивировано из оригинал на 2004-08-23— Исправления
2. «Пример правил ассоциативности». Lambda-bound.com. Получено 2012-06-18.
3. Селинджер, Питер (2008), Конспект лекций по лямбда-исчислению (PDF), 0804, Департамент математики и статистики Оттавского университета, стр. 9, arXiv:0804.3434, Bibcode:2008arXiv0804.3434S
4. «Пример правила ассоциативности». Lambda-bound.com. Получено 2012-06-18.
5. Барендрегт, Хенк; Барендсен, Эрик (март 2000 г.), Введение в лямбда-исчисление (PDF)
6. де Кейруш, Руй Ж. "Теоретико-доказательственный подход к программированию и роли правил редукции. " Диалектика 42(4), страницы 265-282, 1988.
7. Турбак, Франклин; Гиффорд, Дэвид (2008), Концепции дизайна на языках программирования, MIT press, стр. 251, ISBN  978-0-262-20175-9