403
правки
Изменения
Новая страница: «{{В разработке}} \documentclass[11pt,a4paper,oneside]{article} \usepackage[english,russian]{babel} \usepackage[T2A]{fontenc} \usepackage[utf8]{inpute...»
{{В разработке}}
\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}
[http://rain.ifmo.ru/~komarov/Turing.lhs]
\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}
[http://rain.ifmo.ru/~komarov/Turing.lhs]
