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

Эта статья находится в разработке!

\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.Exception import Control.Monad.State import qualified Data.Map as M import Data.Maybe (fromMaybe)

type Variable = String data 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 $ t free (App t t') = (free t) ++ (free t')

subst :: Term -> Variable -> Term -> Term subst t@(Var v) var what = if v == var then what else t subst 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 -> Term deny d (Var v) = Var v -- Var $ newname d v deny d (Lam v t) = Lam v' $ subst t v (Var v') where v' = newname (d ++ free t) v deny 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]) Term unifyBound' (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' t2'

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 -> Bool eq (Var v) (Var v') = v == v' eq (Lam v1 e1) (Lam v2 e2) = v1 == v2 && e1 `eq` e2 eq (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] Variable unused = 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 t

saOne 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 Term normIO 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 -> Term norm = no 1000

toInt :: Term -> Int toInt (Var v) = 0 toInt (Lam v x) = toInt x toInt (App v1 v2) = (toInt v1) + (toInt v2) + 1

\end{code} }

\section{Лямбда-исчисление}

\emph{Лямбда-исчисление}~--- формальная система, придуманная в 1930-х годах Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией. Эта концепция показала себя удобной и сейчас активно используется во многих языках программирования.

Более формально, \emph{лямбда-функцию} (или, \emph{лямбда-терм}) можно задать следующей грамматикой:

$$ \begin{array}{r c l} \langle Term \rangle & ::= & \langle Variable \rangle \\

                      & || & \langle Term \rangle \langle Term \rangle \\
                      & || & \lambda \langle Variable \rangle \to \langle Term \rangle\\
                      & || & ( \langle Term \rangle )\\

\langle Variable \rangle & ::= & \langle Char \rangle *\\ \end{array} $$

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

Рассмотрим, например, функцию |id = \x -> x|. Эта функция принимает аргумент и возвращает его неизменённым. Например, |id 2 == | \eval{id 2}. Аналогично, |id y == y|.

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

\subsection{Приоритет операций} \begin{itemize} \item Применение левоассоциативно: |x y z w == ((x y) z) w| \item Аппликация забирает себе всё, до чего дотянется:\\

   |\x -> \y -> \z -> z y x == \x -> (\y -> (\z -> ((z y) x)))|

\item Скобки играют привычную роль группировки действий \end{itemize}

\subsection{Свободные и связанные переменные} \emph{Связанными} переменными называются все переменные, по которым выше в дереве разбора были абстракции. Все остальные переменные называются свободными.

Например, в |\x -> \y -> x|, |x| связана, а |y|~--- свободна. А в |\y -> x (\x -> x)| в своём первом вхождении переменная |x| свободна, а во втором~--- связана.

Рассмотрим функции |\y -> y| и |\x -> y|. В первой из них при взгляде на |y| понятно, что она имеет отношение к переменной, по которой производилась абстракция. Если по одной и той же переменной абстракция производилась более одного раза, то переменная связана с самым поздним (самым нижним в дереве разбора) абстрагированием. Например, в |\x -> \x -> \y -> \x -> x|, переменная |x| связана с самой правой абстракцией по |x|.

\subsection{$\alpha$-конверсия}

Рассмотрим функции |(\x -> x) z| и |(\y -> y) z|. Интуитивно понятно, что они являются одинаковыми.

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

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

Функции |\x -> \y -> x y z| и |\a -> \x -> a x z| являются $\alpha$-эквивалентными, а |\x -> \y -> y z| и |\y -> \x -> y z|~--- нет.

\subsection{$\beta$-редукция} $\beta$-редукция олицетворяет идею счёта значения функции. Выражение вида |(\x -> f) y| можно заменить на $f[x := y]$, где $f[x:=y]$, как и ранее, означает замену всех свободных вхождений $x$ в $f$ на $y$.

Через $f \to_\beta g$ обозначают сведение $f$ к $g$ с помощью одной $\beta$-редукции. А через $f \to_\beta^* g$~--- за ноль или более.

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

$\eta$-редукция~--- преобразование |\x -> f x| в $f$.

\section{Нотация Де Брюина} Существует также альтернативное эквивалентное определение $\lambda$-исчисления. В оригинальном определении для обозначения переменных использовались имена, и была проблема с тем, что не были запрещены одинаковые имена в разных абстракциях.

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

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

При $\beta$-редукции же нужно будет ко всем свободным переменным заменяющего дерева при каждой замене прибавить число, равное разницы уровней раньше и сейчас. Это будет соответствовать тому, что эта переменная продолжит <<держаться>> за ту же лямбду, что и раньше.

\section{Нумералы Чёрча}

\subsection{Определение} Введём на основе лямбда-исчисления аналог натуральных чисел, основанный на идее, что натуральное число~--- это или ноль, или увеличенное на единицу натуральное число.

\begin{code} zero' = Lam "s" $ Lam "z" $ Var "z" one' = Lam "s" $ Lam "z" $ Var "s" `App` Var "z" two' = Lam "s" $ Lam "z" $ Var "s" `App` (Var "s" `App` Var "z") three' = Lam "s" $ Lam "z" $ Var "s" `App` (Var "s" `App` (Var "s" `App` Var "z")) \end{code}

Каждое число будет функцией двух аргументов: какой-то функции и начального значения. Число $n$ будет $n$ раз применять функцию к начальному значению и возвращать результат. Если такому <<числу>> дать на вход функцию $(+1)$ и $0$ в качестве начального значения, то на выходе как раз будет ожидаемое от функции число: |three (+1) 0 == | \eval{three (+1) 0}.

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

\begin{code} succ' = Lam "n" $ Lam "s" $ Lam "z" $ Var "s" `App` (Var "n" `App` Var "s" `App` Var "z") \end{code}

Здесь $n s z$~--- $n$ раз применённая к $z$ функция $s$. Но нужно применить $n+1$ раз. Отсюда $s (n s z)$.

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

\begin{code} plus' = Lam "n" $ Lam "m" $ Lam "s" $ Lam "z" $ Var "n" `App` Var "s" `App` (Var "m" `App` Var "s" `App` Var "z") \end{code}

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

|(plus three three) (+1) 0 == | \eval{(plus three three) (+1) 0}

\subsection{Умножение} Умножение похоже на сложение, но прибавлять надо не единицу, а второе число. Или, в терминах нумералов Чёрча, в качестве применяемой несколько раз функции должна быть не $s$, а функция, применяющая $n$ раз $s$.

\begin{code} mult' = Lam "n" $ Lam "m" $ Lam "s" $ Var "n" `App` (Var "m" `App` Var "s") \end{code}

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

\begin{spec} mult = \n -> \m -> \s -> n (m s) \end{spec}

|(mult three three) (+1) 0 == | \eval{(mult three three) (+1) 0}

\subsection{Возведение в степень} It's a kind of magic

\begin{code} power' = Lam "n" $ Lam "m" $ Var "m" `App` Var "n" \end{code}

|(power three (succ three)) (+1) 0 == | \eval{(power three (succ three)) (+1) 0}

\subsection{Логические значения} \begin{code} true' = Lam "a" $ Lam "b" $ Var "a" false' = Lam "a" $ Lam "b" $ Var "b" \end{code}

Функции двух аргументов, возвращающие первый и второй, соответственное, аргументы. Забавный факт: $false \equiv_\alpha zero$. Эти функции сделаны такими для того, чтобы красиво написать функцию $if$:

\begin{code} if = Lam "p" $ Lam "t" $ Lam "e" $ Var "p" `App` Var "t" `App` Var "e" \end{code}

Если ей в качестве первого аргумента дадут $true$, то вернётся $t$, иначе~--- $e$.

Стандартные функции булевой логики:

\begin{code} and' = Lam "n" $ Lam "m" $ if `App` Var "n" `App` Var "m" `App` false' or' = Lam "n" $ Lam "m" $ if `App` Var "n" `App` true' `App` Var "m" not' = Lam "b" $ if `App` Var "b" `App` false' `App` true' \end{code}

Ещё одной важной функцией является функция проверки, является ли число нулём:

\begin{code} isZero' = Lam "n" $ Var "n" `App` (Lam "c" false') `App` true' \end{code}

