Лямбда-исчисление — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Определение)
м (rollbackEdits.php mass rollback)
 
(не показаны 94 промежуточные версии 19 участников)
Строка 1: Строка 1:
{{В разработке}}
+
'''Лямбда-исчисление''' (''англ. lambda calculus'') {{---}} формальная система, придуманная в 1930-х годах  
 
 
== Лямбда-исчисление==
 
 
 
''Лямбда-исчисление'' {{---}} формальная система, придуманная в 1930-х годах  
 
 
Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией.
 
Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией.
 
Эта концепция показала себя удобной и сейчас активно используется во многих
 
Эта концепция показала себя удобной и сейчас активно используется во многих
 
языках программирования.
 
языках программирования.
  
Более формально, ''лямбда-функцию'' (или, ''лямбда-терм'') можно задать
+
== Лямбда-исчисление==
следующей грамматикой:
 
 
{{Определение
 
{{Определение
 
|definition=
 
|definition=
 +
'''Лямбда-выражением''' (англ. <tex>\lambda</tex>''-term'') называется выражение, удовлетворяющее следующей грамматике:<br>
 
<tex>
 
<tex>
\begin{array}{r c l}
+
\Lambda \to V\\
\langle Term \rangle & ::= & \langle Variable \rangle \\
+
\Lambda \to \Lambda \ \Lambda\\
                      & || & \langle Term \rangle \langle Term \rangle \\
+
\Lambda \to \lambda V . \Lambda
                      & || & \lambda \langle Variable \rangle \to \langle Term \rangle\\
 
                      & || & ( \langle Term \rangle )\\
 
\langle Variable \rangle & ::= & \langle Char \rangle *\\
 
\end{array}
 
 
</tex>
 
</tex>
 +
где <tex>V</tex> {{---}} множество всех строк над фиксированным алфавитом <tex> \Sigma \setminus \{ "\lambda", "\ ",\ "."\} </tex>.
 
}}
 
}}
 +
Пробел во втором правиле является терминалом грамматики. Иногда его обозначают как @, чтобы он не сливался с другими символами в выражении.
  
 
В первом случае функция является просто переменной.  
 
В первом случае функция является просто переменной.  
Строка 29: Строка 23:
 
создание функции одного аргумента с заданными именем аргумента и телом функции.
 
создание функции одного аргумента с заданными именем аргумента и телом функции.
  
Рассмотрим, например, функцию <tex>id = \lambda x \to x</tex>. Эта функция принимает аргумент и  
+
Рассмотрим, например, <tex>\lambda</tex>-терм <tex>\operatorname{id} = \lambda x\ .\ x</tex>. Эта функция принимает аргумент и  
 
возвращает его неизменённым. Например,  
 
возвращает его неизменённым. Например,  
<tex>id 2 \equiv 2</tex>. Аналогично, <tex>id y == y</tex>.  
+
<tex>\operatorname{id}\ 2 \equiv 2</tex>. Аналогично, <tex>\operatorname{id}\ y \equiv y</tex>.  
  
Ещё один пример функции: <tex>sum = \lambda x \to \lambda y \to x + y|. Эта функция двух аргументов,
+
Еще примеры:
которая возвращает их сумму. Правда, здесь мы немного вышли за написанную выше грамматику.
+
:<tex>
Ну да ладно. <tex>sum 2 3 == 5</tex>
+
x\\
 +
(x\ z)\\
 +
(\lambda x.(x\ z))\\
 +
(\lambda z.(\lambda w.((\lambda y.((\lambda x.(x\ z))\ y))\ w)))\\
 +
</tex>
 +
 
 +
Иногда <tex>\lambda</tex> -термы пишут по другому. Для краткости подряд идущие лямбды заменяют на одну. Например:
 +
:<tex>\lambda x\ .\ \lambda y\ .P\ \to\ \lambda xy.P</tex>  
  
 
===Приоритет операций===
 
===Приоритет операций===
* Применение левоассоциативно: <tex>x y z w == ((x y) z) w</tex>
+
* Аппликация: <tex>x\ y\ z\ w \equiv ((x\ y)\ z)\ w</tex>
* Аппликация забирает себе всё, до чего дотянется: <tex>\lambda x \to \lambda y \to \lambda z \to z y x \equiv \lambda x \to (\lambda y \to (\lambda z \to ((z y) x)))</tex>
+
* Абстракция забирает себе всё, до чего дотянется: <tex>\lambda x\ .\ \lambda y\ .\ \lambda z\ .\ z\ y\ x \equiv \lambda x\ .\ (\lambda y\ .\ (\lambda z\ .\ ((z\ y)\ x)))</tex>
 
* Скобки играют привычную роль группировки действий
 
* Скобки играют привычную роль группировки действий
  
Строка 46: Строка 47:
 
дереве разбора были абстракции. Все остальные переменные называются свободными.
 
дереве разбора были абстракции. Все остальные переменные называются свободными.
  
Например, в <tex>\lambda x \to \lambda y \to x</tex>, <tex>x</tex> связана, а <tex>y</tex>{{---}} свободна. А в <tex>\lambda y \to x (\lambda x \to x)</tex>
+
Например, в <tex>\lambda x\ .\ y\ x</tex>, <tex>x</tex> и  связана, а <tex>y</tex>{{---}} свободна. А в <tex>\lambda y\ .\ x\ (\lambda x\ .\ x)</tex>
 
в своём первом вхождении переменная <tex>x</tex> свободна, а во втором {{---}} связана.
 
в своём первом вхождении переменная <tex>x</tex> свободна, а во втором {{---}} связана.
  
Рассмотрим функции <tex>\lambda y \to y</tex> и <tex>\lambda x \to y</tex>. В первой из них при взгляде на <tex>y</tex>
+
Связанные переменные {{---}} это аргументы функции. То есть для функции они являются локальными.
 +
 
 +
Рассмотрим функции <tex>\lambda y\ .\ y</tex> и <tex>\lambda x\ .\ y</tex>. В первой из них при взгляде на <tex>y</tex>
 
понятно, что она имеет отношение к переменной, по которой производилась  
 
понятно, что она имеет отношение к переменной, по которой производилась  
 
абстракция. Если по одной и той же
 
абстракция. Если по одной и той же
 
переменной абстракция производилась более одного раза, то переменная связана
 
переменной абстракция производилась более одного раза, то переменная связана
 
с самым поздним (самым нижним в дереве разбора) абстрагированием. Например, в
 
с самым поздним (самым нижним в дереве разбора) абстрагированием. Например, в
<tex>\lambda x \to \lambda x \to \lambda y \to \lambda x \to x</tex>, переменная <tex>x</tex> связана с самой правой абстракцией  
+
<tex>\lambda x\ .\ \lambda x\ .\ \lambda y\ .\ \lambda x\ .\ x</tex>, переменная <tex>x</tex> связана с самой правой абстракцией  
 
