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

Общее введение см. в разделе Лямбда-исчисление .

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

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

Это формальное определение было дано Алонсо Чёрчем .

Определение

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

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

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

1. Если $x$ является переменной, то $x\in \Lambda$
2. Если $x$ является переменной и $M\in \Lambda$, затем $(\lambda x.M)\in \Lambda$
3. Если $M,N\in \Lambda$, затем $(M\ N)\in \Lambda$

Экземпляры правила 2 известны как абстракции, а случаи правила 3 ​​— как приложения.

Обозначения

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

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

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

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

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

1. $\operatorname {FV} (x)=\{x\}$, где $x$ это переменная
2. $\operatorname {FV} (\lambda x.M)=\operatorname {FV} (M)\backslash \{x\}$
3. $\operatorname {FV} (M\ N)=\operatorname {FV} (M)\cup \operatorname {FV} (N)$

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

Сокращение

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

Существует три вида сокращения:

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

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

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

α-конверсия

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

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

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

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

Замена

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

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

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

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

β-редукция

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

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

n-редукция

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

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

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

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

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

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

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

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

Имя	БНФ	Описание
Абстракция	<expression> ::= λ <variable-list> . <expression>	Определение анонимной функции.
Срок подачи заявки	<expression> ::= <application-term>
Приложение	<application-term> ::= <application-term> <item>	Вызов функции.
Элемент	<application-term> ::= <item>
Переменная	<item> ::= <variable>	Например, x, y, факт, сумма, ...
Группировка	<item> ::= ( <expression> )	Выражение в квадратных скобках.

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

 <variable-list> ::= <variable> | <variable>, <variable-list>

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

 <variable> ::= <alpha> <extension>
 <extension> ::= 
 <extension> ::= <extension-char> <extension> 
 <extension-char> ::= <alpha> | <digit> | _

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

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

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

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

$x\ y\ z=(x\ y)\ z$

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

$\lambda x.y.z=\lambda x.\lambda y.z$

где,

• х — переменная
• y — список переменных
• z — выражение

как

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

Семантика

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

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

где,

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

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

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

—

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

${\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», + — конкатенация, а «имя» преобразует строку в имя.

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

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

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

Оператор замены

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Слабая голова

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Изменения в операторе замены

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

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

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

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

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

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

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

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

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

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

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

Существует три вида трансформации:

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

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

Термин редекс , сокращение от сокращаемого выражения , относится к подтермам, которые можно сократить с помощью одного из правил сокращения.

α-конверсия

Альфа-конверсия, иногда известная как альфа-переименование, позволяет изменять имена связанных переменных. Например, альфа-конверсия $\lambda x.x$ мог бы дать $\lambda y.y$. Термы, отличающиеся только альфа-конверсией, называются α-эквивалентными .

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

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

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

См. пример;

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

β-редукция (избегание захвата)

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

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

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

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

См. пример;

β-восстановление	λ-выражение	Канонически названный	Комментарий
	$(\lambda x.\lambda y.(\lambda z.(\lambda x.z\ x)(\lambda y.z\ y))(x\ y))$	$(\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,	$(\lambda x.\lambda y.((\lambda x.(x\ y)x)(\lambda y.(x\ y)y)))$	Канонический $(\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} )))$ Естественный $(\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) были уловлены при замене.
Альфа переименовывает внутреннюю, х → а, у → б	$(\lambda x.\lambda y.(\lambda z.(\lambda a.z\ a)(\lambda b.z\ b))(x\ y))$	$(\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,	$(\lambda x.\lambda y.((\lambda a.(x\ y)a)(\lambda b.(x\ y)b)))$	Канонический $(\lambda \operatorname {P} .\lambda \operatorname {PN} .((\lambda \operatorname {PNF} .(\operatorname {P} \operatorname {PN} )\operatorname {PNF} )(\lambda \operatorname {PNS} .(\operatorname {P} \operatorname {PN} )\operatorname {PNS} )))$ Естественный $(\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 не захвачены.

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

n-редукция

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

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

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

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

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

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