Изменения

<tex>\operatorname{if} = \lambda p \to \lambda t \to \lambda e \to p \ t \ e</tex>

<tex>\operatorname{and} = \lambda n \to \lambda m \to \operatorname{if} n \ m \ \operatorname{false}</tex>

<tex>\operatorname{or} = \lambda n \to \lambda m \to \operatorname{if} n \ \operatorname{true} m</tex>

<tex>\opeartornameoperatorname{not} = \lambda b \to \opeartornameoperatorname{if} b \ \operatorname{false} \operatorname{true}</tex>

<tex>\operatorname{isZero} = \lambda n \to n \ (\lambda c \to \operatorname{false}) \ \operatorname{true}</tex>

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

<tex>\beginoperatorname{codepair}pair' = Lam "\lambda a" $ Lam "\to \lambda b" $ Lam "\to \lambda t" $ Var "\to 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$. В $fst$ и $snd$ вместо $t$ в $pair$будет подставлено $} = \lambda p \to p\ \operatorname{true$ или $false$, возвращающие, соответственно, первый ивторой аргументы, то есть $a$ или $b$, соответственно.}</tex>

<tex>\subsectionoperatorname{Вычитаниеsnd}В отличие от всех предыдущих функций, вычитание для натуральных чисел определенотолько в случае, если уменьшаемое больше вычитаемого. Положим в противном случаерезультат равным нулю. Пусть уже есть функция, которая вычитает из числа единицу.Тогда на её основе легко сделать, собственно, вычитание.= \lambda p \to 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) (\u->u)% --pred = to \n -> lambda m \s -> to m\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 \to \lambda s \to \lambda z \to\ \operatorname{snd} (Так как вычитание определено таким способом, чтобы для случая, в котором n\ (уменьшаемое больше, чем вычитаемое, возвращать ноль, можно определить \lambda p \to \operatorname{pair}\ (s\ (\operatorname{fst} p))\ (\operatorname{fst} p)сравнение на больше-меньше через него. Равными же числа $a$ и $b$ считаются, если $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 \to \lambda m \to \operatorname{isZero x) one }\ (fact (pred x))\endoperatorname{specminus}\ n\ m)</tex>

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

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

Мы столкнулись с проблемой. В определении функции <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 \to \lambda x \to \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 \to (\lambda x \to f\ (x\ x))\ (\lambda x \to 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 "\to \lambda x" $ \to \operatorname{if'' `App` }\ (\operatorname{isZero' `App` Var "}\ x") `App` one' `App` \ \bar 1\ (\operatorname{mult' `App` Var "}\ x" `App` \ (Var "f" `App` \ (\operatorname{pred' `App` Var "}\ x")))\end{code}</tex>

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

<tex>\beginoperatorname{codefact}fact' = \operatorname{fix' `App` }\ \operatorname{fact''\end{code}</tex>

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

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

<tex>\beginoperatorname{code}div'' } = Lam "\lambda div" $ Lam "\to \lambda n" $ Lam "\to \lambda m" $ \to \operatorname{if'' `App` }\ (\operatorname{less' `App` Var "}\ n" `App` Var "\ m") `App` zero' `App` \ \bar 0\ (\operatorname{succ' `App` }\ (Var "div" `App` \ (\operatorname{minus' `App` Var "}\ n" `App` Var "\ m") `App` Var "\ m"))</tex> <tex>\operatorname{div' } = \operatorname{fix' `App` }\ \operatorname{div''\end{code}</tex>

<tex>\beginoperatorname{code}mod'' } = Lam "\lambda mod" $ Lam "\to \lambda n" $ Lam "\to \lambda m" $ \to \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> {{---}} принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от 2 до <tex>p-1</tex>. Если на что-нибудь разделилось, то число {{---}} составное, иначе {{---}} простое. <tex>\operatorname{isPrimeHelp' `App` } =</tex><tex>\lambda f \to \lambda p \to \lambda i \to \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 \to \operatorname{isPrimeHelp}\ p\ \bar 2</tex> Следующее простое число. <tex>\operatorname{nextPrime';}</tex> {{---}} следующее, больше либо равное заданного, <tex>\endoperatorname{codenextPrime}</tex> {{---}}следующее, большее заданного.

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

<tex>\beginoperatorname{codenextPrime}isPrimeHelp' = Lam "f" $ Lam "\lambda p" $ Lam "i" $ if\to \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 "\to \lambda p" $ \to \lambda i \to \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"\endto \operatorname{codeithPrimeStep}\ \bar 2\ i</tex>

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