по <tex>x</tex>.
 
по <tex>x</tex>.
  
===<tex>\alpha</tex>-конверсия===
+
===α-эквивалентность===
 
 
Рассмотрим функции <tex>(\lambda x \to x) z</tex> и <tex>(\lambda y \to y) z</tex>. Интуитивно понятно, что они
 
являются одинаковыми.
 
  
 
{{Определение
 
{{Определение
|definition=''<tex>\alpha</tex>-конверсия'' {{---}} переименование связанной переменной. Выражение
+
|definition='''<tex>\alpha</tex>-эквивалентностью''' (англ. ''<tex>\alpha</tex> -equivalence'') {{---}} называется наименьшее соотношение эквивалентности на <tex>\Lambda</tex> такое что:
<tex>\lambda x \to f</tex> можно заменить на <tex>\lambda y \to f[x := y]</tex>, если <tex>y</tex> не входит свободно в <tex>f</tex>,
+
:<tex>P=_\alpha P</tex> для любого <tex>P</tex>
где <tex>f[x:=y]</tex> означает замену всех свободных вхождений <tex>x</tex> в <tex>f</tex> на <tex>y</tex>.
+
:<tex>\lambda x.P=_\alpha \lambda y.P[x:=y]</tex> если <tex>y \not\in FV(P)</tex>
 +
и замкнуто относительно следующих правил:
 +
:<tex> 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''\\</tex>
 
}}
 
}}
  
Функции, получающиеся одна из другой с помощью <tex>\alpha</tex>-конверсий, называются
+
Функции <tex>\lambda x\ .\ \lambda y\ .\ x\ y\ z</tex> и <tex>\lambda a\ .\ \lambda x\ .\ a\ x\ z</tex> являются <tex>\alpha</tex>-эквивалентными,
''<tex>\alpha</tex>-эквивалентными'' и обозначаются <tex>f \equiv_\alpha g</tex>.
+
а <tex>\lambda x\ .\ \lambda y\ .\ y\ z</tex> и <tex>\lambda y\ .\ \lambda x\ .\ y\ z</tex> {{---}} нет.
 
 
Функции <tex>\lambda x \to \lambda y \to x y z</tex> и <tex>\lambda a \to \lambda x \to a x z</tex> являются <tex>\alpha</tex>-эквивалентными,
 
а <tex>\lambda x \to \lambda y \to y z</tex> и <tex>\lambda y \to \lambda x \to y z</tex> {{---}} нет.
 
  
===<tex>\beta</tex>-редукция===
+
===β-редукция===
  
 
{{Определение
 
{{Определение
 
|definition=
 
|definition=
<tex>\beta</tex>-редукция олицетворяет идею счёта значения функции. Выражение вида
+
'''<tex>\beta</tex>-редукция''' (англ. ''<tex>\beta</tex> -reduction'') {{---}} это наименьшее соотношение на <tex>\Lambda</tex> такое что
<tex>(\lambda x \to f) y</tex> можно заменить на <tex>f[x := y]</tex>, где <tex>f[x:=y]</tex>, как и ранее, означает
+
:<tex>(\lambda x.P)Q\to _\beta P[x:=Q]</tex>
замену всех свободных вхождений <tex>x</tex> в <tex>f</tex> на <tex>y</tex>.
+
и замкнуто относительно следующих правил
 +
:<tex>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'</tex>  
 
}}
 
}}
  
Строка 89: Строка 95:
 
}}
 
}}
  
===<tex>\eta</tex>-редукция===
+
В <tex>\beta</tex>-редукции вполне возможна функция вида <tex>\lambda x. \lambda x.x</tex>. Во время подстановки вместо <tex>x</tex> внутренняя переменная не заменяется - действует принцип локальной переменной. Но принято считать, что таких ситуаций не возникает и все переменные называются разными именами.
Рассмотрим выражение вида <tex>\lambda x \to f x</tex>. Если подставить в эту функцию значение
+
 
<tex>y</tex>, то получим: <tex>(\lambda x \to f x) y \to_\beta f y</tex>. Но если просто подставить
+
===Каррирование===
<tex>y</tex> в <tex>f</tex>, то получится то же самое.  
 
  
 
{{Определение
 
{{Определение
 
|definition=
 
|definition=
<tex>\eta</tex>-редукция {{---}} преобразование <tex>\lambda x \to f x</tex> в <tex>f</tex>.
+
'''Каррирование''' (англ. ''carrying'') {{---}} преобразование функции от многих переменных в функцию, берущую свои аргументы по одному. Для функции <tex>h</tex> типа <tex>h\ :\ (A\ *\ B)\ \to\ C</tex> оператор каррирования <tex>\Lambda </tex> выполняет преобразование <tex>\Lambda (h)\ :\ A\to (B\to C)</tex>. Таким образом <tex>\Lambda (h)</tex> берет аргумент типа <tex>A</tex> и возвращает функцию типа <tex>B\ \to\ C</tex>. С интуитивной точки зрения, каррирование функции позволяет фиксировать ее некоторый аргумент, возвращая функцию от остальных аргументов. Таким образом, <tex>\Lambda</tex> представляет собой функцию типа <tex>\Lambda :\ (A\ *\ B\to C)\to (A\to (B\to C))</tex>.
 
}}
 
}}
  
==Нотация Де Брюина==
+
==Нотация Де Брауна==
 
Существует также альтернативное эквивалентное определение <tex>\lambda</tex>-исчисления.
 
Существует также альтернативное эквивалентное определение <tex>\lambda</tex>-исчисления.
 
В оригинальном определении для обозначения переменных использовались имена,
 
В оригинальном определении для обозначения переменных использовались имена,
Строка 110: Строка 115:
 
связана. В данной нотации получаются несколько более простые определения  
 
связана. В данной нотации получаются несколько более простые определения  
 
свободных переменных и <tex>\beta</tex>-редукции.  
 
свободных переменных и <tex>\beta</tex>-редукции.  
 +
 +
Грамматику нотации можно задать как:
 +
:<tex>e\ ::= n\ |\ \lambda .e\ |\ e\ e</tex>
 +
 +
