Изменения

{{В разработке}} == '''Лямбда-исчисление== ''Лямбда-исчисление' (''англ. lambda calculus'' ) {{---}} формальная система, придуманная в 1930-х годах

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

\begin{array}{r c l}Lambda \langle Term \rangle & ::= & \langle Variable \rangle to V\\ & || & \langle Term \rangle \langle Term \rangle \\ & || & \lambda \langle Variable \rangle Lambda \to \langle Term \rangle\\ & || & ( Lambda \langle Term \rangle )Lambda\\\langle Variable Lambda \rangle & ::= & to \langle Char \rangle *\\lambda V . \end{array}Lambda

Рассмотрим, например, функцию <tex>\lambda</tex>-терм <tex>\operatorname{id } = \lambda x \to .\ x</tex>. Эта функция принимает аргумент и

<tex>\operatorname{id }\ 2 \equiv 2</tex>. Аналогично, <tex>\operatorname{id }\ y == \equiv y</tex>.

Ещё один пример функцииЕще примеры:: <tex>sum = x\\(x\ z)\\(\lambda x.(x \to z))\\(\lambda z.(\lambda w.((\lambda y .((\to lambda x.(x + \ z))\ y|. Эта функция двух аргументов,))\ w)))\\ </tex> которая возвращает их суммуИногда <tex>\lambda</tex> -термы пишут по другому. Правда, здесь мы немного вышли за написанную выше грамматикуДля краткости подряд идущие лямбды заменяют на одну.Например:Ну да ладно. :<tex>sum 2 3 == 5\lambda x\ .\ \lambda y\ .P\ \to\ \lambda xy.P</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 \to .\lambda y \to x</tex>, <tex>x</tex> и связана, а <tex>y</tex>{{---}} свободна. А в <tex>\lambda y \to .\ x \ (\lambda x \to .\ x)</tex>

Связанные переменные {{---}} это аргументы функции. То есть для функции они являются локальными. Рассмотрим функции <tex>\lambda y \to .\ y</tex> и <tex>\lambda x \to .\ y</tex>. В первой из них при взгляде на <tex>y</tex>

<tex>\lambda x \to .\ \lambda x \to .\ \lambda y \to .\ \lambda x \to .\ 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>-конверсияэквивалентностью'' {{---}} переименование связанной переменной' (англ. Выражение''<tex>\lambda x \to falpha</tex> можно заменить -equivalence'') {{---}} называется наименьшее соотношение эквивалентности на <tex>\lambda y \to f[x := y]Lambda</tex>, если такое что::<tex>yP=_\alpha P</tex> не входит свободно в для любого <tex>fP</tex>,где :<tex>f\lambda x.P=_\alpha \lambda y.P[x:=y]</tex> означает замену всех свободных вхождений если <tex>xy \not\in FV(P)</tex> в и замкнуто относительно следующих правил::<tex>f</tex> на <tex>yP=_\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\ .\alpha</tex>-эквивалентными'' и обозначаются <tex>f \equiv_lambda y\alpha g</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>β-редукция===

'''<tex>\beta</tex>-редукция олицетворяет идею счёта значения функции''' (англ. Выражение вида ''<tex>(\lambda x \to f) ybeta</tex> можно заменить -reduction'') {{---}} это наименьшее соотношение на <tex>f[x := y]\Lambda</tex>, где такое что:<tex>f(\lambda x.P)Q\to _\beta P[x:=yQ]</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> в <tex>f</tex> на <tex>y</tex>.

===В <tex>\etabeta</tex>-редукция===Рассмотрим выражение редукции вполне возможна функция вида <tex>\lambda x . \to f lambda x.x</tex>. Если подставить в эту функцию значение <tex>yВо время подстановки вместо </tex>, то получим: <tex>(\lambda x \to f x) y \to_\beta f y</tex>внутренняя переменная не заменяется - действует принцип локальной переменной. Но если просто подставить<tex>y</tex> в <tex>f</tex>принято считать, то получится то же самоечто таких ситуаций не возникает и все переменные называются разными именами.  ===Каррирование===

'''Каррирование''' (англ. ''carrying'') {{---}} преобразование функции от многих переменных в функцию, берущую свои аргументы по одному. Для функции <tex>h</tex> типа <tex>h\eta:\ (A\ *\ B)\ \to\ C</tex>-редукция {{---}} оператор каррирования <tex>\Lambda </tex> выполняет преобразование <tex>\lambda x Lambda (h)\ :\ A\to (B\to C)</tex>. Таким образом <tex>\Lambda (h)</tex> берет аргумент типа <tex>A</tex> и возвращает функцию типа <tex>B\ \to f x\ C</tex> в . С интуитивной точки зрения, каррирование функции позволяет фиксировать ее некоторый аргумент, возвращая функцию от остальных аргументов. Таким образом, <tex>\Lambda</tex> представляет собой функцию типа <tex>f\Lambda :\ (A\ *\ B\to C)\to (A\to (B\to C))</tex>.

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

Это будет соответствовать тому, что эта переменная продолжит <<держаться>> «держаться» за

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

результат. Если такому <<"числу>> " дать на вход функцию <tex>(+1)</tex> и <tex>0</tex> в качестве

<tex>\bar 3 \ (+1) \ 0 \equiv 3</tex>.

Функция, прибавляющая <tex>1 </tex> к числу, должна принимать первым аргументом число.

аргумента: <<"число>> " <tex>n</tex>, которое хочется увеличить, функция, которую надо будет

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

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

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

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

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

Здесь <tex>m \ s</tex> {{---}} функция, которая <tex>m</tex> раз применит <tex>s</tex> к тому, что дадут ей на

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

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

\subsection{===Возведение в степень}===

<tex>\beginoperatorname{codepower}power' = Lam "\lambda n" $ Lam "\ .\ \lambda m" $ Var "\ .\ \lambda s\ .\ \lambda z\ .\ m" `App` Var "\ n"\end{code}s\ z</tex>

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

\subsection{===Логические значения}===<tex>\beginoperatorname{codetrue}true' = Lam "\lambda a" $ Lam "\ .\ \lambda b" $ Var "\ .\ a"</tex> <tex>\operatorname{false' } = Lam "\lambda a" $ Lam "\ .\ \lambda b" $ Var "\ .\ b"\end{code}</tex>

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

<tex>\beginoperatorname{codeif}if'' = Lam "\lambda p" $ Lam "\ .\ \lambda t" $ Lam "\ .\ \lambda e" $ Var "\ .\ p" `App` Var "\ t" `App` Var "\ e"\end{code}</tex>

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

<tex>\beginoperatorname{codeand}and' = Lam "\lambda n" $ Lam "\ .\ \lambda m" $ \ .\ \operatorname{if'' `App` Var "}\ n" `App` Var "\ m" `App` \ \operatorname{false'}</tex> <tex>\operatorname{or' } = Lam "\lambda n" $ Lam "\ .\ \lambda m" $ \ .\ \operatorname{if'' `App` Var "}\ n" `App` \ \operatorname{true' `App` Var "} \ m"</tex> <tex>\operatorname{not' } = Lam "\lambda b" $ \ .\ \operatorname{if'' `App` Var "}\ b" `App` \ \operatorname{false' `App` true'} \ \endoperatorname{codetrue}</tex>

<tex>\beginoperatorname{codeisZero}isZero' = Lam "\lambda n" $ Var "\ .\ n" `App` \ (Lam "\lambda c" \ .\ \operatorname{false'}) `App` true'\end\operatorname{codetrue}</tex>

Функция выглядит несколько странно. |<tex>\lambda c -\to \operatorname{false}</tex> false|~--- функция, которая независимоот того, что ей дали на вход, возвращает $<tex>\operatorname{false$}</tex>. Тогда, если в качестве $<tex>n$</tex>

возвращено значение по умолчанию $<tex>\operatorname{true$}</tex>. Иначе же функция будет запущено, и вернётся $<tex>\operatorname{false$}</tex>. ===Пара=== <tex>\operatorname{pair} = \lambda a\ .\ \lambda b\ .\ \lambda t\ .\ t\ a\ b</tex>

<tex>\subsectionoperatorname{Параfst}= \lambda p\ .\ p\ \operatorname{true}</tex>

<tex>\beginoperatorname{codesnd}pair' = Lam "a" $ Lam "b" $ Lam "t" $ Var "t" `App` Var "a" `App` Var "b"fst'' = Lam "\lambda p" $ Var "\ .\ p" `App` true'snd'' = Lam "p" $ Var "p" `App` false'\end\operatorname{codefalse}</tex>

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

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

<tex>\beginoperatorname{codeminus}minus' = Lam "\lambda n" $ Lam "\ .\ \lambda m" $ Var "\ .\ m" `App` pred' `App` Var "n"\end\operatorname{codepred}n</tex>

Это то же самое, что <tex>m<$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>, которое и хочется получить.% --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))

<tex>\beginoperatorname{codepred}pred' = Lam "\lambda n" $ Lam "\ .\ \lambda s" $ Lam "\ .\ \lambda z" $ .\ \operatorname{snd'' `App` }\ (Var " n" `App` \ ( Lam " \lambda p" $ \ .\ \operatorname{pair' `App` }\ (Var "s" `App` \ (\operatorname{fst'' `App` Var "} p")) `App` \ (\operatorname{fst'' `App` Var "} p") ) `App` \ ( \operatorname{pair' `App` Var "}\ z" `App` Var "\ z" ) )\end{code}</tex>

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

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

<tex>\beginoperatorname{codele}le' = Lam "\lambda n" $ Lam "\ .\ \lambda m" $ \ .\ \operatorname{isZero' `App` }\ (\operatorname{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}</tex>

<tex>\subsectionoperatorname{Комбинатор неподвижной точкиless}Попробуем выразить в лямбда-исчислении какую-нибудь рекурсивную функцию= \lambda n\ .Напрмер, факториал\ \lambda m\ .\ \operatorname{le}\ n\ (\operatorname{pred} m)</tex>

<tex>\beginoperatorname{speceq}fact = \x -> if lambda n\ .\ \lambda m\ .\ \operatorname{and}\ (\operatorname{isZero x) one }\ (fact (pred x\operatorname{minus}\ n\ m))\ (\operatorname{isZero}\end(\operatorname{specminus}\ m\ n))</tex>

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

<tex>\beginoperatorname{specfact}fact = (\f -> lambda x\ .\ \x -> operatorname{if }\ (\operatorname{isZero }\ x) one \ \bar 1\ (f \operatorname{fact}\ (\operatorname{pred }\ x))) fact\end{spec}</tex>

Мы столкнулись с проблемой. В определении функции <tex>\operatorname{fact}</tex> используется функция <tex>\emphoperatorname{Неподвижной точкойfact} лямбда-функции $f$ назовём такую </tex>. При формальной замене, получим бесконечную функцию $x$, что$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|definition=' = Lam "f" $ (Lam "x" $ Var "'Неподвижной точкой'' лямбда-функции <tex>f" `App` (Var "</tex> назовём такую функцию <tex>x" `App` Var "x"))</tex>, что `App` (Lam "x" $ Var "<tex>f" `App` (Var "\ x" `App` Var "\to_\beta^* x"))</tex>. \end{code}}

Лямбда исчисление обладаем замечательным свойством: у каждой функции есть неподвижная точка! Рассмотрим следующую функцию.  <tex>\operatorname{fix} = \lambda f\ .\ (\lambda x\ .\ f\ (x\ x))\ (\lambda x\ .\ f\ (x\ x))</tex> Заметим, что $<tex>\operatorname{fix' } \to_\beta ^* \lambda f \to .\ f \ ((\lambda x \to .\ f \ (x \ x)) \ (\lambda x \to .\ f \ (x \ x)))$</tex>.

$<tex>\lambda f \to .\ (\lambda x \to .\ f \ (x \ x)) \ (\lambda x \to .\ f \ (x \ x)) \to_\beta^*</tex> <tex>\lambda f \to .\ f \ ((\lambda x \to .\ f \ (x \ x)) \ (\lambda x \to .\ f \ (x \ x)))$</tex>

<tex>\beginoperatorname{code}fact'' } = Lam "\lambda f" $ Lam "\ .\ \lambda x" $ \ .\ \operatorname{if'' `App` }\ (\operatorname{isZero' `App` Var "}\ x") `App` one' `App` \ \bar 1\ (\operatorname{mult' `App` Var "}\ x" `App` \ (Var "f" `App` \ (\operatorname{pred' `App` Var "}\ x")))\end{code}</tex>

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

<tex>\beginoperatorname{codefact}fact' = \operatorname{fix' `App` }\ \operatorname{fact''\end{code}</tex>

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

Тут правда ничего не понятно? Наиболее известным комбинатором неподвижной точки является <tex>Y</tex>-комбинатор, введенный известным американским ученым Хаскеллом Карри как:'<tex>Y\ = \ \lambda f.(\lambda x.f(x\ x))\ (\lambda x.f(x\ x))</tex>

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

<tex>\beginoperatorname{code}div'' } = Lam "\lambda div" $ Lam "\ .\ \lambda n" $ Lam "\ .\ \lambda m" $ \ .\ \operatorname{if'' `App` }\ (\operatorname{less' `App` Var "}\ n" `App` Var "\ m") `App` zero' `App` \ \bar 0\ (\operatorname{succ' `App` }\ (Var "div" `App` \ (\operatorname{minus' `App` Var "}\ n" `App` Var "\ m") `App` Var "\ m"))</tex> <tex>\operatorname{div' } = \operatorname{fix' `App` }\ \operatorname{div''\end{code}</tex>

<tex>\beginoperatorname{code}mod'' } = Lam "\lambda mod" $ Lam "\ .\ \lambda n" $ Lam "\ .\ \lambda m" $ \ .\ \operatorname{if'' `App` }\ (\operatorname{less' `App` Var "}\ n" `App` Var "\ m") `App` Var "\ n" `App` \ (Var "mod" `App` \ (\operatorname{minus' `App` Var "}\ n" `App` Var "\ m") `App` Var "\ m")</tex> <tex>\operatorname{mod' } = \operatorname{fix' `App` }\ \operatorname{mod'}</tex> ===Проверка на простоту=== <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\ (\endoperatorname{codesucc}\ i)))</tex>

<tex>\subsectionoperatorname{Проверка на простотуisPrimeHelp}= \operatorname{fix}\ \operatorname{isPrimeHelp'}</tex>

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

Следующее простое число. <tex>\beginoperatorname{codenextPrime'}</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'} следующее, больше либо равное заданного, <tex>\endoperatorname{codenextPrime}</tex> {{---}}следующее, большее заданного.

Следующее простое число. $<tex>\operatorname{nextPrime'$~--- следующее, больше либо равное заданного,$nextPrime$~--- следующее, большее заданного'} = \lambda f\ .\ \lambda p\ .\ \operatorname{if}\ (\operatorname{isPrime}\ p)\ p\ (f\ (\operatorname{succ}\ p)) </tex>

<tex>\beginoperatorname{code}nextPrime'' = Lam "f" $ Lam "p" $ if'' `App` (isPrime `App` Var "p") `App` Var "p" `App` (Var "f" `App` (succ' `App` Var "p")) nextPrime' } = \operatorname{fix' `App` nextPrime''nextPrime = Lam "p" $ }\ \operatorname{nextPrime' `App` (succ' `App` Var "p")\end{code}</tex>

$ithPrimeStep$ пропрыгает $i$ простых чисел вперёд. $ithPrime$ принимает число$i$ и пропрыгивает столько простых чисел вперёд, начиная с двойки<tex>\operatorname{nextPrime} = \lambda p\ .\ \operatorname{nextPrime'}\ (\operatorname{succ}\ p)</tex>

<tex>\beginoperatorname{codeithPrimeStep}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 "</tex> пропрыгает <tex>i"</tex> простых чисел вперёд. <tex>\endoperatorname{codeithPrime}</tex> принимает число <tex>i</tex> и пропрыгивает столько простых чисел вперёд, начиная с двойки.

<tex>\operatorname{ithPrimeStep'} = \lambda f\ .\ \lambda p\ .\ \lambda i\ .и всего через 314007 $\beta$-редукций вы узнаете, что третье простое число~---семь!\operatorname{if}\ (\operatorname{isZero}\ i)\ p\ (f\ (\operatorname{nextPrime}\ p)\ (\operatorname{pred}\ i))</tex>

<tex>\subsectionoperatorname{ithPrimeStep} = \operatorname{fix}\ \operatorname{ithPrimeStep'}</tex> <tex>\operatorname{ithPrime} = \lambda i\ .\ \operatorname{ithPrimeStep}\ \bar 2\ i</tex> ...и всего через 314007 <tex>\beta</tex>-редукций вы узнаете, что третье простое число {{---}} семь! ===Списки}===

* <tex>\beginoperatorname{itemizeempty} \item $empty$~</tex> {{--- }} возвращает пустой список * <tex>\item $operatorname{cons$~}</tex> {{--- }} принимает первый элемент и оставшийся список, склеивает их * <tex>\item $operatorname{head$~}</tex> {{--- }} вернуть голову списка * <tex>\item $operatorname{tail$~}</tex> {{--- }} вернуть хвост списка Список будем хранить в следующем виде: <tex>\langle len, p_1^{a_1}p_2^{a_2}\ldots p_{len}^{a_{len}} \endrangle</tex>. При этом, голова списка будет храниться как показатель степени при <tex>p_{itemizelen}</tex>. <tex>\operatorname{empty} = \operatorname{pair}\ \operatorname{zero}\ \bar 1</tex> <tex>\operatorname{cons} = \lambda h\ .\ \lambda t\ .\ \operatorname{pair}\ (\operatorname{succ}\ (\operatorname{fst}\ t))\ (\operatorname{mult}\ (\operatorname{snd}\ t)\ (\operatorname{power}\ (\operatorname{ithPrime}\ (\operatorname{fst}\ t))\ h))</tex> <tex>\operatorname{head} = \lambda list\ .\ \operatorname{getExponent}\ (\operatorname{snd}\ list)\ (\operatorname{ithPrime}\ (\operatorname{pred}\ (\operatorname{fst}\ list)))</tex> <tex>\operatorname{tail} = \lambda list\ .\ \operatorname{pair}\ (\operatorname{pred}\ (\operatorname{fst}\ list)) (\operatorname{eliminateMultiplier}\ (\operatorname{snd}\ list)\ (\operatorname{ithPrime}\ (\operatorname{pred}\ (\operatorname{fst}\ list))))</tex>

Список будем хранить в следующем виде: $<tex>\langle len, p_1^operatorname{a_1eliminateMultiplier'}p_2^=</tex><tex> \lambda f\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{a_2if}\ldots p_(\operatorname{lenisZero}^{a_\ (\operatorname{len}mod} \rangle$. При этом, голова списка будет храниться как показатель степени при $p_n\ m))\ (f\ (\operatorname{lendiv}$.\ n\ m)\ m)\ n</tex>

<tex>\beginoperatorname{codeeliminateMultiplier}empty = pair\operatorname{fix}\ \operatorname{eliminateMultiplier' `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")))}</tex>

tail <tex>\operatorname{getExponent'} = Lam "list" $ pair' `App` </tex><tex> \lambda f\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (pred' `App` \operatorname{isZero}\ (fst'' `App` Var "list"\operatorname{mod}\ n\ m)) `App` (eliminateMultiplier `App` (snd'' `App` Var "list") `App` \ (ithPrime `App` \operatorname{succ}\ (pred' `App` f\ (fst'' `App` Var "list" )\operatorname{div}\ n\ m)\ m) )\ \bar 0</tex>

eliminateMultiplier' = Lam "f" $ Lam "n" $ Lam "m" $ if'' `App` (isZero' `App` (mod' `App` Var "n" `App` Var "m")) `App` (Var "f" `App` (div' `App` Var "n" `App` Var "m") `App` Var "m") `App` Var "n"eliminateMultiplier <tex>\operatorname{getExponent} = \operatorname{fix}\ \operatorname{getExponent' `App` eliminateMultiplier'}</tex>

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> я не дождался окончания выполнения. Скорость лямбда-исчисления как вычислителяпечальна.

four' = norm $ succ' `App` three'===fact====<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>five' = norm $ succ' `App` four'===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>

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) 0main = doИсточники информации== * Lectures on the Curry Howard -- f <- normIO 0 $ ithPrime `App` three'Isomorphism*[https://github.com/shd/tt2014 Д. Штукенберг. Лекции] -- f <*[http://en.wikipedia.org/wiki/Lambda- normIO 0 $ getExponent `App` (norm $ plus' `App` four' `App` four') `App` two'calculus Английская Википедия] f <*[http://ru.wikipedia.org/wiki/%D0%9B%D1%8F%D0%BC%D0%B1%D0%B4%D0%B0- normIO 0 $ head `App` (tail `App` list32) print $ toInt f\end{code}%D0%B8%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5 Русская Википедия]}*[http://worrydream.com/AlligatorEggs Игра про крокодилов]

\end{document}[[Категория: Теория формальных языков]][http[Категория://rain.ifmo.ru/~komarov/Turing.lhsТеория вычислимости]]