Изменения

{{В разработке}} == '''Лямбда-исчисление== ''Лямбда-исчисление' (''англ. 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>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> {{---}} нет.редукция===

\subsection{${Определение|definition='''<tex>\beta$</tex>-редукция}$''' (англ. ''<tex>\beta$</tex> -reduction'') {{---редукция олицетворяет идею счёта значения функции. Выражение вида }} это наименьшее соотношение на <tex>\Lambda</tex> такое что|:<tex>(\lambda x -> f.P) y| можно заменить на $fQ\to _\beta P[x := yQ]$, где $f[</tex>и замкнуто относительно следующих правил:<tex>P\to _\beta P' \Rightarrow \forall x\in V:=y]$, как и ранее, означаетзамену всех свободных вхождений $\lambda x.P\to _\beta \lambda x$ в $f$ на $y$.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> }}

{{Определение|definition=Через $<tex>f \to_\beta g$ </tex> обозначают сведение $<tex>f$ </tex> к $<tex>g$ </tex> с помощью одной $<tex>\beta$</tex>-редукции.А через $<tex>f \to_\beta^* g$~</tex> {{--- }} за ноль или более.}} В <tex>\beta</tex>-редукции вполне возможна функция вида <tex>\lambda x. \lambda x.x</tex>. Во время подстановки вместо <tex>x</tex> внутренняя переменная не заменяется - действует принцип локальной переменной. Но принято считать, что таких ситуаций не возникает и все переменные называются разными именами.

$\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>\subsectionoperatorname{Параpair}= \lambda a\ .\ \lambda b\ .\ \lambda t\ .\ t\ a\ b</tex>

<tex>\beginoperatorname{codefst}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{codetrue}</tex>

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

Функция <tex>\subsectionoperatorname{Вычитание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>, вычитаниесоответственно.

\begin{code}minus' = Lam "n" $ Lam "m" $ Var "m" `App` pred' `App` Var "n"==Вычитание===\end{code}В отличие от всех предыдущих функций, вычитание для натуральных чисел определено только в случае, если уменьшаемое больше вычитаемого. Положим в противном случае результат равным нулю. Пусть уже есть функция, которая вычитает из числа единицу. Тогда на её основе легко сделать, собственно, вычитание.

<<$tex>\operatorname{minus} = \lambda n\ .\ \lambda m\ .\ m$ раз вычесть единицу из $\ \operatorname{pred} n$></tex>.

Осталось, собственно, функция для вычитания единицы. Однако, это не так просто,как может показаться на первый взгляд. Проблема в том, что, имея функцию, которуюнужно применить для того, чтобы продвинуться вперёд, продвинуться назад будетпроблематично. Если попробовать воспользоваться идеей о том, чтобы, начав от нуля, идти вперёд, и пройти на один шаг меньше, Это то будет не очень понятно, какже остановиться ровно за один шаг до конца. Для реализации вычитания единицы сделаем следующее. $n$ раз выполним следующее: имея пару $(n-1самое, n-2)$ построим пару$(n, n-1)$. Тогда после $n$ шагов во втором элементе пары будет записано число$n-1$, которое и хочется получить.% --pred = \n -что <tex> \s -m</tex> \z -раз вычесть единицу из <tex> n (\g -</tex> \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>n</tex> раз выполним следующее: имея пару <tex>\begin{code}pred' = Lam "langle n" $ Lam "s" $ Lam "z" $ snd'' `App` (Var "-1, 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" ) )-2\rangle</tex> построим пару <tex>\end{code}langle n, n-1\rangle</tex>. Тогда после <tex>n</tex> шагов во втором элементе пары будет записано число <tex>n-1</tex>, которое и хочется получить.

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

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

\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' Так как вычитание определено таким способом, чтобы для случая, в котором уменьшаемое больше, чем вычитаемое, возвращать ноль, можно определить сравнение на больше-меньше через него. Равными же числа <tex>a</tex> и <tex>b</tex> считаются, если <tex>a - b = 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"))0 \end{code}wedge b - a = 0</tex>.

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

<tex>\beginoperatorname{specless}fact = \x -> if lambda n\ .\ \lambda m\ .\ \operatorname{le}\ n\ (isZero x) one (fact (pred x))\endoperatorname{specpred}m)</tex>

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

\begin{spec}===Комбинатор неподвижной точки===fact = (\f Попробуем выразить в лямбда-> \x исчислении какую-> if (isZero x) one (f (pred x))) fact\end{spec}нибудь функцию, использующую рекурсию. Например, факториал.

<tex>\emphoperatorname{Неподвижной точкойfact} лямбда-функции $f$ назовём такую функцию $= \lambda x$, что$f \ .\ \operatorname{if}\ (\operatorname{isZero}\ x )\ \bar 1\to_(\operatorname{fact}\ (\operatorname{pred}\beta x$. Лямбда исчисление обладаем замечательным свойством: у каждойфункции есть неподвижная точка!))</tex>

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

<tex>\beginoperatorname{codefact}fix' = Lam "(\lambda f" $ (Lam "\ .\ \lambda x" $ Var "f" `App` \ .\ \operatorname{if}\ (Var "x" `App` Var "\operatorname{isZero}\ x")) `App` \ \bar 1\ (Lam "x" $ Var "f" `App` \ (Var "\operatorname{pred}\ x" `App` Var "x")))\ \endoperatorname{codefact}</tex>

{{Определение|definition=''Неподвижной точкой'' лямбда-функции <tex>f</tex> назовём такую функцию <tex>x</tex>, что<tex>f\ x \to_\beta^* x</tex>. }} Лямбда исчисление обладаем замечательным свойством: у каждой функции есть неподвижная точка! Рассмотрим следующую функцию.  <tex>\operatorname{fix} = \lambda f\ .\ (\lambda x\ .\ f\ (x\ x))\ (\lambda x\ .\ f\ (x\ x))</tex> Заметим, что $<tex>\operatorname{fix' } \to_\beta ^* \lambda f \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\ (\operatorname{succ}\ i)))</tex> <tex>\endoperatorname{codeisPrimeHelp} = \operatorname{fix}\ \operatorname{isPrimeHelp'}</tex>

<tex>\subsectionoperatorname{Проверка на простотуisPrime}= \lambda p\ .\ \operatorname{isPrimeHelp}\ p\ \bar 2</tex>

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

<tex>\beginoperatorname{codenextPrime''}isPrimeHelp' = Lam "\lambda f" $ Lam "\ .\ \lambda p" $ Lam "i" $ \ .\ \operatorname{if'' `App` }\ (le' `App` Var "\operatorname{isPrime}\ 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` \ (\operatorname{succ' `App` Var "i")}\ p) )isPrimeHelp = fix' `App` isPrimeHelp'isPrime = Lam "p" $ isPrimeHelp `App` Var "p" `App` two'\end{code}</tex>

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

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

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

<tex>\beginoperatorname{code}ithPrimeStep' } = Lam "\lambda f" $ Lam "\ .\ \lambda p" $ Lam "\ .\ \lambda i" $ \ .\ \operatorname{if'' `App` }\ (\operatorname{isZero' `App` Var "}\ i") `App` Var "\ p" `App` \ (Var "f" `App` \ (\operatorname{nextPrime `App` Var "}\ p") `App` \ (\operatorname{pred' `App` Var "}\ i"))ithPrimeStep = fix' `App` ithPrimeStep'ithPrime = Lam "i" $ ithPrimeStep `App` two' `App` Var "i"\end{code}</tex>

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

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