Примеры выражений в этой нотации:
 +
 +
{|
 +
! Standart
 +
! de Bruijn
 +
|-
 +
| $\lambda x.x$
 +
| $\lambda .0$
 +
|-
 +
| $\lambda z.z$
 +
| $\lambda .0$
 +
|-
 +
| $\lambda x. \lambda y.x$
 +
| $\lambda . \lambda .1$
 +
|-
 +
| $\lambda x. \lambda y. \lambda s. \lambda z.x\ s\ (y\ s\ z)$
 +
| $\lambda . \lambda . \lambda . \lambda .3\ 1(2\ 1\ 0)$
 +
|-
 +
| $(\lambda x.x\ x)(\lambda x.x\ x)$
 +
| $(\lambda .0\ 0)(\lambda .0\ 0)$
 +
|-
 +
| $(\lambda x. \lambda x.x)(\lambda y.y)$
 +
| $(\lambda .\lambda .0)(\lambda .0)$
 +
|}
  
 
Переменная называется свободной, если ей соответствует число, которое больше
 
Переменная называется свободной, если ей соответствует число, которое больше
Строка 116: Строка 149:
 
При <tex>\beta</tex>-редукции же нужно будет ко всем свободным переменным заменяющего  
 
При <tex>\beta</tex>-редукции же нужно будет ко всем свободным переменным заменяющего  
 
дерева при каждой замене прибавить число, равное разницы уровней раньше и сейчас.
 
дерева при каждой замене прибавить число, равное разницы уровней раньше и сейчас.
Это будет соответствовать тому, что эта переменная продолжит <<держаться>> за
+
Это будет соответствовать тому, что эта переменная продолжит «держаться» за
 
ту же лямбду, что и раньше.
 
ту же лямбду, что и раньше.
  
Строка 126: Строка 159:
 
число.
 
число.
  
<tex>\bar 0 = \lambda s \to \lambda z \to z</tex>
+
:<tex>\bar 0 = \lambda s\ .\ \lambda z\ .\ z</tex>
<tex>\bar 1 = \lambda s \to \lambda z \to s z</tex>
+
:<tex>\bar 1 = \lambda s\ .\ \lambda z\ .\ s\ z</tex>
<tex>\bar 2 = \lambda s \to \lambda z \to s (s z)</tex>
+
:<tex>\bar 2 = \lambda s\ .\ \lambda z\ .\ s\ (s\ z)</tex>
<tex>\bar 3 = \lambda s \to \lambda z \to s (s (s z))</tex>
+
:<tex>\bar 3 = \lambda s\ .\ \lambda z\ .\ s\ (s\ (s\ z))</tex>
  
 
Каждое число будет функцией двух аргументов: какой-то функции и начального значения.
 
Каждое число будет функцией двух аргументов: какой-то функции и начального значения.
 
Число <tex>n</tex> будет <tex>n</tex> раз применять функцию к начальному значению и возвращать  
 
Число <tex>n</tex> будет <tex>n</tex> раз применять функцию к начальному значению и возвращать  
результат. Если такому <<числу>> дать на вход функцию <tex>(+1)</tex> и <tex>0</tex> в качестве  
+
результат. Если такому "числу" дать на вход функцию <tex>(+1)</tex> и <tex>0</tex> в качестве  
 
начального значения, то на выходе как раз будет ожидаемое от функции число:
 
начального значения, то на выходе как раз будет ожидаемое от функции число:
<tex>\bar 3 (+1) 0 \equiv 3</tex>.
+
<tex>\bar 3\ (+1)\ 0 \equiv 3</tex>.
  
 
===+1===
 
===+1===
Функция, прибавляющая 1 к числу, должна принимать первым аргументом число.
+
Функция, прибавляющая <tex>1</tex> к числу, должна принимать первым аргументом число.
 
Но число {{---}} функция двух аргументов. Значит, эта функция должна принимать три
 
Но число {{---}} функция двух аргументов. Значит, эта функция должна принимать три
аргумента: <<число>> <tex>n</tex>, которое хочется увеличить, функция, которую надо будет
+
аргумента: "число" <tex>n</tex>, которое хочется увеличить, функция, которую надо будет
 
<tex>n+1</tex> раз применить, и начальное значение.
 
<tex>n+1</tex> раз применить, и начальное значение.
  
<tex>\operatorname{succ} = \lambda n \to \lambda s \to \lambda z \to s (n s z)</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>n\ s\ z</tex> {{---}} <tex>n</tex> раз применённая к <tex>z</tex> функция <tex>s</tex>. Но нужно применить <tex>n+1</tex>  
раз. Отсюда <tex>s (n s z)</tex>.
+
раз. Отсюда <tex>s\ (n\ s\ z)</tex>.
  
\subsection{Сложение}
+
===Сложение===
Сложение двух чисел похоже на прибавление единицы. Но только надо прибавить не
+
Сложение двух чисел похоже на прибавление единицы. Но только надо прибавить не единицу, а второе число.
единицу, а второе число.
 
  
\begin{code}
+
<tex>\operatorname{plus} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ n\ s\ (m\ s\ z)</tex>
plus' = Lam "n" $ Lam "m" $ Lam "s" $ Lam "z" $ Var "n" `App` Var "s" `App` (Var "m" `App` Var "s" `App` Var "z")
 
\end{code}
 
  
<<$n$ раз применить $s$ к применённому $m$ раз $s$ к $z$>>
+
<tex>n</tex> раз применить <tex>s</tex> к применённому <tex>m</tex> раз <tex>s</tex> к <tex>z</tex>
  
|(plus three three) (+1) 0 == | \eval{(plus three three) (+1) 0}
+
<tex>(\operatorname{plus}\ \bar 3\ \bar 3)\ (+1)\ 0 \equiv 6</tex>
  
\subsection{Умножение}
+
<tex>(\operatorname{plus}\ ((\operatorname{plus}\ 2\ 5)(+1)\ 0)\ 4)(+1)0 \equiv 11</tex>
 +
 
 +
===Умножение===
 
Умножение похоже на сложение, но прибавлять надо не единицу, а второе число.
 
Умножение похоже на сложение, но прибавлять надо не единицу, а второе число.
 
Или, в терминах нумералов Чёрча, в качестве применяемой несколько раз
 
Или, в терминах нумералов Чёрча, в качестве применяемой несколько раз
функции должна быть не $s$, а функция, применяющая $n$ раз $s$.
+
функции должна быть не <tex>s</tex>, а функция, применяющая <tex>n</tex> раз <tex>s</tex>.
  
\begin{code}
+
<tex>\operatorname{mult} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ n\ (m\ s)\ z</tex>
mult' = Lam "n" $ Lam "m" $ Lam "s" $ Var "n" `App` (Var "m" `App` Var "s")
 
\end{code}
 
  
Здесь |m s|~--- функция, которая $m$ раз применит $s$ к тому, что дадут ей на  
+
Здесь <tex>m\ s</tex> {{---}} функция, которая <tex>m</tex> раз применит <tex>s</tex> к тому, что дадут ей на  
вход. С помощью $\eta$-редукции можно немного сократить эту формулу
+
вход. С помощью <tex>\eta</tex>-редукции можно немного сократить эту формулу
  
