Викиконспекты - Вклад участника [ru]

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

2014-04-26T09:46:04Z

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

{{В разработке}}

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

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

Более формально, ''лямбда-функцию'' (или, ''лямбда-терм'') можно задать
следующей грамматикой:
{{Определение
|definition=
<tex>
\begin{array}{r c l}
\langle Term \rangle & ::= & \langle Variable \rangle \\
& | & \langle Term \rangle \langle Term \rangle \\
& | & \lambda \langle Variable \rangle\ .\ \langle Term \rangle\\
& | & ( \langle Term \rangle )\\
\langle Variable \rangle & ::= & \langle Char \rangle +\\
\end{array}
</tex>
}}

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

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

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

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

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

Например, в <tex>\lambda x\ .\ \lambda y\ .\ x</tex>, <tex>x</tex> связана, а <tex>y</tex>{{---}} свободна. А в <tex>\lambda y\ .\ x (\lambda x\ .\ x)</tex>
в своём первом вхождении переменная <tex>x</tex> свободна, а во втором {{---}} связана.

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

===α-конверсия===

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

{{Определение
|definition=''<tex>\alpha</tex>-конверсия'' {{---}} переименование связанной переменной. Выражение
<tex>\lambda x\ .\ f</tex> можно заменить на <tex>\lambda y\ .\ f[x := y]</tex>, если <tex>y</tex> не входит свободно в <tex>f</tex>,
где <tex>f[x:=y]</tex> означает замену всех свободных вхождений <tex>x</tex> в <tex>f</tex> на <tex>y</tex>.
}}

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

Функции <tex>\lambda x\ .\ \lambda y\ .\ x\ y\ z</tex> и <tex>\lambda a\ .\ \lambda x\ .\ a\ x\ z</tex> являются <tex>\alpha</tex>-эквивалентными,
а <tex>\lambda x\ .\ \lambda y\ .\ y\ z</tex> и <tex>\lambda y\ .\ \lambda x\ .\ y\ z</tex> {{---}} нет.

===β-редукция===

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

{{Определение
|definition=
Через <tex>f \to_\beta g</tex> обозначают сведение <tex>f</tex> к <tex>g</tex> с помощью одной <tex>\beta</tex>-редукции.
А через <tex>f \to_\beta^* g</tex> {{---}} за ноль или более.
}}

==Нотация Де Брюина==
Существует также альтернативное эквивалентное определение <tex>\lambda</tex>-исчисления.
В оригинальном определении для обозначения переменных использовались имена,
и была проблема с тем, что не были запрещены одинаковые имена в разных
абстракциях.

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

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

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

==Нумералы Чёрча и программирование на <tex>\lambda</tex>-исчислении==

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

* <tex>\bar 0 = \lambda s\ .\ \lambda z\ .\ z</tex>
* <tex>\bar 1 = \lambda s\ .\ \lambda z\ .\ s\ z</tex>
* <tex>\bar 2 = \lambda s\ .\ \lambda z\ .\ s\ (s\ z)</tex>
* <tex>\bar 3 = \lambda s\ .\ \lambda z\ .\ s\ (s\ (s\ z))</tex>

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

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

<tex>\operatorname{succ} = \lambda n\ .\ \lambda s\ .\ \lambda z\ .\ s\ (n\ s\ z)</tex>

Здесь <tex>n\ s\ z</tex> {{---}} <tex>n</tex> раз применённая к <tex>z</tex> функция <tex>s</tex>. Но нужно применить <tex>n+1</tex>
раз. Отсюда <tex>s\ (n\ s\ z)</tex>.

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

<tex>\operatorname{plus} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ n\ s\ (m\ s\ z)</tex>

<tex>n</tex> раз применить <tex>s</tex> к применённому <tex>m</tex> раз <tex>s</tex> к <tex>z</tex>

<tex>(\operatorname{plus}\ \bar 3\ \bar 3)\ (+1)\ 0 \equiv 6</tex>

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

<tex>\operatorname{mult} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ n\ (m\ s)\ z</tex>

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

<tex>\operatorname{mult} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ n\ (m\ s)</tex>

<tex>(\operatorname{mult} \bar 3\ \bar 3)\ (+1)\ 0 \equiv 9</tex>

