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

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

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

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

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

[math] \begin{array}{r c l} \langle Expression \rangle & ::= & [\langle Application \rangle ]\ \lambda\ \langle Variable \rangle\ .\ \langle Expression \rangle \\ & | & \langle Application \rangle\\ \langle Application \rangle & ::= & \langle Application \rangle \langle Unary \rangle\ |\ \langle Unary \rangle\\ \langle Unary \rangle & ::= & '('\langle Expression \rangle ')'\ |\ \langle Variable \rangle\\ \langle Variable \rangle & ::= & \langle Char \rangle +\\ \end{array} [/math]

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

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

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

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

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

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

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

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

Связанные переменные - это аргументы функции. То есть для функции они являются локальными.

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

α-эквивалетность

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

[math]\alpha[/math]-эквивалетностью — называется наименьшее соотношение эквивалентности на [math]\Lambda[/math] такое что: [math]P=_\alpha P[/math] для любого [math]P[/math] [math]\lambda x.P=_\alpha \lambda y.P[x:=y][/math] если [math]y \not\in FV(P)[/math] и замкнуто относительно следующих правил: [math] P=_\alpha P' \Rightarrow \forall x \in V: \lambda x.P=_\alpha \lambda x.P'\\ P=_\alpha P' \Rightarrow \forall Z \in \Lambda : P Z =_\alpha P'Z\\ P=_\alpha P' \Rightarrow \forall Z \in \Lambda : Z P =_\alpha Z P'\\ P=_\alpha P' \Rightarrow P'=_\alpha P\\ P=_\alpha P' \ \& \ P'=_\alpha P'' \Rightarrow P=_\alpha P''\\[/math]

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

β-редукция

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

[math]\beta[/math]-редукция это наименьшее соотношение на [math]\Lambda[/math] такое что [math](\lambda x.P)Q\to _\beta P[x:=Q][/math] и замкнуто относительно следующих правил [math]P\to _\beta P' \Rightarrow \forall x\in V:\lambda x.P\to _\beta \lambda x.P'\\ P\to _\beta P' \Rightarrow \forall Z\in \Lambda : P\ Z\to _\beta P'\ Z\\ P\to _\beta P' \Rightarrow \forall Z\in \Lambda : Z\ P\to _\beta Z\ P'[/math]

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

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

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

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

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

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

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

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

Определение

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

[math]\bar 0 = \lambda s\ .\ \lambda z\ .\ z[/math]

[math]\bar 1 = \lambda s\ .\ \lambda z\ .\ s\ z[/math]

[math]\bar 2 = \lambda s\ .\ \lambda z\ .\ s\ (s\ z)[/math]

[math]\bar 3 = \lambda s\ .\ \lambda z\ .\ 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\ .\ \lambda s\ .\ \lambda z\ .\ 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\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ 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\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ n\ (m\ s)\ z[/math]

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

[math]\operatorname{mult} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ 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\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ m\ n\ s\ z[/math]

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

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

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

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

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

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

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

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

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

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

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

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