\begin{spec}
+
<tex>\operatorname{mult} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ n\ (m\ s)</tex>
mult = \n -> \m -> \s -> n (m s)
 
\end{spec}
 
  
|(mult three three) (+1) 0 == | \eval{(mult three three) (+1) 0}
+
<tex>(\operatorname{mult} \bar 3\ \bar 3)\ (+1)\ 0 \equiv 9</tex>
  
\subsection{Возведение в степень}
+
===Возведение в степень===
 
It's a kind of magic
 
It's a kind of magic
  
\begin{code}
+
<tex>\operatorname{power} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ m\ n\ s\ z</tex>
power' = Lam "n" $ Lam "m" $ Var "m" `App` Var "n"
 
\end{code}
 
  
|(power three (succ three)) (+1) 0 == | \eval{(power three (succ three)) (+1) 0}
+
<tex>(\operatorname{power}\ \bar 3\ (\operatorname{succ}\ \bar 3))\ (+1)\ 0 \equiv 81</tex>
  
\subsection{Логические значения}
+
===Логические значения===
\begin{code}
+
<tex>\operatorname{true} = \lambda a\ .\ \lambda b\ .\ a</tex>
true' = Lam "a" $ Lam "b" $ Var "a"
+
 
false' = Lam "a" $ Lam "b" $ Var "b"
+
<tex>\operatorname{false} = \lambda a\ .\ \lambda b\ .\ b</tex>
\end{code}
 
  
 
Функции двух аргументов, возвращающие первый и второй, соответственное, аргументы.
 
Функции двух аргументов, возвращающие первый и второй, соответственное, аргументы.
Забавный факт: $false \equiv_\alpha zero$. Эти функции сделаны такими для того,  
+
Забавный факт: <tex>\operatorname{false} \equiv_\alpha \operatorname{zero}</tex>. Эти функции сделаны такими для того,  
чтобы красиво написать функцию $if$:
+
чтобы красиво написать функцию <tex>\operatorname{if}</tex>:
  
\begin{code}
+
<tex>\operatorname{if} = \lambda p\ .\ \lambda t\ .\ \lambda e\ .\ p\ t\ e</tex>
if'' = Lam "p" $ Lam "t" $ Lam "e" $ Var "p" `App` Var "t" `App` Var "e"
 
\end{code}
 
  
Если ей в качестве первого аргумента дадут $true$, то вернётся $t$, иначе~--- $e$.
+
Если ей в качестве первого аргумента дадут <tex>\operatorname{true}</tex>, то вернётся <tex>t</tex>, иначе {{---}} <tex>e</tex>.
  
 
Стандартные функции булевой логики:
 
Стандартные функции булевой логики:
  
\begin{code}
+
<tex>\operatorname{and} = \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ n\ m\ \operatorname{false}</tex>
and' = Lam "n" $ Lam "m" $ if'' `App` Var "n" `App` Var "m" `App` false'
+
 
or' = Lam "n" $ Lam "m" $ if'' `App` Var "n" `App` true' `App` Var "m"
+
<tex>\operatorname{or} = \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ n\ \operatorname{true} \  m</tex>
not' = Lam "b" $ if'' `App` Var "b" `App` false' `App` true'
+
 
\end{code}
+
<tex>\operatorname{not} = \lambda b\ .\ \operatorname{if}\ b\ \operatorname{false} \ \operatorname{true}</tex>
  
 
Ещё одной важной функцией является функция проверки, является ли число нулём:
 
Ещё одной важной функцией является функция проверки, является ли число нулём:
  
\begin{code}
+
<tex>\operatorname{isZero} = \lambda n\ .\ n\ (\lambda c\ .\ \operatorname{false})\ \operatorname{true}</tex>
isZero' = Lam "n" $ Var "n" `App` (Lam "c" false') `App` true'
 
\end{code}
 
  
Функция выглядит несколько странно. |\c -> false|~--- функция, которая независимо
+
Функция выглядит несколько странно. <tex>\lambda c \to \operatorname{false}</tex> - функция, которая независимо
от того, что ей дали на вход, возвращает $false$. Тогда, если в качестве $n$
+
от того, что ей дали на вход, возвращает <tex>\operatorname{false}</tex>. Тогда, если в качестве <tex>n</tex>
 
будет дан ноль, то функция, по определению нуля, не выполнится ни разу, и будет
 
будет дан ноль, то функция, по определению нуля, не выполнится ни разу, и будет
возвращено значение по умолчанию $true$. Иначе же функция будет запущено, и  
+
возвращено значение по умолчанию <tex>\operatorname{true}</tex>. Иначе же функция будет запущено, и  
вернётся $false$.
+
вернётся <tex>\operatorname{false}</tex>.
 +
 
 +
===Пара===
 +
 
 +
<tex>\operatorname{pair} = \lambda a\ .\ \lambda b\ .\ \lambda t\ .\ t\ a\ b</tex>
  
\subsection{Пара}
+
<tex>\operatorname{fst} = \lambda p\ .\ p\ \operatorname{true}</tex>
  
\begin{code}
+
<tex>\operatorname{snd} = \lambda p\ .\ p\ \operatorname{false}</tex>
pair' = Lam "a" $ Lam "b" $ Lam "t" $ Var "t" `App` Var "a" `App` Var "b"
 
fst'' = Lam "p" $ Var "p" `App` true'
 
snd'' = Lam "p" $ Var "p" `App` false'
 
\end{code}
 
  
Функция $pair$ принимает два значения и запаковывает их в пару так, чтобы к
+
Функция <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>, соответственно.
ним можно было обращаться по $fst$ и $snd$. В $fst$ и $snd$ вместо $t$ в $pair$
 
будет подставлено $true$ или $false$, возвращающие, соответственно, первый и
 
второй аргументы, то есть $a$ или $b$, соответственно.
 
  
\subsection{Вычитание}
+
===Вычитание===
В отличие от всех предыдущих функций, вычитание для натуральных чисел определено
+
В отличие от всех предыдущих функций, вычитание для натуральных чисел определено только в случае, если уменьшаемое больше вычитаемого. Положим в противном случае результат равным нулю. Пусть уже есть функция, которая вычитает из числа единицу. Тогда на её основе легко сделать, собственно, вычитание.
только в случае, если уменьшаемое больше вычитаемого. Положим в противном случае
 
результат равным нулю. Пусть уже есть функция, которая вычитает из числа единицу.
 
