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

Эта статья находится в разработке!

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

Лямбда-исчисление — формальная система, придуманная в 1930-х годах Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией. Эта концепция показала себя удобной и сейчас активно используется во многих языках программирования.

Более формально, лямбда-функцию (или, лямбда-терм) можно задать следующей грамматикой:

Определение:

[math] \begin{array}{r c l} \langle Term \rangle & ::= & \langle Variable \rangle \\ & | & \langle Term \rangle \langle Term \rangle \\ & | & \lambda \langle Variable \rangle \to \langle Term \rangle\\ & | & ( \langle Term \rangle )\\ \langle Variable \rangle & ::= & \langle Char \rangle *\\ \end{array} [/math]

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

Рассмотрим, например, функцию [math]id = \lambda x \to x[/math]. Эта функция принимает аргумент и возвращает его неизменённым. Например, [math]id 2 \equiv 2[/math]. Аналогично, [math]id y == y[/math].

Ещё один пример функции: [math]sum = \lambda x \to \lambda y \to x + y|. Эта функция двух аргументов, которая возвращает их сумму. Правда, здесь мы немного вышли за написанную выше грамматику. Ну да ладно. \lt tex\gt sum 2 3 == 5[/math]

Приоритет операций

• Применение левоассоциативно: [math]x y z w == ((x y) z) w[/math]
• Аппликация забирает себе всё, до чего дотянется: [math]\lambda x \to \lambda y \to \lambda z \to z y x \equiv \lambda x \to (\lambda y \to (\lambda z \to ((z y) x)))[/math]
• Скобки играют привычную роль группировки действий

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

Связанными переменными называются все переменные, по которым выше в дереве разбора были абстракции. Все остальные переменные называются свободными.

Например, в [math]\lambda x \to \lambda y \to x[/math], [math]x[/math] связана, а [math]y[/math]— свободна. А в [math]\lambda y \to x (\lambda x \to x)[/math] в своём первом вхождении переменная [math]x[/math] свободна, а во втором — связана.

Рассмотрим функции [math]\lambda y \to y[/math] и [math]\lambda x \to y[/math]. В первой из них при взгляде на [math]y[/math] понятно, что она имеет отношение к переменной, по которой производилась абстракция. Если по одной и той же переменной абстракция производилась более одного раза, то переменная связана с самым поздним (самым нижним в дереве разбора) абстрагированием. Например, в [math]\lambda x \to \lambda x \to \lambda y \to \lambda x \to x[/math], переменная [math]x[/math] связана с самой правой абстракцией по [math]x[/math].

[math]\alpha[/math]-конверсия

Рассмотрим функции [math](\lambda x \to x) z[/math] и [math](\lambda y \to y) z[/math]. Интуитивно понятно, что они являются одинаковыми.

Определение:

[math]\alpha[/math]-конверсия — переименование связанной переменной. Выражение [math]\lambda x \to f[/math] можно заменить на [math]\lambda y \to f[x := y][/math], если [math]y[/math] не входит свободно в [math]f[/math], где [math]f[x:=y][/math] означает замену всех свободных вхождений [math]x[/math] в [math]f[/math] на [math]y[/math].

Функции, получающиеся одна из другой с помощью [math]\alpha[/math]-конверсий, называются [math]\alpha[/math]-эквивалентными и обозначаются [math]f \equiv_\alpha g[/math].

Функции [math]\lambda x \to \lambda y \to x y z[/math] и [math]\lambda a \to \lambda x \to a x z[/math] являются [math]\alpha[/math]-эквивалентными, а [math]\lambda x \to \lambda y \to y z[/math] и [math]\lambda y \to \lambda x \to y z[/math] — нет.

[math]\beta[/math]-редукция

Определение:

[math]\beta[/math]-редукция олицетворяет идею счёта значения функции. Выражение вида [math](\lambda x \to f) y[/math] можно заменить на [math]f[x := y][/math], где [math]f[x:=y][/math], как и ранее, означает замену всех свободных вхождений [math]x[/math] в [math]f[/math] на [math]y[/math].

Определение:

Через [math]f \to_\beta g[/math] обозначают сведение [math]f[/math] к [math]g[/math] с помощью одной [math]\beta[/math]-редукции. А через [math]f \to_\beta^* g[/math] — за ноль или более.

[math]\eta[/math]-редукция

