Изменения

{{В разработке}} == '''Лямбда-исчисление== ''Лямбда-исчисление' (''англ. 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>x\\(x\ z)\\(\lambda x.(x\ z))\\(\lambda z.(\lambda w.((\lambda y.((\lambda x.(x\ z))\ y))\ w)))\\ </tex>

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

Функции, получающиеся одна из другой с помощью <tex>\lambda x\ .\ \lambda y\ .\ x\ y\ z</tex> и <tex>\lambda a\ .\ \lambda x\ .\ a\ x\ z</tex> являются <tex>\alpha</tex>-конверсийэквивалентными, называются ''а <tex>\alphalambda x\ .\ \lambda y\ .\ y\ z</tex>-эквивалентными'' и обозначаются <tex>f \equiv_lambda y\ .\ \lambda x\ .\alpha gy\ 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>β-редукция===

'''<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>f \to_\beta^* g</tex>~{{--- }} за ноль или более.

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

$\eta$-редукция~{{Определение|definition='''Каррирование''' (англ. ''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\x -to C))</tex> f x| в $f$.}}

\section{==Нотация Де Брюина}Брауна==Существует также альтернативное эквивалентное определение $<tex>\lambda$</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$|-| $\betalambda 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)$|}

При $<tex>\beta$</tex>-редукции же нужно будет ко всем свободным переменным заменяющего

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

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

\subsection{===Определение}===

что натуральное число~{{--- }} это или ноль, или увеличенное на единицу натуральное

:<tex>\begin{code}zero' bar 0 = Lam "\lambda s" $ Lam "\ .\ \lambda z" $ Var "\ .\ z"</tex>one' :<tex>\bar 1 = Lam "\lambda s" $ Lam "\ .\ \lambda z" $ Var "\ .\ s" `App` Var "\ z"</tex>two' :<tex>\bar 2 = Lam "\lambda s" $ Lam "\ .\ \lambda z" $ Var "\ .\ s" `App` \ (Var "s" `App` Var "\ z")</tex>three' :<tex>\bar 3 = Lam "\lambda s" $ Lam "\ .\ \lambda z" $ Var "\ .\ s" `App` \ (Var "s" `App` \ (Var "s" `App` Var "\ z"))\end{code}</tex>

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

|three <tex>\bar 3\ (+1) \ 0 == | \eval{three (+1) 0}equiv 3</tex>.

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

<tex>\beginoperatorname{codesucc}succ' = Lam "\lambda n" $ Lam "\ .\ \lambda s" $ Lam "\ .\ \lambda z" $ Var "\ .\ s" `App` \ (Var "n" `App` Var "\ s" `App` Var "\ z")\end{code}</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>.

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

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

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

|<tex>(plus three three) (+1) 0 == | \evaloperatorname{(plus three three}\ \bar 3\ \bar 3) \ (+1) \ 0}\equiv 6</tex>

<tex>(\subsectionoperatorname{plus}\ ((\operatorname{plus}\ 2\ 5)(+1)\ 0)\ 4)(+1)0 \equiv 11</tex>  ===Умножение}===

функции должна быть не $<tex>s$</tex>, а функция, применяющая $<tex>n$ </tex> раз $<tex>s$</tex>.

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

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

<tex>\beginoperatorname{specmult}mult = \lambda n -> \.\ \lambda m -> \.\ \lambda s -> \ .\ n \ (m \ s)\end{spec}</tex>