Тогда на её основе легко сделать, собственно, вычитание.
 
  
\begin{code}
+
<tex>\operatorname{minus} = \lambda n\ .\ \lambda m\ .\ m\ \operatorname{pred} n</tex>
minus' = Lam "n" $ Lam "m" $ Var "m" `App` pred' `App` Var "n"
 
\end{code}
 
  
<<$m$ раз вычесть единицу из $n$>>.
+
Это то же самое, что <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>, которое и хочется получить.  
как может показаться на первый взгляд. Проблема в том, что, имея функцию, которую
 
нужно применить для того, чтобы продвинуться вперёд, продвинуться назад будет
 
проблематично. Если попробовать воспользоваться идеей о том, чтобы, начав от  
 
нуля, идти вперёд, и пройти на один шаг меньше, то будет не очень понятно, как
 
же остановиться ровно за один шаг до конца. Для реализации вычитания единицы  
 
сделаем следующее. $n$ раз выполним следующее: имея пару $(n-1, n-2)$ построим пару
 
$(n, n-1)$. Тогда после $n$ шагов во втором элементе пары будет записано число
 
$n-1$, которое и хочется получить.
 
% --pred = \n -> \s -> \z -> n (\g -> \h -> h (g s)) (\u -> z) (\u->u)
 
% --pred = \n -> \s -> \z -> snd (n (\p -> (pair (s (fst p)) (fst p))) (pair z z))
 
% --pred = \n -> \s -> \z -> fst' (n (\p -> pair (s (fst p))(fst p)) (pair z z))
 
  
\begin{code}
+
<tex>\operatorname{pred} = \lambda n\ .\ \lambda s\ .\ \lambda z.\ \operatorname{snd}\ (
pred' = Lam "n" $
+
  n\ (
        Lam "s" $
+
          \lambda p\ .\ \operatorname{pair}\ (s\ (\operatorname{fst} p))\ (\operatorname{fst} p)
        Lam "z" $
+
    )\ (\operatorname{pair}\ z\ z))</tex>
            snd'' `App` (Var "n"
 
                            `App` (  
 
                                    Lam "p" $ pair'
 
                                        `App` (Var "s" `App` (fst'' `App` Var "p"))
 
                                        `App` (fst'' `App` Var "p")
 
                                  )
 
                            `App` ( pair' `App` Var "z" `App` Var "z" )
 
                        )
 
\end{code}
 
  
Если вы ничего не поняли, не огорчайтесь. Вычитание придумал Клини, когда  
+
Если вы ничего не поняли, не огорчайтесь. Вычитание придумал Клини, когда ему вырывали зуб мудрости. А сейчас наркоз уже не тот.
ему вырывали зуб мудрости. А сейчас наркоз уже не тот!
 
  
\subsection{Сравнение}
+
===Сравнение===
Так как вычитание определено таким способом, чтобы для случая, в котором
+
Так как вычитание определено таким способом, чтобы для случая, в котором уменьшаемое больше, чем вычитаемое, возвращать ноль, можно определить сравнение на больше-меньше через него. Равными же числа <tex>a</tex> и <tex>b</tex> считаются, если <tex>a - b = 0 \wedge b - a = 0</tex>.
уменьшаемое больше, чем вычитаемое, возвращать ноль, можно определить
 
сравнение на больше-меньше через него. Равными же числа $a$ и $b$ считаются,  
 
если $a - b = 0 \wedge b - a = 0$.
 
  
\begin{code}
+
<tex>\operatorname{le} = \lambda n\ .\ \lambda m\ .\ \operatorname{isZero}\ (\operatorname{minus}\ n\ m)</tex>
le' = Lam "n" $ Lam "m" $ isZero' `App` (minus' `App` Var "n" `App` Var "m")
 
less' = Lam "n" $ Lam "m" $ le' `App` Var "n" `App` (pred' `App` Var "m")
 
eq' = Lam "n" $ Lam "m" $ and'
 
            `App` (isZero' `App` (minus' `App` Var "n" `App` Var "m"))
 
            `App` (isZero' `App` (minus' `App` Var "m" `App` Var "n"))
 
\end{code}
 
  
\subsection{Комбинатор неподвижной точки}
+
<tex>\operatorname{less} = \lambda n\ .\ \lambda m\ .\ \operatorname{le}\ n\ (\operatorname{pred} m)</tex>
Попробуем выразить в лямбда-исчислении какую-нибудь рекурсивную функцию.
 
Напрмер, факториал.
 
  
\begin{spec}
+
<tex>\operatorname{eq} = \lambda n\ .\ \lambda m\ .\ \operatorname{and}\ (\operatorname{isZero}\ (\operatorname{minus}\ n\ m))\
fact = \x -> if (isZero x) one (fact (pred x))
+
(\operatorname{isZero}\ (\operatorname{minus}\ m\ n))</tex>
\end{spec}
 
  
Мы столкнулись с проблемой. В определении функции $fact$ используется функция
+
===Комбинатор неподвижной точки===
$fact$. При формальной замене, получим бесконечную функцию. Можно попытаться решить
+
Попробуем выразить в лямбда-исчислении какую-нибудь функцию, использующую рекурсию. Например, факториал.
эту проблему следующим образом
 
  
\begin{spec}
+
<tex>\operatorname{fact} = \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))</tex>
fact = (\f -> \x -> if (isZero x) one (f (pred x))) fact
 
\end{spec}
 
  
\emph{Неподвижной точкой} лямбда-функции $f$ назовём такую функцию $x$, что
+
Мы столкнулись с проблемой. В определении функции <tex>\operatorname{fact}</tex> используется функция <tex>\operatorname{fact}</tex>. При формальной замене, получим бесконечную функцию. Можно попытаться решить эту проблему следующим образом
$f x \to_\beta x$. Лямбда исчисление обладаем замечательным свойством: у каждой
 
функции есть неподвижная точка!
 
  
Рассмотрим такую функцию.  
+
<tex>\operatorname{fact} = (\lambda f\ .\ \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (f\ (\operatorname{pred}\ x)))\ \operatorname{fact}</tex>
  
\begin{code}
+
{{Определение
fix' = Lam "f" $  (Lam "x" $ Var "f" `App` (Var "x" `App` Var "x"))
+
|definition=''Неподвижной точкой'' лямбда-функции <tex>f</tex> назовём такую функцию <tex>x</tex>, что
            `App`  (Lam "x" $ Var "f" `App` (Var "x" `App` Var "x"))
+
<tex>f\ x \to_\beta^* x</tex>.
\end{code}
+
}}
  
Заметим, что $fix' \to_\beta \lambda f \to f ((\lambda x \to f (x x)) (\lambda x \to f (x x)))$.
+
Лямбда исчисление обладаем замечательным свойством: у каждой функции есть неподвижная точка!
 +
 
 +
