Изменения

{{В разработке}} \documentclass[11pt,a4paper,oneside]{article} \usepackage[english,russian]{babel}\usepackage[T2A]{fontenc}\usepackage[utf8]{inputenc}\usepackage{graphicx}\usepackage{expdlist}\usepackage{mfpic}\usepackage{comment}\usepackage{listings}\usepackage{epigraph}\usepackage{url}\usepackage{array}%include polycode.fmt%options ghci%format Var v = v%format App x y = x "\times" y%format `App` = " \cdot "%format Lam x = "\lambda" x "\to"%format if' = if%format then' = then%format else' = else%format $ = " " \long\def\ignore#1{} \begin{document} \ignore{\begin{code}import Prelude hiding (id, succ, pred, and, or, catch, head, tail)import qualified Prelude as P\end{code}} \ignore{\begin{code}import Control.Exceptionimport Control.Monad.Stateimport qualified Data.Map as Mimport Data.Maybe (fromMaybe) type Variable = Stringdata Term = Var Variable | Lam Variable Term | App Term Term deriving (Ord) instance Show Term where show (Var x) = x show (Lam x e) = "\\" ++ x ++ "." ++ show e show (App e1@(Lam _ _) e2) = "(" ++ show e1 ++ ") (" ++ show e2 ++ ")" show (App e1 (Var v)) = show e1 ++ " " ++ v show (App e1 e2) = show e1 ++ " (" ++ show e2 ++ ")" free (Var v) = [ v ]free (Lam v t) = filter (/= v) . free $ tfree (App t t') = (free t) ++ (free t') subst :: Term Лямбда-> Variable -> Term -> Termsubst t@(Var v) var what = if v == var then what else tsubst t@(Lam v b) var what = if v == var then t else Lam v (subst b var what)subst (App t t') var what = App (subst t var what) (subst t' var what) newname :: [Variable] -> Variable -> Variable newname fv = P.head . filter (not . flip elem fv) . iterate ('_':) deny:: [String] -> Term -> Termdeny d (Var v) = Var v -- Var $ newname d vdeny d (Lam v t) = Lam vисчисление' $ subst t v (Var v') where v' = newname (d ++ free t) vdeny d (App t1 t2) = App (deny d t1) (deny d t2) unifyBound :: Term -> Term unifyBound e = fst $ runState (unifyBound' e) (M.empty, free e) unifyBound' :: Term -> State (M.Map Variable Variable, [Variable]) TermunifyBound' (Var v) = do (m, used) <- get return $ Var $ fromMaybe v (Mангл.lookup v m)unifyBound' e@(App t1 t2) = do t1' <- unifyBound' t1 t2' <- unifyBound' t2 return $ App t1' t2lambda calculus'unifyBound' (Lam x t) = do (m, used) <- get let new = fst $ runState unused used put (M.insert x new m, new:used) e <- unifyBound' t (_, used') <- get put (m, used') return $ Lam new e eq :: Term -> Term -> Booleq (Var v) (Var v') = v == v'eq (Lam v1 e1) (Lam v2 e2) = v1 == v2 && e1 `eq` e2eq (App e1 e2) (App e1' e2') = e1 `eq` e1' && e2 `eq` e2'eq _ _ = False instance Eq Term where e1 == e2 = free e1 == free e2 && newE1 `eq` newE2 where newE1 = unifyBound e1 newE2 = unifyBound e2 fv = free e1 unused :: State [Variable] Variableunused = do used <- get let new = P.head $ filter (not . (`elem` used)) $ map show [1..] put $ new:used return new  no :: Integer -> Term -> Term no n t = no' n ({- unifyBound -} t) no' 0 t = error $ "Too long sequence at [" ++ show t ++ "]"no' n t | reduced = no (n - 1) rest | otherwise = t where (reduced, rest) = noOne t noOne :: Term -> (Bool, Term)noOne (App (Lam v t1) t2) = (True, subst (deny (free t2) t1) v t2)noOne t@(Var v) = (False, t)noOne (Lam v t) = (reduced, Lam v rest) where (reduced, rest) = noOne t noOne t@(App t1 t2) = if reducedLeft then (True, App t1' t2) else if reducedRight then (True, App t1 t2') else (False, t) where (reducedLeft, t1') = noOne t1 (reducedRight, t2') = noOne t2 fv = free t2 sa n t = sa' n $ {- unifyBound -} t sa' 0 t = error $ "Too long sequence at [" ++ show t ++ "]"sa' n t | reduced = sa (n - 1) rest | otherwise = t where (reduced, rest) = saOne t  saOne :: Term -> (Bool, Term)saOne t@(Var v) = (False, t)saOne (Lam v t) = (reduced, Lam v rest) where (reduced, rest) = saOne tsaOne t@(App t1 t2) = if reducedRight then (True, App t1 t2') else case t1 of (Lam v t1'') -> (True, subst (deny (free t2) t1'') v t2) where (_, t1''') = saOne t1'' _ -> (reducedLeft, App t1' t2) where (reducedRight, t2') = saOne t2 (reducedLeft, t1') = saOne t1 normIO :: Int -> Term -> IO TermnormIO step t = do let (reduced, rest) = noOne t print $ "================" ++ " step " ++ show step ++ " ======== " if reduced then normIO (step + 1) rest else do print rest return rest norm :: Term -> Termnorm = no 1000 toInt :: Term -> InttoInt (Var v) = 0toInt (Lam v x) = toInt xtoInt (App v1 v2) = (toInt v1) + (toInt v2) + 1 \end{code}}  \section{Лямбда-исчисление} \emph{Лямбда-исчисление}~--- формальная система, придуманная в 1930-х годах

Более формально, \emph== Лямбда-исчисление=={{лямбдаОпределение|definition='''Лямбда-функцию} выражением''' (или, англ. <tex>\emph{лямбдаlambda</tex>''-терм}term'') можно задать называется выражение, удовлетворяющее следующей грамматикойграмматике:<br> $$<tex>\begin{array}{r c l}Lambda \langle Term \rangle & ::= & to V\langle Variable \rangle \Lambda \ & || & to \langle Term Lambda \rangle \langle Term \rangle Lambda\\ & || & \lambda \langle Variable \rangle Lambda \to \langle Term \rangle\lambda V . \Lambda</tex> & || & ( где <tex>V</tex> {{---}} множество всех строк над фиксированным алфавитом <tex> \langle Term Sigma \rangle )setminus \{ "\lambda", "\langle Variable \rangle & ::= & \langle Char \rangle *",\"."\} </tex>.\end{array}}$$Пробел во втором правиле является терминалом грамматики. Иногда его обозначают как @, чтобы он не сливался с другими символами в выражении.

Во втором происходит \emph{''аппликация} '' (\emph{''применение}'') одной функции к другой.

В третьем~{{--- \emph{}} ''абстракция} '' по переменной. В данном случае происходит

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

|<tex>\operatorname{id }\ 2 == | \eval{id 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>

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

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

\subsection{===Свободные и связанные переменные}===\emph{''Связанными} '' переменными называются все переменные, по которым выше в

Например, в |<tex>\lambda x -> \ .\y -\ x</tex> x|, |<tex>x| </tex> и связана, а |<tex>y|~</tex>{{--- }} свободна. А в |<tex>\lambda y -> \ .\ x \ (\lambda x -> \ .\ x)|</tex>в своём первом вхождении переменная |<tex>x| </tex> свободна, а во втором~{{--- }} связана. Связанные переменные {{---}} это аргументы функции. То есть для функции они являются локальными.

Рассмотрим функции |<tex>\lambda y -\ .\ y</tex> y| и |<tex>\lambda x -\ .\ y</tex> y|. В первой из них при взгляде на |<tex>y|</tex>

|<tex>\lambda x -> \.\ \lambda x -> \.\ \lambda y -> \ .\ \lambda x\ .\x -</tex> x|, переменная |<tex>x| </tex> связана с самой правой абстракцией по |<tex>x|</tex>.

\subsection{$\alpha$===α-конверсия}эквивалентность===

Рассмотрим функции {{Определение|definition='''<tex>\alpha</tex>-эквивалентностью''' (англ. ''<tex>\x alpha</tex> -equivalence'') {{---}} называется наименьшее соотношение эквивалентности на <tex>\Lambda</tex> такое что::<tex>P=_\alpha P</tex> для любого <tex>P</tex>:<tex> \lambda x) z| и |(.P=_\alpha \lambda y.P[x:=y -]</tex> если <tex> y\not\in FV(P) z|</tex>и замкнуто относительно следующих правил::<tex> P=_\alpha P' \Rightarrow \forall x \in V: \lambda x.P=_\alpha \lambda x. Интуитивно понятно, что они P'\\P=_\alpha P' \Rightarrow \forall Z \in \Lambda : P Z =_\alpha P'Z\\P=_\alpha P' \Rightarrow \forall Z \in \Lambda : Z P =_\alpha Z P'\\P=_\alpha P' \Rightarrow P'=_\alpha P\\P=_\alpha P' \ \& \ P'=_\alpha P'' \Rightarrow P=_\alpha P''\\</tex>являются одинаковыми. }}

Функции <tex>\lambda x\ .\ \lambda y\ .\ x\ y\ z</tex> и <tex>\lambda a\ .\emph{$\alpha$-конверсия}~--- переименование связанной переменнойlambda x\ . Выражение|\ a\x -\ z</tex> являются <tex> f| можно заменить на |\y alpha</tex>-эквивалентными,а <tex> f[\lambda x := \ .\ \lambda y]|, если |\ .\ y| не входит свободно в |f|,где $f[x:=\ z</tex> и <tex>\lambda y]$ означает замену всех свободных вхождений $\ .\ \lambda x$ в $f$ на $\ .\ y$\ z</tex> {{---}} нет.

Функции, получающиеся одна из другой с помощью $\alpha$===β-конверсий, называются \emph{$\alpha$-эквивалентными} и обозначаются $f \equiv_\alpha g$.редукция===

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

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

Через $f \to_\beta g$ обозначают сведение $f$ к $g$ с помощью одной $В <tex>\beta$</tex>-редукциивполне возможна функция вида <tex>\lambda x.А через $f \to_\beta^* g$~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>.

\subsection{===Пара}===

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

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

<tex>\subsectionoperatorname{Вычитаниеsnd}В отличие от всех предыдущих функций, вычитание для натуральных чисел определенотолько в случае, если уменьшаемое больше вычитаемого. Положим в противном случаерезультат равным нулю. Пусть уже есть функция, которая вычитает из числа единицу.Тогда на её основе легко сделать, собственно, вычитание= \lambda p\ .\ p\ \operatorname{false}</tex>

Функция <tex>\beginoperatorname{codepair}minus' = Lam "n" $ Lam "m" $ Var "m" `App` pred' `App` Var "n"</tex> принимает два значения и запаковывает их в пару так, чтобы к ним можно было обращаться по <tex>\endoperatorname{codefst}</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>, соответственно.

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

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

\begin{code}pred' = Lam "Это то же самое, что <tex>m</tex> раз вычесть единицу из <tex>n" $ Lam "s" $ Lam "z" $ snd'' `App` (Var "n" `App` ( Lam "p" $ pair' `App` (Var "s" `App` (fst'' `App` Var "p")) `App` (fst'' `App` Var "p") ) `App` ( pair' `App` Var "z" `App` Var "z" ) )\end{code}</tex>.

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

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

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

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

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

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

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

Рассмотрим такую функцию<tex>\operatorname{fact} = \lambda x\ . \ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))</tex>

Мы столкнулись с проблемой. В определении функции <tex>\beginoperatorname{codefact}fix' = Lam "f" $ (Lam "x" $ Var "f" `App` (Var "x" `App` Var "x")) `App` (Lam "x" $ Var "f" `App` (Var "x" `App` Var "x"))</tex> используется функция <tex>\endoperatorname{codefact}</tex>. При формальной замене, получим бесконечную функцию. Можно попытаться решить эту проблему следующим образом

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

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

Это даст функцию, которая посчитает факториал числа. Но делать она это будет мееедленно-меееедленно. Для того, чтобы посчитать <tex>5!</tex> потребовалось сделать 66066 <tex>\begin{code}fact' = fix' `App` fact''\end{code}beta</tex>-редукций.

Это даст функциюНаиболее известным комбинатором неподвижной точки является <tex>Y</tex>-комбинатор, которая посчитает факториал числавведенный известным американским ученым Хаскеллом Карри как:<tex>Y\ = \ \lambda f. Но делать она это будет мееедленно-меееедленно(\lambda x. Для того, чтобы посчитать $5!$ потребовалось сделать66066 $f(x\ x))\ (\beta$-редукцийlambda x.f(x\ x))</tex>

<tex>\subsectionoperatorname{Делениеdiv'}Воспользовавшись идеей о том, что можно делать рекурсивные функции, сделаем функцию, которая будет искать частное двух чисел= \lambda div\ .\ \lambda n\ .\ \lambda m\ .\ \operatorname{if}\ (\operatorname{less}\ n\ m)\ \bar 0\ (\operatorname{succ}\ (div\ (\operatorname{minus}\ n\ m)\ m))</tex>

<tex>\beginoperatorname{codediv}div'' = Lam "div" $ Lam "n" $ Lam "m" $ if'' `App` (less' `App` Var "n" `App` Var "m") `App` zero' `App` (succ' `App` (Var "div" `App` (minus' `App` Var "n" `App` Var "m") `App` Var "m"))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Теория вычислимости]]