|<tex>(mult three three) (+1) 0 == | \evaloperatorname{(mult three three} \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>\operatorname{fst} = \lambda p\ .\ p\ \operatorname{true}</tex> <tex>\operatorname{snd} = \lambda p\ .\ p\ \operatorname{false}</tex> Функция <tex>\operatorname{pair}</tex> принимает два значения и запаковывает их в пару так, чтобы к ним можно было обращаться по <tex>\operatorname{fst}</tex> и <tex>\operatorname{snd}</tex>. В <tex>\operatorname{fst}</tex> и <tex>\operatorname{snd}</tex> вместо <tex>t</tex> в <tex>\operatorname{pair}</tex> будет подставлено <tex>\operatorname{true}</tex> или <tex>\operatorname{false}</tex>, возвращающие, соответственно, первый и второй аргументы, то есть <tex>a</tex> или <tex>b</tex>, соответственно.

<tex>\beginoperatorname{codeminus}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'\endlambda n\ .\ \lambda m\ .\ m\ \operatorname{codepred}n</tex>

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

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

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

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

Осталось, собственно, функция для вычитания единицы. Однако, это не так просто,===Сравнение===Так как может показаться на первый взгляд. Проблема в томвычитание определено таким способом, что, имея функцию, которуюнужно применить чтобы для тогослучая, чтобы продвинуться вперёдв котором уменьшаемое больше, продвинуться назад будетпроблематично. Если попробовать воспользоваться идеей о томчем вычитаемое, чтобывозвращать ноль, начав от нуля, идти вперёд, и пройти можно определить сравнение на один шаг больше-меньше, то будет не очень понятно, какчерез него. Равными же остановиться ровно за один шаг до конца. Для реализации вычитания единицы сделаем следующее. $n$ раз выполним следующее: имея пару $(n-1, n-2)$ построим пару$(n, n-1)$. Тогда после $n$ шагов во втором элементе пары будет записано число$n-1$, которое и хочется получить.% --pred = \n -числа <tex> \s -a</tex> \z -и <tex> n (\g -b</tex> \h -> h (g s)) (\u -> z) (\u-считаются, если <tex>u)% a --pred b = 0 \n wedge b -> \s -> \z -> snd (n (\p -> (pair (s (fst p)) (fst p))) (pair z z))% --pred a = \n -0</tex> \s -> \z -> fst' (n (\p -> pair (s (fst p))(fst p)) (pair z z)).

<tex>\beginoperatorname{codele}pred' = Lam "\lambda n" $ Lam "s" $ Lam "z" $ snd'' `App` (Var "n" `App` ( Lam "p" $ pair' `App` (Var "s" `App` (fst'' `App` Var "p")) `App` \ .\ \lambda m\ .\ \operatorname{isZero}\ (fst'' `App` Var "p") ) `App` ( pair' `App` Var "z" `App` Var "z" ) )\endoperatorname{codeminus}\ n\ m)</tex>

Если вы ничего не поняли, не огорчайтесь<tex>\operatorname{less} = \lambda n\ . Вычитание придумал Клини, когда ему вырывали зуб мудрости\ \lambda m\ . А сейчас наркоз уже не тот!\ \operatorname{le}\ n\ (\operatorname{pred} m)</tex>

<tex>\subsectionoperatorname{Сравнениеeq}Так как вычитание определено таким способом, чтобы для случая, в которомуменьшаемое больше, чем вычитаемое, возвращать ноль, можно определитьсравнение на больше-меньше через него= \lambda n\ .\ \lambda m\ . Равными же числа $a$ и $b$ считаются, \ \operatorname{and}\ (\operatorname{isZero}\ (\operatorname{minus}\ n\ m))\ если $a - b = 0 (\operatorname{isZero}\ (\operatorname{minus}\ m\wedge b - a = 0$.n))</tex>

\begin{code}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}Попробуем выразить в лямбда-исчислении какую-нибудь функцию, использующую рекурсию. Например, факториал.

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

Мы столкнулись с проблемой. В определении функции <tex>\beginoperatorname{specfact}fact = \x -</tex> используется функция <tex> if (isZero x) one (fact (pred x))\endoperatorname{specfact}</tex>. При формальной замене, получим бесконечную функцию. Можно попытаться решить эту проблему следующим образом