Рассмотрим следующую функцию.
 +
 
 +
<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>.
 
Или, что то же самое,  
 
Или, что то же самое,  
$\lambda f \to (\lambda x \to f (x x)) (\lambda x \to f (x x)) \to_\beta
+
<tex>\lambda f\ .\ (\lambda x\ .\ f\ (x\ x))\ (\lambda x\ .\ f\ (x\ x)) \to_\beta^*</tex>
\lambda f \to f ((\lambda x \to f (x x)) (\lambda x \to f (x x)))$
+
<tex>\lambda f\ .\ f\ ((\lambda x\ .\ f\ (x\ x))\ (\lambda x\ .\ f\ (x\ x)))</tex>
  
 
Рассмотрим функцию
 
Рассмотрим функцию
  
\begin{code}
+
<tex>\operatorname{fact'} = \lambda f\ .\ \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{mult}\ x\ (f\ (\operatorname{pred}\ x)))</tex>
fact'' = Lam "f" $ Lam "x" $ if'' `App` (isZero' `App` Var "x")  
 
                                  `App` one'
 
                                  `App` (mult' `App` Var "x" `App` (Var "f" `App`
 
                                            (pred' `App` Var "x")))
 
\end{code}
 
  
Как было показано выше, $fix f \to_\beta f (fix f)$, то есть,  
+
Как было показано выше, <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> {{---}} искомая функция, считающая факториал.
$fix fact'' \to_\beta fact'$, где $fact'$~--- искомая функция, считающая факториал.
 
  
\begin{code}
+
<tex>\operatorname{fact} = \operatorname{fix}\ \operatorname{fact'}</tex>
fact' = fix' `App` fact''
 
\end{code}
 
  
Это даст функцию, которая посчитает факториал числа. Но делать она это будет  
+
Это даст функцию, которая посчитает факториал числа. Но делать она это будет мееедленно-меееедленно. Для того, чтобы посчитать <tex>5!</tex> потребовалось сделать 66066 <tex>\beta</tex>-редукций.
мееедленно-меееедленно. Для того, чтобы посчитать $5!$ потребовалось сделать
 
66066 $\beta$-редукций.
 
  
Тут правда ничего не понятно? :'(
+
Наиболее известным комбинатором неподвижной точки является <tex>Y</tex>-комбинатор, введенный известным американским ученым Хаскеллом Карри как
 +
:<tex>Y\ = \ \lambda f.(\lambda x.f(x\ x))\ (\lambda x.f(x\ x))</tex>
  
\subsection{Деление}
+
===Деление===
Воспользовавшись идеей о том, что можно делать рекурсивные функции, сделаем  
+
Воспользовавшись идеей о том, что можно делать рекурсивные функции, сделаем функцию, которая будет искать частное двух чисел.
функцию, которая будет искать частное двух чисел.
 
  
\begin{code}
+
<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>
div'' = Lam "div" $ Lam "n" $ Lam "m" $ if'' `App` (less' `App` Var "n" `App` Var "m")
+
 
        `App` zero'
+
<tex>\operatorname{div} = \operatorname{fix}\ \operatorname{div'}</tex>
        `App` (succ' `App` (Var "div" `App` (minus' `App` Var "n" `App` Var "m") `App` Var "m"))
 
div' = fix' `App` div''
 
\end{code}
 
  
 
И остатка от деления
 
И остатка от деления
  
\begin{code}
+
<tex>\operatorname{mod'} = \lambda mod\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (\operatorname{less}\ n\ m)\ n\ (mod\ (\operatorname{minus}\ n\ m)\ m)</tex>
mod'' = Lam "mod" $ Lam "n" $ Lam "m" $ if'' `App` (less' `App` Var "n" `App` Var "m")
+
 
        `App` Var "n"
+
<tex>\operatorname{mod} = \operatorname{fix}\ \operatorname{mod'}</tex>
        `App` (Var "mod" `App` (minus' `App` Var "n" `App` Var "m") `App` Var "m")
+
 
mod' = fix' `App` mod'';
+
===Проверка на простоту===
\end{code}
+
 
 +
<tex>\operatorname{isPrimeHelp}</tex> {{---}} принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от <tex>2</tex> до <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>
  
\subsection{Проверка на простоту}
+
<tex>\operatorname{isPrimeHelp} = \operatorname{fix}\ \operatorname{isPrimeHelp'}</tex>
  
$isPrimeHelp$~--- принимает число, которое требуется проверить на простоту и
+
<tex>\operatorname{isPrime} = \lambda p\ .\ \operatorname{isPrimeHelp}\ p\ \bar 2</tex>
то, на что его надо попытаться поделить, перебирая это от 2 до $p-1$. Если на
 
что-нибудь разделилось, то число~--- составное, иначе~--- простое.
 
  
\begin{code}
+
Следующее простое число. <tex>\operatorname{nextPrime'}</tex> {{---}} следующее, больше либо равное заданного, <tex>\operatorname{nextPrime}</tex> {{---}} следующее, большее заданного.
isPrimeHelp' = Lam "f" $ Lam "p" $ Lam "i" $ if'' `App` (le' `App` Var "p" `App` Var "i")
 
                `App` true'
 
                `App` ( if'' `App` (isZero' `App` (mod' `App` Var "p" `App` Var "i"))
 
                        `App` false'
 
                        `App` (Var "f" `App` Var "p" `App` (succ' `App` Var "i"))
 
                )
 
isPrimeHelp = fix' `App` isPrimeHelp'
 
isPrime = Lam "p" $ isPrimeHelp `App` Var "p" `App` two'
 
\end{code}
 
  
Следующее простое число. $nextPrime'$~--- следующее, больше либо равное заданного,
+
<tex>\operatorname{nextPrime''} = \lambda f\ .\ \lambda p\ .\ \operatorname{if}\ (\operatorname{isPrime}\ p)\ p\ (f\ (\operatorname{succ}\ p)) </tex>
$nextPrime$~--- следующее, большее заданного.
 
  
\begin{code}
+
<tex>\operatorname{nextPrime'} = \operatorname{fix}\ \operatorname{nextPrime'}</tex>
nextPrime'' = Lam "f" $ Lam "p" $ if'' `App` (isPrime `App` Var "p")
 
                                  `App` Var "p"
 
                                  `App` (Var "f" `App` (succ' `App` Var "p"))
 
nextPrime' = fix' `App` nextPrime''
 
nextPrime = Lam "p" $ nextPrime' `App` (succ' `App` Var "p")
 
\end{code}
 
  
$ithPrimeStep$ пропрыгает $i$ простых чисел вперёд. $ithPrime$ принимает число
+
<tex>\operatorname{nextPrime} = \lambda p\ .\ \operatorname{nextPrime'}\ (\operatorname{succ}\ p)</tex>
$i$ и пропрыгивает столько простых чисел вперёд, начиная с двойки.
 
  
\begin{code}
+
<tex>\operatorname{ithPrimeStep}</tex> пропрыгает <tex>i</tex> простых чисел вперёд. <tex>\operatorname{ithPrime}</tex> принимает число <tex>i</tex> и пропрыгивает столько простых чисел вперёд, начиная с двойки.
ithPrimeStep' = Lam "f" $ Lam "p" $ Lam "i" $ if'' `App` (isZero' `App` Var "i")
 
                `App` Var "p"
 
                `App` (Var "f" `App` (nextPrime `App` Var "p") `App` (pred' `App` Var "i"))
 
ithPrimeStep = fix' `App` ithPrimeStep'
 
ithPrime = Lam "i" $ ithPrimeStep `App` two' `App` Var "i"
 
\end{code}
 
  
...и всего через 314007 $\beta$-редукций вы узнаете, что третье простое число~---
+
<tex>\operatorname{ithPrimeStep'} = \lambda f\ .\ \lambda p\ .\ \lambda i\ .\ \operatorname{if}\ (\operatorname{isZero}\ i)\ p\ (f\  (\operatorname{nextPrime}\ p)\ (\operatorname{pred}\ i))</tex>
семь!
 
  
\subsection{Списки}
+
<tex>\operatorname{ithPrimeStep} = \operatorname{fix}\ \operatorname{ithPrimeStep'}</tex>
 +
 
 +
<tex>\operatorname{ithPrime} = \lambda i\ .\ \operatorname{ithPrimeStep}\ \bar 2\ i</tex>
 +
 
 +
...и всего через 314007 <tex>\beta</tex>-редукций вы узнаете, что третье простое число {{---}} семь!
 +
 
 +
===Списки===
  
 
Для работы со списками чисел нам понадобятся следующие функции:
 
Для работы со списками чисел нам понадобятся следующие функции:
\begin{itemize}
+
* <tex>\operatorname{empty}</tex> {{---}} возвращает пустой список
    \item $empty$~--- возвращает пустой список
+
* <tex>\operatorname{cons}</tex> {{---}} принимает первый элемент и оставшийся список, склеивает их
    \item $cons$~--- принимает первый элемент и оставшийся список, склеивает их
+
* <tex>\operatorname{head}</tex> {{---}} вернуть голову списка
    \item $head$~--- вернуть голову списка
+
* <tex>\operatorname{tail}</tex> {{---}} вернуть хвост списка
    \item $tail$~--- вернуть хвост списка
+
 
\end{itemize}
+
Список будем хранить в следующем виде: <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>
  
Список будем хранить в следующем виде: $\langle len, p_1^{a_1}p_2^{a_2}\ldots p_{len}^{a_{len}} \rangle$. При этом, голова списка будет храниться как показатель степени при $p_{len}$.
+
<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>
  
\begin{code}
+
<tex>\operatorname{eliminateMultiplier} = \operatorname{fix}\ \operatorname{eliminateMultiplier'}</tex>
empty = pair' `App` zero' `App` one'
 
cons = Lam "h" $ Lam "t" $ pair' `App` (succ' `App` (fst'' `App` Var "t"))
 
        `App` (mult' `App` (snd'' `App` Var "t") `App` (power'
 
                `App` (ithPrime `App` (fst'' `App` Var "t"))
 
                `App` Var "h"
 
        ))
 
head = Lam "list" $ getExponent `App` (snd'' `App` Var "list")
 
                                `App` (ithPrime `App` (pred' `App` (fst'' `App` Var "list")))
 
  
tail = Lam "list" $ pair' `App` (pred' `App` (fst'' `App` Var "list"))
+
<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>
                          `App` (eliminateMultiplier `App` (snd'' `App` Var "list")
 
                                  `App` (ithPrime `App` (pred' `App` (fst'' `App` Var "list" )))
 
                                )
 
  
eliminateMultiplier' = Lam "f" $ Lam "n" $ Lam "m" $ if'' `App` (isZero' `App` (mod' `App` Var "n" `App` Var "m"))
+
<tex>\operatorname{getExponent} = \operatorname{fix}\ \operatorname{getExponent'}</tex>
                        `App` (Var "f" `App` (div' `App` Var "n" `App` Var "m") `App` Var "m")
 
                        `App` Var "n"
 
eliminateMultiplier = fix' `App` eliminateMultiplier'
 
  
getExponent' = Lam "f" $ Lam "n" $ Lam "m" $ if'' `App` (isZero' `App` (mod' `App` Var "n" `App` Var "m"))
+
==Выводы==
                `App` (succ' `App`(Var "f" `App` (div' `App` Var "n" `App` Var "m") `App` Var "m"))
 
                `App` zero'
 
getExponent = fix' `App` getExponent'
 
\end{code}
 
  
На основе этого всего уже можно реализовать эмулятор машины тьюринга:
+
На основе этого всего уже можно реализовать эмулятор машины тьюринга: с помощью пар, списков чисел можно хранить состояния. С помощью рекурсии можно обрабатывать переходы. Входная строка будет даваться, например, закодированной аналогично списку: пара из длины и числа, характеризующего список степенями простых. Я бы продолжил это писать, но уже на операции <tex>\operatorname{head} [1, 2]</tex> я не дождался окончания выполнения. Скорость лямбда-исчисления как вычислителя печальна.
с помощью пар, списков чисел можно хранить состояния. С помощью рекурсии можно
 
обрабатывать переходы. Входная строка будет даваться, например, закодированной
 
аналогично списку: пара из длины и числа, характеризующего список степенями  
 
простых. Я бы продолжил это писать, но уже на операции $head [1, 2]$ я не  
 
дождался окончания выполнения. Скорость лямбда-исчисления как вычислителя
 
печальна.
 
  
\ignore{
+
==Примеры (слабонервным не смотреть)==
\begin{code}
 
  
four' = norm $ succ' `App` three'
+
====fact====
five' = norm $ succ' `App` four'
+
<tex>(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda x.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> (x))</tex><tex> (\lambda s.\lambda z.s z)</tex><tex> ((\lambda n.\lambda m.\lambda s.n (m s))</tex><tex> (x)</tex><tex> (f ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex>((\lambda a.\lambda b.\lambda t.t a b)</tex><tex>(z)</tex><tex> z))) (x)))))</tex>
 +
====head====
 +
<tex>\lambda list.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n(\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m)) n m)) ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (f ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda div.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) (\lambda s.\lambda z.z)</tex><tex> ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (div ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m))) n m) m)) (\lambda s.\lambda z.z))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (list))</tex><tex> ((\lambda i.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> (i))</tex><tex> p (f ((\lambda p.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda p.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (p)</tex><tex> i) (\lambda a.\lambda b.a)</tex><tex> ((\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m)) p i)) (\lambda a.\lambda b.b)</tex><tex> (f p ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (i)))))</tex><tex> p (\lambda s.\lambda z.s (s z)))</tex><tex> (p))</tex><tex> p (f ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (p))))</tex><tex> ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (p)))</tex><tex> (p))</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (i))))</tex><tex> (\lambda s.\lambda z.s (s z))</tex><tex> i) ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (list))))</tex>
  