Функция выглядит несколько странно. |\c -> false|~--- функция, которая независимо от того, что ей дали на вход, возвращает $false$. Тогда, если в качестве $n$ будет дан ноль, то функция, по определению нуля, не выполнится ни разу, и будет возвращено значение по умолчанию $true$. Иначе же функция будет запущено, и вернётся $false$.

\subsection{Пара}

\begin{code} pair' = Lam "a" $ Lam "b" $ Lam "t" $ Var "t" `App` Var "a" `App` Var "b" fst = Lam "p" $ Var "p" `App` true' snd = Lam "p" $ Var "p" `App` false' \end{code}

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

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

\begin{code} minus' = Lam "n" $ Lam "m" $ Var "m" `App` pred' `App` Var "n" \end{code}

<<$m$ раз вычесть единицу из $n$>>.

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

\begin{code} pred' = Lam "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}

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

\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' = Lam "n" $ Lam "m" $ and'

           `App` (isZero' `App` (minus' `App` Var "n" `App` Var "m"))
           `App` (isZero' `App` (minus' `App` Var "m" `App` Var "n"))

\end{code}

\subsection{Комбинатор неподвижной точки} Попробуем выразить в лямбда-исчислении какую-нибудь рекурсивную функцию. Напрмер, факториал.

\begin{spec} fact = \x -> if (isZero x) one (fact (pred x)) \end{spec}

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