Мы столкнулись с проблемой. В определении функции $<tex>\operatorname{fact$ используется функция $fact$} = (\lambda f\ . При формальной замене, получим бесконечную функцию\ \lambda x\ . Можно попытаться решить эту проблему следующим образом\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (f\ (\operatorname{pred}\ x)))\ \operatorname{fact}</tex>

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

\emph{Неподвижной точкой} лямбда-функции $f$ назовём такую функцию $x$, что$f x \to_\beta x$. Лямбда исчисление обладаем замечательным свойством: у каждойфункции есть неподвижная точка!

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

<tex>\beginoperatorname{codefix}fix' = Lam "\lambda f" $ \ .\ (Lam "\lambda x" $ Var "\ .\ f" `App` \ (Var "x" `App` Var "\ x")) `App` \ (Lam "\lambda x" $ Var "\ .\ f" `App` \ (Var "x" `App` Var "\ x"))\end{code}</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}\ \operatorname{mod' }</tex> ===Проверка на простоту== fix= <tex>\operatorname{isPrimeHelp}</tex> {{---}} принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от <tex>2</tex> до <tex>p-1</tex>. Если на что-нибудь разделилось, то число {{---}} составное, иначе {{---}} простое. <tex>\operatorname{isPrimeHelp' `App` } =</tex><tex>\lambda f\ .\ \lambda p\ .\ \lambda i\ .\ \operatorname{if}\ (\operatorname{le}\ p\ i)\ \operatorname{true}\ (\operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ p\ i))\ \operatorname{false}\ (f\ p\ (\operatorname{succ}\ i)))</tex> <tex>\operatorname{isPrimeHelp} = \operatorname{fix}\ \operatorname{isPrimeHelp'}</tex> <tex>\operatorname{isPrime} = \lambda p\ .\ \operatorname{isPrimeHelp}\ p\ \bar 2</tex> Следующее простое число. <tex>\operatorname{nextPrime';}</tex> {{---}} следующее, больше либо равное заданного, <tex>\endoperatorname{codenextPrime}</tex> {{---}}следующее, большее заданного.

<tex>\subsectionoperatorname{Проверка на простотуnextPrime''}= \lambda f\ .\ \lambda p\ .\ \operatorname{if}\ (\operatorname{isPrime}\ p)\ p\ (f\ (\operatorname{succ}\ p)) </tex>

<tex>\beginoperatorname{codenextPrime}isPrimeHelp' = Lam "f" $ Lam "\lambda p" $ Lam "i" $ if\ .\ \operatorname{nextPrime'' `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'\endoperatorname{codesucc}\ p)</tex>

Следующее простое <tex>\operatorname{ithPrimeStep}</tex> пропрыгает <tex>i</tex> простых чисел вперёд. <tex>\operatorname{ithPrime}</tex> принимает число. $nextPrime'$~--- следующее, больше либо равное заданного,$nextPrime$~--- следующее<tex>i</tex> и пропрыгивает столько простых чисел вперёд, большее заданногоначиная с двойки.

<tex>\beginoperatorname{codeithPrimeStep'}nextPrime'' = Lam "\lambda f" $ Lam "\ .\ \lambda p" $ \ .\ \lambda i\ .\ \operatorname{if'' `App` }\ (isPrime `App` Var "p"\operatorname{isZero}\ i) `App` Var "\ p" `App` \ (Var "f" `App` \ (succ' `App` Var "\operatorname{nextPrime}\ p")) nextPrime' = fix' `App` nextPrime''nextPrime = Lam "p" $ nextPrime' `App` \ (succ' `App` Var "p")\endoperatorname{codepred}\ i))</tex>

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

<tex>\beginoperatorname{codeithPrime}ithPrimeStep' = Lam "f" $ Lam "p" $ Lam "\lambda 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.\ \operatorname{codeithPrimeStep}\ \bar 2\ i</tex>

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

\subsection{===Списки}===

* <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Теория вычислимости]]