Рассмотрим выражение вида [math]\lambda x \to f x[/math]. Если подставить в эту функцию значение [math]y[/math], то получим: [math](\lambda x \to f x) y \to_\beta f y[/math]. Но если просто подставить [math]y[/math] в [math]f[/math], то получится то же самое.

Определение:

[math]\eta[/math]-редукция — преобразование [math]\lambda x \to f x[/math] в [math]f[/math].

Нотация Де Брюина

Существует также альтернативное эквивалентное определение [math]\lambda[/math]-исчисления. В оригинальном определении для обозначения переменных использовались имена, и была проблема с тем, что не были запрещены одинаковые имена в разных абстракциях.

От этой проблемы можно избавиться следующим образом. Вместо имени переменной будет храниться натуральное число — количество абстракций в дереве разбора, на которое нужно подняться, чтобы найти ту лямбду, с которой данная переменная связана. В данной нотации получаются несколько более простые определения свободных переменных и [math]\beta[/math]-редукции.

Переменная называется свободной, если ей соответствует число, которое больше количества абстракций на пути до неё в дереве разбора.

При [math]\beta[/math]-редукции же нужно будет ко всем свободным переменным заменяющего дерева при каждой замене прибавить число, равное разницы уровней раньше и сейчас. Это будет соответствовать тому, что эта переменная продолжит <<держаться>> за ту же лямбду, что и раньше.

Нумералы Чёрча и программирование на [math]\lambda[/math]-исчислении

Определение

Введём на основе лямбда-исчисления аналог натуральных чисел, основанный на идее, что натуральное число — это или ноль, или увеличенное на единицу натуральное число.

• [math]\bar 0 = \lambda s \to \lambda z \to z[/math]
• [math]\bar 1 = \lambda s \to \lambda z \to s z[/math]
• [math]\bar 2 = \lambda s \to \lambda z \to s (s z)[/math]
• [math]\bar 3 = \lambda s \to \lambda z \to s (s (s z))[/math]

Каждое число будет функцией двух аргументов: какой-то функции и начального значения. Число [math]n[/math] будет [math]n[/math] раз применять функцию к начальному значению и возвращать результат. Если такому <<числу>> дать на вход функцию [math](+1)[/math] и [math]0[/math] в качестве начального значения, то на выходе как раз будет ожидаемое от функции число: [math]\bar 3 (+1) 0 \equiv 3[/math].

+1

Функция, прибавляющая 1 к числу, должна принимать первым аргументом число. Но число — функция двух аргументов. Значит, эта функция должна принимать три аргумента: <<число>> [math]n[/math], которое хочется увеличить, функция, которую надо будет [math]n+1[/math] раз применить, и начальное значение.

[math]\operatorname{succ} = \lambda n \to \lambda s \to \lambda z \to s (n s z)[/math]

Здесь [math]n s z[/math] — [math]n[/math] раз применённая к [math]z[/math] функция [math]s[/math]. Но нужно применить [math]n+1[/math] раз. Отсюда [math]s (n s z)[/math].

Сложение

Сложение двух чисел похоже на прибавление единицы. Но только надо прибавить не единицу, а второе число.

[math]\operatorname{plus} = \lambda n \to \lambda m \to \lambda s \to \lambda z \to n s (m s z)[/math]

[math]n[/math] раз применить [math]s[/math] к применённому [math]m[/math] раз [math]s[/math] к [math]z[/math]

[math](\operatorname{plus} \bar 3 \bar 3) (+1) 0 \equiv 6[/math]

Умножение

Умножение похоже на сложение, но прибавлять надо не единицу, а второе число. Или, в терминах нумералов Чёрча, в качестве применяемой несколько раз функции должна быть не [math]s[/math], а функция, применяющая [math]n[/math] раз [math]s[/math].

[math]\operatorname{mult} = \lambda n \to \lambda m \to \lambda s \to n (m s)[/math]

Здесь [math]m s[/math] — функция, которая [math]m[/math] раз применит [math]s[/math] к тому, что дадут ей на вход. С помощью [math]\eta[/math]-редукции можно немного сократить эту формулу

[math]\operatorname{mult} = \lambda n \to \lambda m \to \lambda s \to n (m s)[/math]

[math](\operatorname{mult} \bar 3 \bar 3) (+1) 0 \equiv 9[/math]

Возведение в степень

It's a kind of magic

[math]\operatorname{power} = \lambda n \to \lambda m \to m n[/math]