\begin{spec} fact = (\f -> \x -> if (isZero x) one (f (pred x))) fact \end{spec}

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

Рассмотрим такую функцию.

\begin{code} fix' = Lam "f" $ (Lam "x" $ Var "f" `App` (Var "x" `App` Var "x"))

           `App`  (Lam "x" $ Var "f" `App` (Var "x" `App` Var "x"))

\end{code}

Заметим, что $fix' \to_\beta \lambda f \to f ((\lambda x \to f (x x)) (\lambda x \to f (x x)))$. Или, что то же самое, $\lambda f \to (\lambda x \to f (x x)) (\lambda x \to f (x x)) \to_\beta

\lambda f \to f ((\lambda x \to f (x x)) (\lambda x \to f (x x)))$

Рассмотрим функцию

\begin{code} fact = Lam "f" $ Lam "x" $ if `App` (isZero' `App` Var "x")

                                 `App` one'
                                 `App` (mult' `App` Var "x" `App` (Var "f" `App`
                                           (pred' `App` Var "x")))

\end{code}

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

\begin{code} fact' = fix' `App` fact \end{code}

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

Тут правда ничего не понятно? :'(

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

\begin{code} 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' = fix' `App` div \end{code}

И остатка от деления

\begin{code} mod = Lam "mod" $ Lam "n" $ Lam "m" $ if `App` (less' `App` Var "n" `App` Var "m")

        `App` Var "n"
        `App` (Var "mod" `App` (minus' `App` Var "n" `App` Var "m") `App` Var "m")

mod' = fix' `App` mod; \end{code}

\subsection{Проверка на простоту}

$isPrimeHelp$~--- принимает число, которое требуется проверить на простоту и то, на что его надо попытаться поделить, перебирая это от 2 до $p-1$. Если на что-нибудь разделилось, то число~--- составное, иначе~--- простое.

\begin{code} isPrimeHelp' = Lam "f" $ Lam "p" $ Lam "i" $ if `App` (le' `App` Var "p" `App` Var "i")

               `App` true'
               `App` ( if `App` (isZero' `App` (mod' `App` Var "p" `App` Var "i"))
                        `App` false'
                        `App` (Var "f" `App` Var "p" `App` (succ' `App` Var "i"))
               )

isPrimeHelp = fix' `App` isPrimeHelp' isPrime = Lam "p" $ isPrimeHelp `App` Var "p" `App` two' \end{code}

Следующее простое число. $nextPrime'$~--- следующее, больше либо равное заданного, $nextPrime$~--- следующее, большее заданного.

\begin{code} nextPrime = Lam "f" $ Lam "p" $ if `App` (isPrime `App` Var "p")

                                  `App` Var "p"
                                  `App` (Var "f" `App` (succ' `App` Var "p")) 

nextPrime' = fix' `App` nextPrime nextPrime = Lam "p" $ nextPrime' `App` (succ' `App` Var "p") \end{code}

$ithPrimeStep$ пропрыгает $i$ простых чисел вперёд. $ithPrime$ принимает число $i$ и пропрыгивает столько простых чисел вперёд, начиная с двойки.

\begin{code} ithPrimeStep' = Lam "f" $ Lam "p" $ Lam "i" $ if `App` (isZero' `App` Var "i")

               `App` Var "p"
               `App` (Var "f" `App` (nextPrime `App` Var "p") `App` (pred' `App` Var "i"))

ithPrimeStep = fix' `App` ithPrimeStep' ithPrime = Lam "i" $ ithPrimeStep `App` two' `App` Var "i" \end{code}

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

\subsection{Списки}

Для работы со списками чисел нам понадобятся следующие функции: \begin{itemize}

   \item $empty$~--- возвращает пустой список
   \item $cons$~--- принимает первый элемент и оставшийся список, склеивает их
   \item $head$~--- вернуть голову списка
   \item $tail$~--- вернуть хвост списка

\end{itemize}

Список будем хранить в следующем виде: $\langle len, p_1^{a_1}p_2^{a_2}\ldots p_{len}^{a_{len}} \rangle$. При этом, голова списка будет храниться как показатель степени при $p_{len}$.

\begin{code} empty = pair' `App` zero' `App` one' cons = Lam "h" $ Lam "t" $ pair' `App` (succ' `App` (fst `App` Var "t"))

       `App` (mult' `App` (snd `App` Var "t") `App` (power' 
               `App` (ithPrime `App` (fst `App` Var "t"))
               `App` Var "h"
       ))

head = Lam "list" $ getExponent `App` (snd `App` Var "list")

                               `App` (ithPrime `App` (pred' `App` (fst `App` Var "list")))

tail = Lam "list" $ pair' `App` (pred' `App` (fst `App` Var "list"))

                         `App` (eliminateMultiplier `App` (snd `App` Var "list")
                                 `App` (ithPrime `App` (pred' `App` (fst `App` Var "list" )))
                               )

eliminateMultiplier' = Lam "f" $ Lam "n" $ Lam "m" $ if `App` (isZero' `App` (mod' `App` Var "n" `App` Var "m"))

                       `App` (Var "f" `App` (div' `App` Var "n" `App` Var "m") `App` Var "m")
                       `App` Var "n"

eliminateMultiplier = fix' `App` eliminateMultiplier'

getExponent' = Lam "f" $ Lam "n" $ Lam "m" $ if `App` (isZero' `App` (mod' `App` Var "n" `App` Var "m"))

               `App` (succ' `App`(Var "f" `App` (div' `App` Var "n" `App` Var "m") `App` Var "m"))
               `App` zero'

getExponent = fix' `App` getExponent' \end{code}

На основе этого всего уже можно реализовать эмулятор машины тьюринга: с помощью пар, списков чисел можно хранить состояния. С помощью рекурсии можно обрабатывать переходы. Входная строка будет даваться, например, закодированной аналогично списку: пара из длины и числа, характеризующего список степенями простых. Я бы продолжил это писать, но уже на операции $head [1, 2]$ я не дождался окончания выполнения. Скорость лямбда-исчисления как вычислителя печальна.

\ignore{ \begin{code}

four' = norm $ succ' `App` three' five' = norm $ succ' `App` four'

list2 = norm $ cons `App` one' `App` empty list32 = cons `App` zero' `App` list2

normFiveFact = normIO 0 $ fact' `App` five'

-- fiftysix = mult twentyeight two -- fiftyfive = pred fiftysix -- six = pred seven

--main = do print $ fiftysix (+1) 0 main = do

--   f <- normIO 0 $ ithPrime `App` three'
--   f <- normIO 0 $ getExponent `App` (norm $ plus' `App` four' `App` four') `App` two'
   f <- normIO 0 $ head `App` (tail `App` list32)
   print $ toInt f

\end{code} }

\end{document} [1]