Лямбда-исчисление(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))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda f.\lambda x.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] (x))[/math][math] (\lambda s.\lambda z.s z)[/math][math] ((\lambda n.\lambda m.\lambda s.n (m s))[/math][math] (x)[/math][math] (f ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math]((\lambda a.\lambda b.\lambda t.t a b)[/math][math](z)[/math][math] z))) (x)))))[/math]
head
[math]\lambda list.(\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda f.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n(\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m)) (n)[/math][math] ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) (m)))[/math][math] (n)[/math][math] m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m) m)) n m)) ((\lambda n.\lambda s.\lambda z.s (n s z))[/math][math] (f ((\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda div.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m)) (n)[/math][math] ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) (m)))[/math][math] (n)[/math][math] m) (\lambda s.\lambda z.z)[/math][math] ((\lambda n.\lambda s.\lambda z.s (n s z))[/math][math] (div ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m) m))) n m) m)) (\lambda s.\lambda z.z))[/math][math] ((\lambda p.p (\lambda a.\lambda b.b))[/math][math] (list))[/math][math] ((\lambda i.(\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] (i))[/math][math] p (f ((\lambda p.(\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda f.\lambda p.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda p.(\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m)) (p)[/math][math] i) (\lambda a.\lambda b.a)[/math][math] ((\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m)) (n)[/math][math] ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) (m)))[/math][math] (n)[/math][math] m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m) m)) p i)) (\lambda a.\lambda b.b)[/math][math] (f p ((\lambda n.\lambda s.\lambda z.s (n s z))[/math][math] (i)))))[/math][math] p (\lambda s.\lambda z.s (s z)))[/math][math] (p))[/math][math] p (f ((\lambda n.\lambda s.\lambda z.s (n s z))[/math][math] (p))))[/math][math] ((\lambda n.\lambda s.\lambda z.s (n s z))[/math][math] (p)))[/math][math] (p))[/math][math] ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) (i))))[/math][math] (\lambda s.\lambda z.s (s z))[/math][math] i) ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (list))))[/math]
tail
[math]\lambda list.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (list)))[/math][math] ((\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda f.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m)) (n)[/math][math] ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) (m)))[/math][math] (n)[/math][math] m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m) m)) n m)) (f ((\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda div.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m)) (n)[/math][math] ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) (m)))[/math][math] (n)[/math][math] m) (\lambda s.\lambda z.z)[/math][math] ((\lambda n.\lambda s.\lambda z.s (n s z))[/math][math] (div ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m) m))) n m) m) n) ((\lambda p.p (\lambda a.\lambda b.b))[/math][math] (list))[/math][math] ((\lambda i.(\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] (i))[/math][math] p (f ((\lambda p.(\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda f.\lambda p.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda p.(\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m)) (p)[/math][math] i) (\lambda a.\lambda b.a)[/math][math] ((\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda f.(\lambda x.f (x x))[/math][math] (\lambda x.f (x x)))[/math][math] (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)[/math][math] ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)[/math][math] (\lambda a.\lambda b.a))[/math][math] ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m)) (n)[/math][math] ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) (m)))[/math][math] (n)[/math][math] m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) n) (n)[/math][math] m) m)) p i)) (\lambda a.\lambda b.b)[/math][math] (f p ((\lambda n.\lambda s.\lambda z.s (n s z))[/math][math] (i)))))[/math][math] p (\lambda s.\lambda z.s (s z)))[/math][math] (p))[/math][math] p (f ((\lambda n.\lambda s.\lambda z.s (n s z))[/math][math] (p))))[/math][math] ((\lambda n.\lambda s.\lambda z.s (n s z))[/math][math] (p)))[/math][math] (p))[/math][math] ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) (i))))[/math][math] (\lambda s.\lambda z.s (s z))[/math][math] i) ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))[/math][math] (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)[/math][math] (s ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (p)))[/math][math] ((\lambda a.\lambda b.\lambda t.t a b)[/math][math] (z)[/math][math] z))) ((\lambda p.p (\lambda a.\lambda b.a))[/math][math] (list)))))[/math]
Источники
См. также