[math](\operatorname{power} \bar 3 (\operatorname{succ} \bar 3)) (+1) 0 \equiv 81[/math]

Логические значения

[math]\operatorname{true} = \lambda a \to \lambda b \to a[/math]

[math]\operatorname{false} = \lambda a \to \lambda b \to b[/math]

Функции двух аргументов, возвращающие первый и второй, соответственное, аргументы. Забавный факт: [math]\operatorname{false} \equiv_\alpha \operatorname{zero}[/math]. Эти функции сделаны такими для того, чтобы красиво написать функцию [math]\operatorname{if}[/math]:

[math]\operatorname{if} = \lambda p \to \lambda t \to \lambda e \to p\ t\ e[/math]

Если ей в качестве первого аргумента дадут [math]\operatorname{true}[/math], то вернётся [math]t[/math], иначе — [math]e[/math].

Стандартные функции булевой логики:

[math]\operatorname{and} = \lambda n \to \lambda m \to \operatorname{if} n\ m\ \operatorname{false}[/math]

[math]\operatorname{or} = \lambda n \to \lambda m \to \operatorname{if} n\ \operatorname{true} m[/math]

[math]\operatorname{not} = \lambda b \to \operatorname{if} b\ \operatorname{false} \operatorname{true}[/math]

Ещё одной важной функцией является функция проверки, является ли число нулём:

[math]\operatorname{isZero} = \lambda n \to n\ (\lambda c \to \operatorname{false})\ \operatorname{true}[/math]

Функция выглядит несколько странно. [math]\lambda c -\gt \operatorname{false}[/math] — функция, которая независимо от того, что ей дали на вход, возвращает [math]\operatorname{false}[/math]. Тогда, если в качестве [math]n[/math] будет дан ноль, то функция, по определению нуля, не выполнится ни разу, и будет возвращено значение по умолчанию [math]\operatorname{true}[/math]. Иначе же функция будет запущено, и вернётся [math]\operatorname{false}[/math].

Пара

[math]\operatorname{pair} = \lambda a \to \lambda b \to \lambda t \to t\ a\ b[/math]

[math]\operatorname{fst} = \lambda p \to p\ \operatorname{true}[/math]

[math]\operatorname{snd} = \lambda p \to p\ \operatorname{false}[/math]

Функция [math]\operatorname{pair}[/math] принимает два значения и запаковывает их в пару так, чтобы к ним можно было обращаться по [math]\operatorname{fst}[/math] и [math]\operatorname{snd}[/math]. В [math]\operatorname{fst}[/math] и [math]\operatorname{snd}[/math] вместо [math]t[/math] в [math]\operatorname{pair}[/math] будет подставлено [math]\operatorname{true}[/math] или [math]\operatorname{false}[/math], возвращающие, соответственно, первый и второй аргументы, то есть [math]a[/math] или [math]b[/math], соответственно.

Вычитание

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

[math]\operatorname{minus} = \lambda n \to \lambda m \to m\ \operatorname{pred} n[/math]

Это то же самое, что [math]m[/math] раз вычесть единицу из [math]n[/math].

Осталось, собственно, функция для вычитания единицы. Однако, это не так просто, как может показаться на первый взгляд. Проблема в том, что, имея функцию, которую нужно применить для того, чтобы продвинуться вперёд, продвинуться назад будет проблематично. Если попробовать воспользоваться идеей о том, чтобы, начав от нуля, идти вперёд, и пройти на один шаг меньше, то будет не очень понятно, как же остановиться ровно за один шаг до конца. Для реализации вычитания единицы сделаем следующее. [math]n[/math] раз выполним следующее: имея пару [math]\langle n-1, n-2\rangle[/math] построим пару [math]\langle n, n-1\rangle[/math]. Тогда после [math]n[/math] шагов во втором элементе пары будет записано число [math]n-1[/math], которое и хочется получить.