===Возведение в степень===
It's a kind of magic

<tex>\operatorname{power} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ m\ n\ s\ z</tex>

<tex>(\operatorname{power}\ \bar 3\ (\operatorname{succ}\ \bar 3))\ (+1)\ 0 \equiv 81</tex>

===Логические значения===
<tex>\operatorname{true} = \lambda a\ .\ \lambda b\ .\ a</tex>

<tex>\operatorname{false} = \lambda a\ .\ \lambda b\ .\ b</tex>

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

<tex>\operatorname{if} = \lambda p\ .\ \lambda t\ .\ \lambda e\ .\ p\ t\ e</tex>

Если ей в качестве первого аргумента дадут <tex>\operatorname{true}</tex>, то вернётся <tex>t</tex>, иначе {{---}} <tex>e</tex>.

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

<tex>\operatorname{and} = \lambda n\ .\ \lambda m\ .\ \operatorname{if} n\ m\ \operatorname{false}</tex>

<tex>\operatorname{or} = \lambda n\ .\ \lambda m\ .\ \operatorname{if} n\ \operatorname{true} m</tex>

<tex>\operatorname{not} = \lambda b\ .\ \operatorname{if} b\ \operatorname{false} \operatorname{true}</tex>

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

<tex>\operatorname{isZero} = \lambda n\ .\ n\ (\lambda c\ .\ \operatorname{false})\ \operatorname{true}</tex>

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

===Пара===

<tex>\operatorname{pair} = \lambda a\ .\ \lambda b\ .\ \lambda t\ .\ t\ a\ b</tex>

<tex>\operatorname{fst} = \lambda p\ .\ p\ \operatorname{true}</tex>

<tex>\operatorname{snd} = \lambda p\ .\ p\ \operatorname{false}</tex>

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

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

<tex>\operatorname{minus} = \lambda n\ .\ \lambda m\ .\ m\ \operatorname{pred} n</tex>

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

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

<tex>\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))</tex>

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

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

<tex>\operatorname{le} = \lambda n\ .\ \lambda m\ .\ \operatorname{isZero}\ (\operatorname{minus}\ n\ m)</tex>

<tex>\operatorname{less} = \lambda n\ .\ \lambda m\ .\ \operatorname{le}\ n\ (\operatorname{pred} m)</tex>

<tex>\operatorname{eq} = \lambda n\ .\ \lambda m\ .\ \operatorname{and}\ (\operatorname{isZero}\ (\operatorname{minus}\ n\ m))\
(\operatorname{isZero}\ (\operatorname{minus}\ m\ n))</tex>

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

<tex>\operatorname{fact} = \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))</tex>

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

<tex>\operatorname{fact} = (\lambda f\ .\ \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (f\ (\operatorname{pred}\ x)))\ \operatorname{fact}</tex>

{{Определение
|definition=''Неподвижной точкой'' лямбда-функции <tex>f</tex> назовём такую функцию <tex>x</tex>, что
<tex>f\ x \to_\beta^* x</tex>.
}}

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

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

<tex>\operatorname{fix} = \lambda f\ .\ (\lambda x\ .\ f\ (x\ x))\ (\lambda x\ .\ f\ (x\ x))</tex>

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

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