list2 = norm $ cons `App` one' `App` empty
 
list32 = cons `App` zero' `App` list2
 
  
normFiveFact = normIO 0 $ fact' `App` five'
+
====tail====
 +
<tex>\lambda list.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (list)))</tex><tex> ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m)) n m)) (f ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda div.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) (\lambda s.\lambda z.z)</tex><tex> ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (div ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m))) n m) m) n) ((\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (list))</tex><tex> ((\lambda i.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> (i))</tex><tex> p (f ((\lambda p.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda p.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (p)</tex><tex> i) (\lambda a.\lambda b.a)</tex><tex> ((\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m)) p i)) (\lambda a.\lambda b.b)</tex><tex> (f p ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (i)))))</tex><tex> p (\lambda s.\lambda z.s (s z)))</tex><tex> (p))</tex><tex> p (f ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (p))))</tex><tex> ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (p)))</tex><tex> (p))</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (i))))</tex><tex> (\lambda s.\lambda z.s (s z))</tex><tex> i) ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (list)))))</tex>
  
-- fiftysix = mult twentyeight two
+
== См. также ==
-- fiftyfive = pred fiftysix
+
*[[Неразрешимость задачи вывода типов в языке с зависимыми типами]]
-- six = pred seven
 
  
--main = do print $ fiftysix (+1) 0
+
==Источники информации==
main = do
+
* Lectures on the Curry Howard - Isomorphism
--  f <- normIO 0 $ ithPrime `App` three'
+
*[https://github.com/shd/tt2014 Д. Штукенберг. Лекции]
--  f <- normIO 0 $ getExponent `App` (norm $ plus' `App` four' `App` four') `App` two'
+
*[http://en.wikipedia.org/wiki/Lambda-calculus Английская Википедия]
    f <- normIO 0 $ head `App` (tail `App` list32)
+
*[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 Русская Википедия]
    print $ toInt f
+
*[http://worrydream.com/AlligatorEggs Игра про крокодилов]
\end{code}
 
}
 
  
\end{document}
+
[[Категория: Теория формальных языков]]
[http://rain.ifmo.ru/~komarov/Turing.lhs]
+
[[Категория: Теория вычислимости]]

Текущая версия на 19:42, 4 сентября 2022

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

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

Определение:
Лямбда-выражением (англ. [math]\lambda[/math]-term) называется выражение, удовлетворяющее следующей грамматике:

[math] \Lambda \to V\\ \Lambda \to \Lambda \ \Lambda\\ \Lambda \to \lambda V . \Lambda [/math]

где [math]V[/math] — множество всех строк над фиксированным алфавитом [math] \Sigma \setminus \{ "\lambda", "\ ",\ "."\} [/math].

Пробел во втором правиле является терминалом грамматики. Иногда его обозначают как @, чтобы он не сливался с другими символами в выражении.

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

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

Еще примеры:

[math] x\\ (x\ z)\\ (\lambda x.(x\ z))\\ (\lambda z.(\lambda w.((\lambda y.((\lambda x.(x\ z))\ y))\ w)))\\ [/math]

Иногда [math]\lambda[/math] -термы пишут по другому. Для краткости подряд идущие лямбды заменяют на одну. Например:

[math]\lambda x\ .\ \lambda y\ .P\ \to\ \lambda xy.P[/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\ .\ 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]\alpha[/math] -equivalence) — называется наименьшее соотношение эквивалентности на [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]\beta[/math] -reduction) — это наименьшее соотношение на [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]\beta[/math]-редукции вполне возможна функция вида [math]\lambda x. \lambda x.x[/math]. Во время подстановки вместо [math]x[/math] внутренняя переменная не заменяется - действует принцип локальной переменной. Но принято считать, что таких ситуаций не возникает и все переменные называются разными именами.

Каррирование

Определение:
Каррирование (англ. carrying) — преобразование функции от многих переменных в функцию, берущую свои аргументы по одному. Для функции [math]h[/math] типа [math]h\ :\ (A\ *\ B)\ \to\ C[/math] оператор каррирования [math]\Lambda [/math] выполняет преобразование [math]\Lambda (h)\ :\ A\to (B\to C)[/math]. Таким образом [math]\Lambda (h)[/math] берет аргумент типа [math]A[/math] и возвращает функцию типа [math]B\ \to\ C[/math]. С интуитивной точки зрения, каррирование функции позволяет фиксировать ее некоторый аргумент, возвращая функцию от остальных аргументов. Таким образом, [math]\Lambda[/math] представляет собой функцию типа [math]\Lambda :\ (A\ *\ B\to C)\to (A\to (B\to C))[/math].


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

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

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

Грамматику нотации можно задать как:

[math]e\ ::= n\ |\ \lambda .e\ |\ e\ e[/math]

Примеры выражений в этой нотации:

Standart de Bruijn
$\lambda x.x$ $\lambda .0$
$\lambda z.z$ $\lambda .0$
$\lambda x. \lambda y.x$ $\lambda . \lambda .1$
$\lambda x. \lambda y. \lambda s. \lambda z.x\ s\ (y\ s\ z)$ $\lambda . \lambda . \lambda . \lambda .3\ 1(2\ 1\ 0)$
$(\lambda x.x\ x)(\lambda x.x\ x)$ $(\lambda .0\ 0)(\lambda .0\ 0)$
$(\lambda x. \lambda x.x)(\lambda y.y)$ $(\lambda .\lambda .0)(\lambda .0)$

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

При [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

Функция, прибавляющая [math]1[/math] к числу, должна принимать первым аргументом число. Но число — функция двух аргументов. Значит, эта функция должна принимать три аргумента: "число" [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](\operatorname{plus}\ ((\operatorname{plus}\ 2\ 5)(+1)\ 0)\ 4)(+1)0 \equiv 11[/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 \to \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]Y[/math]-комбинатор, введенный известным американским ученым Хаскеллом Карри как

[math]Y\ = \ \lambda f.(\lambda x.f(x\ x))\ (\lambda x.f(x\ x))[/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] — принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от [math]2[/math] до [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]

См. также

Источники информации