[math]\operatorname{pred} = \lambda n \to \lambda s \to \lambda z \to\ \operatorname{snd} ( n\ ( \lambda p \to \operatorname{pair}\ (s\ (\operatorname{fst} p))\ (\operatorname{fst} p) )\ (\operatorname{pair}\ z\ z)[/math]

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

Сравнение

Так как вычитание определено таким способом, чтобы для случая, в котором уменьшаемое больше, чем вычитаемое, возвращать ноль, можно определить сравнение на больше-меньше через него. Равными же числа [math]a[/math] и [math]b[/math] считаются, если [math]a - b = 0 \wedge b - a = 0[/math].

[math]\operatorname{le} = \lambda n \to \lambda m \to \operatorname{isZero}\ (\operatorname{minus}\ n\ m)[/math]

[math]\operatorname{less} = \lambda n \to \lambda m \to \operatorname{le}\ n\ (\operatorname{pred} m)[/math]

[math]\operatorname{eq} = \lambda n \to \lambda m \to \operatorname{and}\ (\operatorname{isZero}\ (\operatorname{minus}\ n\ m))\ (\operatorname{isZero}\ (\operatorname{minus}\ m\ n))[/math]

Комбинатор неподвижной точки

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

[math]\operatorname{fact} = \lambda x \to \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))[/math]

Мы столкнулись с проблемой. В определении функции [math]\operatorname{fact}[/math] используется функция [math]\operatorname{fact}[/math]. При формальной замене, получим бесконечную функцию. Можно попытаться решить эту проблему следующим образом

[math]\operatorname{fact} = (\lambda f \to \lambda x \to \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (f\ (\operatorname{pred}\ x)))\ \operatorname{fact}[/math]

Определение:

Неподвижной точкой лямбда-функции [math]f[/math] назовём такую функцию [math]x[/math], что [math]f\ x \to_\beta x[/math].

Лямбда исчисление обладаем замечательным свойством: у каждой функции есть неподвижная точка!

Рассмотрим следующую функцию.

[math]\operatorname{fix} = \lambda f \to (\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x))[/math]

Заметим, что [math]\operatorname{fix} \to_\beta \lambda f \to f\ ((\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)))[/math]. Или, что то же самое, [math]\lambda f \to (\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)) \to_\beta[/math] [math]\lambda f \to f\ ((\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)))[/math]

Рассмотрим функцию

