Ответ 1

Лямбда-исчисление

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

В лямбда-исчислении в основном два с половиной процесса:

1) Преобразование альфа - если вы применяете два лямбда-выражения с одним и тем же именем переменной внутри, вы меняете одно из них на новое имя переменной. Например (λx.xx) (λx.x) становится чем-то вроде (λx.xx) (λy.y) или (λx.xx) (λx'.x ') после редукции. Результат эквивалентен тому, с чего вы начинаете, только с разными именами переменных.

2) Beta Reduction - в основном просто замена. Это процесс вызова лямбда-выражения с вводом и получения вывода. Лямбда-выражение похоже на функцию, которую вы вызываете, подставляя ввод во всем выражении. Возьмите (λx.xy) z, вторая половина (λx.xy), все после периода, выводится, вы сохраняете выходные данные, но заменяете переменную (названную перед периодом) предоставленным вводом. z - это вход, x - это имя параметра, xy - это выход. Найдите все вхождения параметра в выходных данных и замените их входными данными, и это то, к чему он сводится, поэтому (λx.xy)z => xy с заменой z на x, то есть zy.

2.5) Eta Conversion/Eta Reduction - Это частное сокращение, которое я называю только половиной процесса, потому что это своего рода Beta Reduction, вроде как в техническом смысле это не так. Вы можете видеть это написанным в википедии или в учебнике как "Eta-преобразование конвертирует между λx. (F x) и f всякий раз, когда x не кажется свободным в f", что звучит очень странно. Все, что на самом деле означает, это λx. (F x) = f, если f не использует x. если это действительно имеет смысл, но лучше показать на примере. Рассмотрим (λx. (Λy.yy) x), это эквивалентно через сокращение eta до (λy.yy), потому что f = (λy.yy), в котором нет x, вы можете показать это, уменьшив его, как это было бы решить для (λx.xx), что, очевидно, то же самое. Вы сказали сосредоточиться на сокращении бета-версии, и поэтому я не буду обсуждать eta-преобразование в деталях, которых оно заслуживает, но множество людей посвятили это обмену стеками теории cs

Об обозначении для сокращения бета:

Я собираюсь использовать следующие обозначения для подстановки предоставленного ввода в вывод:

(λ param . output)input => output [param := input] => result

Это означает, что мы заменяем вхождения param в выходных данных, и это сокращает их до

Пример:

(λx.xy)z

= (xy)[x:=z]

= (zy)

= zy

Хватит теории, давай решим это. Лямбда-исчисление это весело.

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

(Λxyz.xyz) (λx.xx) (λx.x) х

= (((λxyz.xyz) (λx.xx)) (λx.x)) x - Позвольте добавить скобку в "Нормальном порядке", левая ассоциативность, abc уменьшается как ((ab) c), где b применяется к а, и с применяется к результату этого

= (((λxyz.xyz) (λx.xx)) (λx.x)) x - выберите самое глубокое вложенное приложение и сначала уменьшите его.

Раздел с полужирным шрифтом уменьшается как:

(Λxyz.xyz) (λx.xx)

= (λx.λyz.xyz) (λx.xx) - означает то же самое, но мы вытаскиваем первый параметр, так как мы собираемся уменьшить его, и поэтому я хочу, чтобы он был понятен

= (λx.λyz.xyz) (λx'.x'x ') - Альфа-преобразование, некоторые люди придерживаются новых букв, но мне нравится добавлять цифры в конце или s, в любом случае это нормально. Поскольку оба выражения используют параметр x, мы должны переименовать их с одной стороны, потому что два X являются локальными переменными, и поэтому не должны представлять одно и то же.

= (λyz.xyz) [x: = λx'.x'x '] - Обозначение для бета-сокращения, мы удаляем первый параметр и заменяем его вхождения в выходных данных тем, что применяется [a: = b] обозначает что а нужно заменить на б.

= (λyz. (λx'.x'x ') yz) - Фактическое сокращение, мы заменяем вхождение x на предоставленное лямбда-выражение.

= (λyz. ((λx'.x'x ') y) z) - снова нормальный порядок для круглых скобок, и посмотрите, еще одно приложение для сокращения, на этот раз y применяется к (λx'.x "х"), так что теперь давайте уменьшим это

= (λyz. ((x'x ') [x': = y]) z). Поместите это в нотацию для уменьшения бета-версии.

= (λyz. (yy) z) - мы поменяем два вхождения x'x 'на Ys, и теперь оно полностью уменьшено.

Добавьте это обратно в исходное выражение:

(((λxyz.xyz) (λx.xx)) (λx.x)) х

= ((λyz. (yy) z) (λx.x)) x - Это не ново, просто возвращаем то, что мы нашли ранее.

= ((λyz. (yy) z) (λx.x)) x - захватить самое глубокое вложенное приложение, оно из (λx.x) применено к (λyz. (yy) z)

Мы снова решим это отдельно:

(Λyz. (Уу) г) (λx.x)

= (λy.λz. (yy) z) (λx.x) - просто снова вывести первый параметр для ясности.

= (λz. (yy) z) [y: = (λx.x)] - Поместите в нотацию бета-редукции, мы выберем первый параметр и отметим, что Ys будет переключен на (λx.x)

= (λz. ((λx.x) (λx.x)) z) - Фактическое сокращение/замена, выделенный жирным шрифтом участок теперь может быть уменьшен

= (λz. ((x) [x: = λx.x]) z) - Надеемся, что вы уже получили картину, мы начинаем бета-уменьшение (λx.x) (λx.x) поместив его в форму (x) [x: = λx.x]

= (λz. ((λx.x)) z) - и есть замена

= (λz.(λx.x) z) - Устранена лишняя скобка, и что мы находим, но другое приложение для решения

= (λz. (x) [x: = z]) - вставьте параметр x в нотацию

= (λz. (z)) - выполнить замену

= (λz.z) - убрать лишние скобки

Поместите его обратно в основное выражение:

((λyz. (Уу) г) (λx.x)) х

= ((λz.z)) x - Заполнение того, что мы доказали выше

= (λz.z) x - удаление лишних скобок, теперь это сокращено до одного конечного применения, x применено к (λz.z)

= (z) [z: = x] - бета-сокращение, введено в запись

= (x) - сделать замену

= x - убрать лишние скобки

Так что да. Ответ - x, он уменьшен до минимума.