Сокращение исчисления лямбда

Question

Я могу сделать простые сокращения лямбда-исчисления, однако я не могу понять, как делать те, которые получают «currying».

Эти два примера, которые я не могу понять:

1. (((lambda x . (lambda y . (j y))) j) m)
2. ((lambda p . (p j)) (lambda x . (q x)))

Answer 1

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

1. (((лямбда х. (Лямбда-у (JY).)) К) м) - заменить x для j
2. ((лямбда-у (JY)) м.) - заменить y для m
3. (JM)
4. здесь , вы застряли ...

Обычно не применяется правило сокращения для применения переменной к переменной. Обычно мы используем систему типов, чтобы гарантировать, что для любой хорошо типизированной программы, когда мы оцениваем, мы никогда не «застреваем», как это было на шаге 3.

Каррирование не должно создавать дополнительной сложности, чем то, что вы, возможно, уже видели. В общем, стратегия образует что-то вроде формы e1 e2 ... en, вы можете думать об этом как (((e1 e2) e3) ... en). Затем вы уменьшите e1 e2, что должно дать лямбду, которую вы, чем оцениваете, применяете к e3 и так далее.

Я позволю вам понять, как это упражнение.

Answer 2

Замечание Ошибка при оценке, она сводится к j m, поэтому часть о самоприложении не имеет отношения к делу.

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

В математических терминах ((lambda x . (lambda y . (j y))) может быть дано имя, а затем записать в виде: f(x,y) = j(y). В вашем примере вы бы оценили f(m,j) = j(j). Итак, что произойдет, если у нас нет обоих аргументов для f? Мы не можем его полностью оценить, но мы можем определить новую функцию g (y) = f (j, y), где мы просто вставляем первый аргумент. Эта пошаговая оценка функции называется частичной оценкой или каррированием.

В исчислении лямбда эти два аспекта выглядят абсолютно одинаково. Если вы хотите применить оба параметра к своему термину, вы начинаете с первого аргумента:

Ваша начальная функция f (m, j): (((lambda x . (lambda y . (j y))) j) m) сводится к g (j): ((lambda y . (j y))) j. Когда мы продолжим нашу оценку (мы все равно можем применить нашу функцию к j), мы достигнем j (j): j j. Теперь мы больше не можем применять какие-либо правила сокращения, поэтому мы можем увидеть j j в результате наших вычислений. То, что наш результат - приложение, прекрасно, но что он применяется к себе, является чем-то особенным.

(остальное не имеет отношения к выделки больше, но само-приложение, которое мосты к тому, что писал)

@ Matt

Возможно, следует объяснить, что это означает: функция J получает в качестве аргумента. С помощью этого вы можете реализовать рекурсию. Знаменитый Y combinator Y: (lambda x . f x x) делает именно это: если вы оцениваете Y Y, то есть (lambda x . f x x) Y, вы вычисляете f (Y Y). Когда вы снова оцените внутренний Y Y, вы вычисляете f f (Y Y) и так далее. Это как раз рекурсивное применение функции f. Побочным эффектом является то, что для некоторого f оценка никогда не прекратится (уже если вы используете функцию идентификации (lambda x.x)).

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

E.g. предположим, что x имеет тип int, то в приложении f x, f должен быть такого типа, который принимает переменную типа int и вычисляет результат, скажем, типа string. Тогда мы можем написать тип f как int -> string. Тип f x - string, так как это мы получаем, когда оцениваем f на x.

Абстракции создают новую функцию. Например, (lambda x . x) нуждается в аргументе типа int и производит термин типа int, то есть он имеет тип int -> int.

Но теперь самоприложение вроде j j больше не работает: скажем, внутренний j имеет тип t. Тогда внешний j должен быть типа t -> t. Единственный способ сделать эту работу состоит в том, что ваш тип - это бесконечное гнездование t, которое обычно запрещено.

Несмотря на то, что этот подход кажется немного ограниченным, вы можете добавить рекурсию поверх типизированного лямбда-исчисления для создания языков программирования, таких как Haskell или OCaml.