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

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

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

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

Определение

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

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

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

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

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

Обозначения

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

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

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

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

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

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

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

Снижение

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

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

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

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

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

α-конверсия

Альфа-конверсия, иногда известная как альфа-переименование, ^[7] позволяет изменять имена связанных переменных. Например, альфа-конверсия $\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 — выражение

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

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

Семантика

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

α-конверсия - $\operatorname {alpha-conv} (a)\to \operatorname {canonym} [A,P]=\operatorname {canonym} [a[A],P]$
β-восстановление - $\operatorname {beta-redex} [\lambda p.b\ v]=b[p:=v]$
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», + — конкатенация, а «имя» преобразует строку в имя.

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

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

$O[x]=x$
$M[x:=y][x]=y$
$x\neq z\to M[x:=y][z]=M[z]$

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

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

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

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

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

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

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

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

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

Слабая голова, нормальная форма.

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

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

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

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

$(\lambda x.b)[x:=y]=\lambda x.b$
$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)

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

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

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

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

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

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

α-конверсия

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

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$ незамещенный.

Ссылки

^ Барендрегт, Хендрик Питер (1984), Лямбда-исчисление: его синтаксис и семантика , Исследования по логике и основам математики, том. 103 (пересмотренная редакция), Северная Голландия, Амстердам., ISBN. 978-0-444-87508-2 , заархивировано из оригинала 23 августа 2004 г. — Исправления
^ «Пример правил ассоциативности» . Lambda-bound.com . Проверено 18 июня 2012 г.
^ Селинджер, Питер (2008), Конспекты лекций по лямбда-исчислению (PDF) , том. 0804, факультет математики и статистики, Оттавский университет, с. 9, arXiv : 0804.3434 , Bibcode : 2008arXiv0804.3434S
^ «Пример правила ассоциативности» . Lambda-bound.com . Проверено 18 июня 2012 г.
^ Jump up to: ^а ^б Барендрегт, Хенк; Барендсен, Эрик (март 2000 г.), Введение в лямбда-исчисление (PDF)
^ Jump up to: ^а ^б де Кейро, Рюи ЖГБ « Теоретико-доказательное описание программирования и роли правил редукции » . Dialectica 42 (4), страницы 265–282, 1988.
^ Jump up to: ^а ^б Турбак, Франклин; Гиффорд, Дэвид (2008), Концепции дизайна в языках программирования , MIT Press, стр. 251, ISBN 978-0-262-20175-9
^ «Заметки по оценке терминов λ-исчисления и абстрактных машин» . ученый.google.ca . Проверено 14 мая 2024 г.
^ Пейтон Джонс, Саймон Л. (1987). Реализация функциональных языков программирования . Энглвуд Клиффс, Нью-Джерси: Prentice/Hill International. ISBN 978-0-13-453333-9 .

[1] Барендрегт, Хендрик Питер (1984), Лямбда-исчисление: его синтаксис и семантика , Исследования по логике и основам математики, том. 103 (пересмотренная редакция), Северная Голландия, Амстердам., ISBN. 978-0-444-87508-2 , заархивировано из оригинала 23 августа 2004 г. — Исправления

[2] «Пример правил ассоциативности» . Lambda-bound.com . Проверено 18 июня 2012 г.

[Selinger-3] Селинджер, Питер (2008), Конспекты лекций по лямбда-исчислению (PDF) , том. 0804, факультет математики и статистики, Оттавский университет, с. 9, arXiv : 0804.3434 , Bibcode : 2008arXiv0804.3434S

[4] «Пример правила ассоциативности» . Lambda-bound.com . Проверено 18 июня 2012 г.

[BarendregtBarendsen-5] Jump up to: ^а ^б Барендрегт, Хенк; Барендсен, Эрик (март 2000 г.), Введение в лямбда-исчисление (PDF)

[dx.doi.org-6] Jump up to: ^а ^б де Кейро, Рюи ЖГБ « Теоретико-доказательное описание программирования и роли правил редукции » . Dialectica 42 (4), страницы 265–282, 1988.

[MIT_press-7] Jump up to: ^а ^б Турбак, Франклин; Гиффорд, Дэвид (2008), Концепции дизайна в языках программирования , MIT Press, стр. 251, ISBN 978-0-262-20175-9

[8] «Заметки по оценке терминов λ-исчисления и абстрактных машин» . ученый.google.ca . Проверено 14 мая 2024 г.

[9] Пейтон Джонс, Саймон Л. (1987). Реализация функциональных языков программирования . Энглвуд Клиффс, Нью-Джерси: Prentice/Hill International. ISBN 978-0-13-453333-9 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]