[math]\operatorname{isZero} = \lambda n\ .\ n\ (\lambda c\ .\ \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\ .\ \lambda b\ .\ \lambda t\ .\ t\ a\ b[/math]

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

[math]\operatorname{snd} = \lambda p\ .\ 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\ .\ \lambda m\ .\ 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\ .\ \lambda s\ .\ \lambda z.\ \operatorname{snd}\ ( n\ ( \lambda p\ .\ \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\ .\ \lambda m\ .\ \operatorname{isZero}\ (\operatorname{minus}\ n\ m)[/math]

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

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

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

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

[math]\operatorname{fact} = \lambda x\ .\ \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\ .\ \lambda x\ .\ \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\ .\ (\lambda x\ .\ f\ (x\ x))\ (\lambda x\ .\ f\ (x\ x))[/math]

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

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

[math]\operatorname{fact'} = \lambda f\ .\ \lambda x\ .\ \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]

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

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

Деление

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

[math]\operatorname{div'} = \lambda div\ .\ \lambda n\ .\ \lambda m\ .\ \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\ .\ \lambda n\ .\ \lambda m\ .\ \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\ .\ \lambda p\ .\ \lambda i\ .\ \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\ .\ \operatorname{isPrimeHelp}\ p\ \bar 2[/math]

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

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

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

[math]\operatorname{nextPrime} = \lambda p\ .\ \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\ .\ \lambda p\ .\ \lambda i\ .\ \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\ .\ \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\ .\ \lambda t\ .\ \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\ .\ \operatorname{getExponent}\ (\operatorname{snd}\ list)\ (\operatorname{ithPrime}\ (\operatorname{pred}\ (\operatorname{fst}\ list)))[/math]

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

[math]\operatorname{eliminateMultiplier'} =[/math][math] \lambda f\ .\ \lambda n\ .\ \lambda m\ .\ \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'} =[/math][math] \lambda f\ .\ \lambda n\ .\ \lambda m\ .\ \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] я не дождался окончания выполнения. Скорость лямбда-исчисления как вычислителя печальна.

Примеры (слабонервным не смотреть)

fact

[math](\lambda f.(\lambda x.f (x x)) (\lambda x.f (x x))) (\lambda f.\lambda x.(\lambda p.\lambda t.\lambda e.p t e) ((\lambda n.n (\lambda c.\lambda a.\lambda b.b) (\lambda a.\lambda b.a)) (x)) (\lambda s.\lambda z.s z) ((\lambda n.\lambda m.\lambda s.n (m s)) (x) (f ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b)) (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b) (s ((\lambda p.p (\lambda a.\lambda b.a)) (p))) ((\lambda p.p (\lambda a.\lambda b.a)) (p))) ((\lambda a.\lambda b.\lambda t.t a b) (z) z))) (x))))) [/math]

head

\list.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\n.\m.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) ((\f.(\x.f (x x)) (\x.f (x x))) (\mod.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) n (mod ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m)) n m)) ((\n.\s.\z.s (n s z)) (f ((\f.(\x.f (x x)) (\x.f (x x))) (\div.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) (\s.\z.z) ((\n.\s.\z.s (n s z)) (div ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m))) n m) m)) (\s.\z.z)) ((\p.p (\a.\b.b)) (list)) ((\i.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.\i.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) (i)) p (f ((\p.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.(\p.\t.\e.p t e) ((\p.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.\i.(\p.\t.\e.p t e) ((\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (p) i) (\a.\b.a) ((\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) ((\f.(\x.f (x x)) (\x.f (x x))) (\mod.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) n (mod ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m)) p i)) (\a.\b.b) (f p ((\n.\s.\z.s (n s z)) (i))))) p (\s.\z.s (s z))) (p)) p (f ((\n.\s.\z.s (n s z)) (p)))) ((\n.\s.\z.s (n s z)) (p))) (p)) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (i)))) (\s.\z.s (s z)) i) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) ((\p.p (\a.\b.a)) (list))))

tail

\list.(\a.\b.\t.t a b) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) ((\p.p (\a.\b.a)) (list))) ((\f.(\x.f (x x)) (\x.f (x x))) (\f.\n.\m.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) ((\f.(\x.f (x x)) (\x.f (x x))) (\mod.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) n (mod ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m)) n m)) (f ((\f.(\x.f (x x)) (\x.f (x x))) (\div.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) (\s.\z.z) ((\n.\s.\z.s (n s z)) (div ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m))) n m) m) n) ((\p.p (\a.\b.b)) (list)) ((\i.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.\i.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) (i)) p (f ((\p.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.(\p.\t.\e.p t e) ((\p.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.\i.(\p.\t.\e.p t e) ((\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (p) i) (\a.\b.a) ((\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) ((\f.(\x.f (x x)) (\x.f (x x))) (\mod.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) n (mod ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m)) p i)) (\a.\b.b) (f p ((\n.\s.\z.s (n s z)) (i))))) p (\s.\z.s (s z))) (p)) p (f ((\n.\s.\z.s (n s z)) (p)))) ((\n.\s.\z.s (n s z)) (p))) (p)) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (i)))) (\s.\z.s (s z)) i) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) ((\p.p (\a.\b.a)) (list)))))

Ссылки

Английская Википедия

Русская Википедия

Тут можно это всё потыкать

А это игра про крокодильчиков