<tex>\operatorname{fact'} = \lambda f\ .\ \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{mult}\ x\ (f\ (\operatorname{pred}\ x)))</tex>

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

<tex>\operatorname{fact} = \operatorname{fix}\ \operatorname{fact'}</tex>

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

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

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

<tex>\operatorname{div'} = \lambda div\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (\operatorname{less}\ n\ m)\ \bar 0\ (\operatorname{succ}\ (div\ (\operatorname{minus}\ n\ m)\ m))</tex>

<tex>\operatorname{div} = \operatorname{fix}\ \operatorname{div'}</tex>

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

<tex>\operatorname{mod'} = \lambda mod\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (\operatorname{less}\ n\ m)\ n\ (mod\ (\operatorname{minus}\ n\ m)\ m)</tex>

<tex>\operatorname{mod} = \operatorname{fix}\ \operatorname{mod'}</tex>

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

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

<tex>\operatorname{isPrimeHelp'} =</tex><tex>\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)))</tex>

<tex>\operatorname{isPrimeHelp} = \operatorname{fix}\ \operatorname{isPrimeHelp'}</tex>

<tex>\operatorname{isPrime} = \lambda p\ .\ \operatorname{isPrimeHelp}\ p\ \bar 2</tex>

Следующее простое число. <tex>\operatorname{nextPrime'}</tex> {{---}} следующее, больше либо равное заданного, <tex>\operatorname{nextPrime}</tex> {{---}} следующее, большее заданного.

<tex>\operatorname{nextPrime''} = \lambda f\ .\ \lambda p\ .\ \operatorname{if}\ (\operatorname{isPrime}\ p)\ p\ (f\ (\operatorname{succ}\ p)) </tex>

<tex>\operatorname{nextPrime'} = \operatorname{fix}\ \operatorname{nextPrime'}</tex>

<tex>\operatorname{nextPrime} = \lambda p\ .\ \operatorname{nextPrime'}\ (\operatorname{succ}\ p)</tex>

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

<tex>\operatorname{ithPrimeStep'} = \lambda f\ .\ \lambda p\ .\ \lambda i\ .\ \operatorname{if}\ (\operatorname{isZero}\ i)\ p\ (f\ (\operatorname{nextPrime}\ p)\ (\operatorname{pred}\ i))</tex>

<tex>\operatorname{ithPrimeStep} = \operatorname{fix}\ \operatorname{ithPrimeStep'}</tex>

<tex>\operatorname{ithPrime} = \lambda i\ .\ \operatorname{ithPrimeStep}\ \bar 2\ i</tex>

...и всего через 314007 <tex>\beta</tex>-редукций вы узнаете, что третье простое число {{---}} семь!

===Списки===

Для работы со списками чисел нам понадобятся следующие функции:
* <tex>\operatorname{empty}</tex> {{---}} возвращает пустой список
* <tex>\operatorname{cons}</tex> {{---}} принимает первый элемент и оставшийся список, склеивает их
* <tex>\operatorname{head}</tex> {{---}} вернуть голову списка
* <tex>\operatorname{tail}</tex> {{---}} вернуть хвост списка

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

<tex>\operatorname{empty} = \operatorname{pair}\ \operatorname{zero}\ \bar 1</tex>

<tex>\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))</tex>

<tex>\operatorname{head} = \lambda list\ .\ \operatorname{getExponent}\ (\operatorname{snd}\ list)\ (\operatorname{ithPrime}\ (\operatorname{pred}\ (\operatorname{fst}\ list)))</tex>

<tex>\operatorname{tail} = \lambda list\ .\ \operatorname{pair}\ (\operatorname{pred}\ (\operatorname{fst}\ list))
(\operatorname{eliminateMultiplier}\ (\operatorname{snd}\ list)\ (\operatorname{ithPrime}\ (\operatorname{pred}\ (\operatorname{fst}\ list))))</tex>

<tex>\operatorname{eliminateMultiplier'} =</tex><tex> \lambda f\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ n\ m))\ (f\ (\operatorname{div}\ n\ m)\ m)\ n</tex>

<tex>\operatorname{eliminateMultiplier} = \operatorname{fix}\ \operatorname{eliminateMultiplier'}</tex>

<tex>\operatorname{getExponent'} =</tex><tex> \lambda f\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ n\ m))\ (\operatorname{succ}\ (f\ (\operatorname{div}\ n\ m)\ m))\ \bar 0</tex>

<tex>\operatorname{getExponent} = \operatorname{fix}\ \operatorname{getExponent'}</tex>

==Выводы==

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

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

====fact====
(\f.(\x.f (x x)) (\x.f (x x))) (\f.\x.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) (x)) (\s.\z.s z) ((\n.\m.\s.n (m s)) (x) (f ((\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))) (x)))))

====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)))))

==Ссылки==
[http://en.wikipedia.org/wiki/Lambda-calculus Английская Википедия]

[http://ru.wikipedia.org/wiki/%D0%9B%D1%8F%D0%BC%D0%B1%D0%B4%D0%B0-%D0%B8%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5 Русская Википедия]

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

[http://worrydream.com/AlligatorEggs А это игра про крокодильчиков]

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

2014-04-26T09:24:38Z

83.234.102.107: Поправил mult без η-редукции

{{В разработке}}

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

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

Более формально, ''лямбда-функцию'' (или, ''лямбда-терм'') можно задать
следующей грамматикой:
{{Определение
|definition=
<tex>
\begin{array}{r c l}
\langle Term \rangle & ::= & \langle Variable \rangle \\
& | & \langle Term \rangle \langle Term \rangle \\
& | & \lambda \langle Variable \rangle\ .\ \langle Term \rangle\\
& | & ( \langle Term \rangle )\\
\langle Variable \rangle & ::= & \langle Char \rangle +\\
\end{array}
</tex>
}}

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

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

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

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

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

Например, в <tex>\lambda x\ .\ \lambda y\ .\ x</tex>, <tex>x</tex> связана, а <tex>y</tex>{{---}} свободна. А в <tex>\lambda y\ .\ x (\lambda x\ .\ x)</tex>
в своём первом вхождении переменная <tex>x</tex> свободна, а во втором {{---}} связана.

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

===α-конверсия===

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

{{Определение
|definition=''<tex>\alpha</tex>-конверсия'' {{---}} переименование связанной переменной. Выражение
<tex>\lambda x\ .\ f</tex> можно заменить на <tex>\lambda y\ .\ f[x := y]</tex>, если <tex>y</tex> не входит свободно в <tex>f</tex>,
где <tex>f[x:=y]</tex> означает замену всех свободных вхождений <tex>x</tex> в <tex>f</tex> на <tex>y</tex>.
}}

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

Функции <tex>\lambda x\ .\ \lambda y\ .\ x\ y\ z</tex> и <tex>\lambda a\ .\ \lambda x\ .\ a\ x\ z</tex> являются <tex>\alpha</tex>-эквивалентными,
а <tex>\lambda x\ .\ \lambda y\ .\ y\ z</tex> и <tex>\lambda y\ .\ \lambda x\ .\ y\ z</tex> {{---}} нет.

===β-редукция===

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

{{Определение
|definition=
Через <tex>f \to_\beta g</tex> обозначают сведение <tex>f</tex> к <tex>g</tex> с помощью одной <tex>\beta</tex>-редукции.
А через <tex>f \to_\beta^* g</tex> {{---}} за ноль или более.
}}

==Нотация Де Брюина==
Существует также альтернативное эквивалентное определение <tex>\lambda</tex>-исчисления.
В оригинальном определении для обозначения переменных использовались имена,
и была проблема с тем, что не были запрещены одинаковые имена в разных
абстракциях.

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

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

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

==Нумералы Чёрча и программирование на <tex>\lambda</tex>-исчислении==

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

* <tex>\bar 0 = \lambda s\ .\ \lambda z\ .\ z</tex>
* <tex>\bar 1 = \lambda s\ .\ \lambda z\ .\ s\ z</tex>
* <tex>\bar 2 = \lambda s\ .\ \lambda z\ .\ s\ (s\ z)</tex>
* <tex>\bar 3 = \lambda s\ .\ \lambda z\ .\ s\ (s\ (s\ z))</tex>

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

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

<tex>\operatorname{succ} = \lambda n\ .\ \lambda s\ .\ \lambda z\ .\ s\ (n\ s\ z)</tex>

Здесь <tex>n\ s\ z</tex> {{---}} <tex>n</tex> раз применённая к <tex>z</tex> функция <tex>s</tex>. Но нужно применить <tex>n+1</tex>
раз. Отсюда <tex>s\ (n\ s\ z)</tex>.

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

<tex>\operatorname{plus} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ n\ s\ (m\ s\ z)</tex>

<tex>n</tex> раз применить <tex>s</tex> к применённому <tex>m</tex> раз <tex>s</tex> к <tex>z</tex>

<tex>(\operatorname{plus}\ \bar 3\ \bar 3)\ (+1)\ 0 \equiv 6</tex>

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

<tex>\operatorname{mult} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ n\ (m\ s)\ z</tex>

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

<tex>\operatorname{mult} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ n\ (m\ s)</tex>

<tex>(\operatorname{mult} \bar 3\ \bar 3)\ (+1)\ 0 \equiv 9</tex>

===Возведение в степень===
It's a kind of magic

<tex>\operatorname{power} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ m\ n\ s\ z</tex>

<tex>(\operatorname{power}\ \bar 3\ (\operatorname{succ}\ \bar 3))\ (+1)\ 0 \equiv 81</tex>

===Логические значения===
<tex>\operatorname{true} = \lambda a\ .\ \lambda b\ .\ a</tex>

<tex>\operatorname{false} = \lambda a\ .\ \lambda b\ .\ b</tex>

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

<tex>\operatorname{if} = \lambda p\ .\ \lambda t\ .\ \lambda e\ .\ p\ t\ e</tex>

Если ей в качестве первого аргумента дадут <tex>\operatorname{true}</tex>, то вернётся <tex>t</tex>, иначе {{---}} <tex>e</tex>.

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

<tex>\operatorname{and} = \lambda n\ .\ \lambda m\ .\ \operatorname{if} n\ m\ \operatorname{false}</tex>

<tex>\operatorname{or} = \lambda n\ .\ \lambda m\ .\ \operatorname{if} n\ \operatorname{true} m</tex>

<tex>\operatorname{not} = \lambda b\ .\ \operatorname{if} b\ \operatorname{false} \operatorname{true}</tex>

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

<tex>\operatorname{isZero} = \lambda n\ .\ n\ (\lambda c\ .\ \operatorname{false})\ \operatorname{true}</tex>

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

===Пара===

<tex>\operatorname{pair} = \lambda a\ .\ \lambda b\ .\ \lambda t\ .\ t\ a\ b</tex>

<tex>\operatorname{fst} = \lambda p\ .\ p\ \operatorname{true}</tex>

<tex>\operatorname{snd} = \lambda p\ .\ p\ \operatorname{false}</tex>

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

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

<tex>\operatorname{minus} = \lambda n\ .\ \lambda m\ .\ m\ \operatorname{pred} n</tex>

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

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

<tex>\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))</tex>

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

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

<tex>\operatorname{le} = \lambda n\ .\ \lambda m\ .\ \operatorname{isZero}\ (\operatorname{minus}\ n\ m)</tex>

<tex>\operatorname{less} = \lambda n\ .\ \lambda m\ .\ \operatorname{le}\ n\ (\operatorname{pred} m)</tex>

<tex>\operatorname{eq} = \lambda n\ .\ \lambda m\ .\ \operatorname{and}\ (\operatorname{isZero}\ (\operatorname{minus}\ n\ m))\
(\operatorname{isZero}\ (\operatorname{minus}\ m\ n))</tex>

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

<tex>\operatorname{fact} = \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))</tex>

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

<tex>\operatorname{fact} = (\lambda f\ .\ \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (f\ (\operatorname{pred}\ x)))\ \operatorname{fact}</tex>

{{Определение
|definition=''Неподвижной точкой'' лямбда-функции <tex>f</tex> назовём такую функцию <tex>x</tex>, что
<tex>f\ x \to_\beta^* x</tex>.
}}

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

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

<tex>\operatorname{fix} = \lambda f\ .\ (\lambda x\ .\ f\ (x\ x))\ (\lambda x\ .\ f\ (x\ x))</tex>

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

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

<tex>\operatorname{fact'} = \lambda f\ .\ \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{mult}\ x\ (f\ (\operatorname{pred}\ x)))</tex>

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

<tex>\operatorname{fact} = \operatorname{fix}\ \operatorname{fact'}</tex>

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

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

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

<tex>\operatorname{div'} = \lambda div\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (\operatorname{less}\ n\ m)\ \bar 0\ (\operatorname{succ}\ (div\ (\operatorname{minus}\ n\ m)\ m))</tex>

<tex>\operatorname{div} = \operatorname{fix}\ \operatorname{div'}</tex>

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

<tex>\operatorname{mod'} = \lambda mod\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (\operatorname{less}\ n\ m)\ n\ (mod\ (\operatorname{minus}\ n\ m)\ m)</tex>

<tex>\operatorname{mod} = \operatorname{fix}\ \operatorname{mod'}</tex>

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

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

<tex>\operatorname{isPrimeHelp'} =</tex><tex>\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)))</tex>

<tex>\operatorname{isPrimeHelp} = \operatorname{fix}\ \operatorname{isPrimeHelp'}</tex>

<tex>\operatorname{isPrime} = \lambda p\ .\ \operatorname{isPrimeHelp}\ p\ \bar 2</tex>

Следующее простое число. <tex>\operatorname{nextPrime'}</tex> {{---}} следующее, больше либо равное заданного, <tex>\operatorname{nextPrime}</tex> {{---}} следующее, большее заданного.

<tex>\operatorname{nextPrime''} = \lambda f\ .\ \lambda p\ .\ \operatorname{if}\ (\operatorname{isPrime}\ p)\ p\ (f\ (\operatorname{succ}\ p)) </tex>

<tex>\operatorname{nextPrime'} = \operatorname{fix}\ \operatorname{nextPrime'}</tex>

<tex>\operatorname{nextPrime} = \lambda p\ .\ \operatorname{nextPrime'}\ (\operatorname{succ}\ p)</tex>

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

<tex>\operatorname{ithPrimeStep'} = \lambda f\ .\ \lambda p\ .\ \lambda i\ .\ \operatorname{if}\ (\operatorname{isZero}\ i)\ p\ (f\ (\operatorname{nextPrime}\ p)\ (\operatorname{pred}\ i))</tex>

<tex>\operatorname{ithPrimeStep} = \operatorname{fix}\ \operatorname{ithPrimeStep'}</tex>

<tex>\operatorname{ithPrime} = \lambda i\ .\ \operatorname{ithPrimeStep}\ \bar 2\ i</tex>

...и всего через 314007 <tex>\beta</tex>-редукций вы узнаете, что третье простое число {{---}} семь!

===Списки===

Для работы со списками чисел нам понадобятся следующие функции:
* <tex>\operatorname{empty}</tex> {{---}} возвращает пустой список
* <tex>\operatorname{cons}</tex> {{---}} принимает первый элемент и оставшийся список, склеивает их
* <tex>\operatorname{head}</tex> {{---}} вернуть голову списка
* <tex>\operatorname{tail}</tex> {{---}} вернуть хвост списка

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

<tex>\operatorname{empty} = \operatorname{pair}\ \operatorname{zero}\ \bar 1</tex>

<tex>\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))</tex>

<tex>\operatorname{head} = \lambda list\ .\ \operatorname{getExponent}\ (\operatorname{snd}\ list)\ (\operatorname{ithPrime}\ (\operatorname{pred}\ (\operatorname{fst}\ list)))</tex>

<tex>\operatorname{tail} = \lambda list\ .\ \operatorname{pair}\ (\operatorname{pred}\ (\operatorname{fst}\ list))
(\operatorname{eliminateMultiplier}\ (\operatorname{snd}\ list)\ (\operatorname{ithPrime}\ (\operatorname{pred}\ (\operatorname{fst}\ list))))</tex>

<tex>\operatorname{eliminateMultiplier'} =</tex><tex> \lambda f\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ n\ m))\ (f\ (\operatorname{div}\ n\ m)\ m)\ n</tex>

<tex>\operatorname{eliminateMultiplier} = \operatorname{fix}\ \operatorname{eliminateMultiplier'}</tex>

<tex>\operatorname{getExponent'} =</tex><tex> \lambda f\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ n\ m))\ (\operatorname{succ}\ (f\ (\operatorname{div}\ n\ m)\ m))\ \bar 0</tex>

<tex>\operatorname{getExponent} = \operatorname{fix}\ \operatorname{getExponent'}</tex>

==Выводы==

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

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

====fact====
(\f.(\x.f (x x)) (\x.f (x x))) (\f.\x.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) (x)) (\s.\z.s z) ((\n.\m.\s.n (m s)) (x) (f ((\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))) (x)))))

====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)))))

==Ссылки==
[http://en.wikipedia.org/wiki/Lambda-calculus Английская Википедия]

[http://ru.wikipedia.org/wiki/%D0%9B%D1%8F%D0%BC%D0%B1%D0%B4%D0%B0-%D0%B8%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5 Русская Википедия]

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

[http://worrydream.com/AlligatorEggs А это игра про крокодильчиков]