[math]\operatorname{fact'} = \lambda f \to \lambda x \to \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{mult}\ x\ (f\ (\operatorname{pred}\ x)))[/math]

Как было показано выше, [math]\operatorname{fix} f \to_\beta f\ (\operatorname{fix} f)[/math], то есть, [math]\operatorname{fix}\ \operatorname{fact'} \to_\beta \operatorname{fact}[/math], где [math]\operatorname{fact}[/math] — искомая функция, считающая факториал.

[math]\operatorname{fact} = \operatorname{fix}\ \operatorname{fact'}[/math]

Это даст функцию, которая посчитает факториал числа. Но делать она это будет мееедленно-меееедленно. Для того, чтобы посчитать <tex?5!</tex> потребовалось сделать 66066 [math]\beta[/math]-редукций.

Тут правда ничего не понятно? :'(

Деление

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

[math]\operatorname{div'} = \lambda div \to \lambda n \to \lambda m \to \operatorname{if}\ (\operatorname{less}\ n\ m)\ \bar 0\ (\operatorname{succ}\ (div\ (\operatorname{minus}\ n\ m)\ m))[/math]

[math]\operatorname{div} = \operatorname{fix}\ \operatorname{div'}[/math]

И остатка от деления

[math]\operatorname{mod'} = \lambda mod \to \lambda n \to \lambda m \to \operatorname{if}\ (\operatorname{less}\ n\ m)\ n\ (mod\ (\operatorname{minus}\ n\ m)\ m)[/math]

[math]\operatorname{mod} = \operatorname{fix}\ \operatorname{mod'}[/math]

Проверка на простоту

[math]\operatorname{isPrimeHelp}[/math] — принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от 2 до [math]p-1[/math]. Если на что-нибудь разделилось, то число — составное, иначе — простое.

[math]\operatorname{isPrimeHelp'} =[/math][math]\lambda f \to \lambda p \to \lambda i \to \operatorname{if}\ (\operatorname{le}\ p\ i)\ \operatorname{true}\ (\operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ p\ i))\ \operatorname{false}\ (f\ p\ (\operatorname{succ}\ i)))[/math]

[math]\operatorname{isPrimeHelp} = \operatorname{fix}\ \operatorname{isPrimeHelp'}[/math]

[math]\operatorname{isPrime} = \lambda p \to \operatorname{isPrimeHelp}\ p\ \bar 2[/math]

Следующее простое число. [math]\operatorname{nextPrime'}[/math] — следующее, больше либо равное заданного, [math]\operatorname{nextPrime}[/math] — следующее, большее заданного.

[math]\operatorname{nextPrime''} = \lambda f \to \lambda p \to \operatorname{if}\ (\operatorname{isPrime}\ p)\ p\ (f\ (\operatorname{succ}\ p)) [/math]

[math]\operatorname{nextPrime'} = \operatorname{fix}\ \operatorname{nextPrime'}[/math]

[math]\operatorname{nextPrime} = \lambda p \to \operatorname{nextPrime'}\ (\operatorname{succ}\ p)[/math]

[math]\operatorname{ithPrimeStep}[/math] пропрыгает [math]i[/math] простых чисел вперёд. [math]\operatorname{ithPrime}[/math] принимает число [math]i[/math] и пропрыгивает столько простых чисел вперёд, начиная с двойки.

[math]\operatorname{ithPrimeStep'} = \lambda f \to \lambda p \to \lambda i \to \operatorname{if}\ (\operatorname{isZero}\ i)\ p\ (f\ (\operatorname{nextPrime}\ p)\ (\operatorname{pred}\ i))[/math]

[math]\operatorname{ithPrimeStep} = \operatorname{fix}\ \operatorname{ithPrimeStep'}[/math]

[math]\operatorname{ithPrime} = \lambda i \to \operatorname{ithPrimeStep}\ \bar 2\ i[/math]

...и всего через 314007 [math]\beta[/math]-редукций вы узнаете, что третье простое число — семь!

Списки

Для работы со списками чисел нам понадобятся следующие функции:

• [math]\operatorname{empty}[/math] — возвращает пустой список
• [math]\operatorname{cons}[/math] — принимает первый элемент и оставшийся список, склеивает их
• [math]\operatorname{head}[/math] — вернуть голову списка
• [math]\operatorname{tail}[/math] — вернуть хвост списка

Список будем хранить в следующем виде: [math]\langle len, p_1^{a_1}p_2^{a_2}\ldots p_{len}^{a_{len}} \rangle[/math]. При этом, голова списка будет храниться как показатель степени при [math]p_{len}[/math].

[math]\operatorname{empty} = \operatorname{pair}\ \operatorname{zero}\ \bar 1[/math]

[math]\operatorname{cons} = \lambda h \to \lambda t \to \operatorname{pair}\ (\operatorname{succ}\ (\operatorname{fst}\ t))\ (\operatorname{mult}\ (\operatorname{snd}\ t)\ (\operatorname{power}\ (\operatorname{ithPrime}\ (\operatorname{fst}\ t))\ h))[/math]

[math]\operatorname{head} = \lambda list \to \operatorname{getExponent}\ (\operatorname{snd}\ list)\ (\operatorname{ithPrime}\ (\operatorname{pred}\ (\operatorname{fst}\ list)))[/math]

[math]\operatorname{tail} = \lambda list \to \operatorname{pair}\ (\operatorname{pred}\ (\operatorname{fst}\ list)) (\operatorname{eliminateMultiplier}\ (\operatorname{snd}\ list)\ (\operatorname{ithPrime}\ (\operatorname{pred}\ (\operatorname{fst}\ list))))[/math]

[math]\operatorname{eliminateMultiplier'} = \lambda f \to \lambda n \to \lambda m \to \operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ n\ m\))\ (f\ (\operatorname{div}\ n\ m)\ m)\ n[/math]

[math]\operatorname{eliminateMultiplier} = \operatorname{fix}\ \operatorname{eliminateMultiplier'}[/math]

[math]\operatorname{getExponent'} = \lambda f \to \lambda n \to \lambda m \to \operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ n\ m\))\ (\operatorname{succ}\ (f\ (\operatorname{div}\ n\ m)\ m))\ \bar 0[/math]

[math]\operatorname{getExponent} = \operatorname{fix}\ \operatorname{getExponent'}[/math]

Выводы

На основе этого всего уже можно реализовать эмулятор машины тьюринга: с помощью пар, списков чисел можно хранить состояния. С помощью рекурсии можно обрабатывать переходы. Входная строка будет даваться, например, закодированной аналогично списку: пара из длины и числа, характеризующего список степенями простых. Я бы продолжил это писать, но уже на операции [math]\operatorname{head} [1, 2][/math] я не дождался окончания выполнения. Скорость лямбда-исчисления как вычислителя печальна.

[Тут можно это всё потыкать|http://rain.ifmo.ru/~komarov/Turing.lhs]