Лямбда-исчисление — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Логические значения)
(Логические значения)
Строка 187: Строка 187:
 
чтобы красиво написать функцию <tex>\operatorname{if}</tex>:
 
чтобы красиво написать функцию <tex>\operatorname{if}</tex>:
  
<tex>\operatorname{if} = \lambda p \to \lambda t \to \lambda e \to p t e</tex>
+
<tex>\operatorname{if} = \lambda p \to \lambda t \to \lambda e \to p\ t\ e</tex>
  
 
Если ей в качестве первого аргумента дадут <tex>\operatorname{true}</tex>, то вернётся <tex>t</tex>, иначе {{---}} <tex>e</tex>.
 
Если ей в качестве первого аргумента дадут <tex>\operatorname{true}</tex>, то вернётся <tex>t</tex>, иначе {{---}} <tex>e</tex>.
Строка 193: Строка 193:
 
Стандартные функции булевой логики:
 
Стандартные функции булевой логики:
  
<tex>\operatorname{and} = \lambda n \to \lambda m \to \operatorname{if} n m \operatorname{false}</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>\operatorname{or} = \lambda n \to \lambda m \to \operatorname{if} n\ \operatorname{true} m</tex>
  
<tex>\opeartorname{not} = \lambda b \to \opeartorname{if} b \operatorname{false} \operatorname{true}</tex>
+
<tex>\operatorname{not} = \lambda b \to \operatorname{if} b\ \operatorname{false} \operatorname{true}</tex>
  
 
Ещё одной важной функцией является функция проверки, является ли число нулём:
 
Ещё одной важной функцией является функция проверки, является ли число нулём:
  
<tex>\operatorname{isZero} = \lambda n \to n (\lambda c \to \operatorname{false}) \operatorname{true}</tex>
+
<tex>\operatorname{isZero} = \lambda n \to n\ (\lambda c \to \operatorname{false})\ \operatorname{true}</tex>
  
 
Функция выглядит несколько странно. <tex>\lambda c -> \operatorname{false}</tex> {{---}} функция, которая независимо
 
Функция выглядит несколько странно. <tex>\lambda c -> \operatorname{false}</tex> {{---}} функция, которая независимо
Строка 209: Строка 209:
 
вернётся <tex>\operatorname{false}</tex>.
 
вернётся <tex>\operatorname{false}</tex>.
  
\subsection{Пара}
+
===Пара===
  
\begin{code}
+
<tex>\operatorname{pair} = \lambda a \to \lambda b \to \lambda t \to t\ a\ b</tex>
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$ принимает два значения и запаковывает их в пару так, чтобы к
+
<tex>\operatorname{fst} = \lambda p \to p\ \operatorname{true}</tex>
ним можно было обращаться по $fst$ и $snd$. В $fst$ и $snd$ вместо $t$ в $pair$
 
будет подставлено $true$ или $false$, возвращающие, соответственно, первый и
 
второй аргументы, то есть $a$ или $b$, соответственно.
 
  
\subsection{Вычитание}
+
<tex>\operatorname{snd} = \lambda p \to p\ \operatorname{false}</tex>
В отличие от всех предыдущих функций, вычитание для натуральных чисел определено
 
только в случае, если уменьшаемое больше вычитаемого. Положим в противном случае
 
результат равным нулю. Пусть уже есть функция, которая вычитает из числа единицу.
 
Тогда на её основе легко сделать, собственно, вычитание.
 
  
\begin{code}
+
Функция <tex>\operatorname{pair}</tex> принимает два значения и запаковывает их в пару так, чтобы к ним можно было обращаться по <tex>\operatorname{fst}</tex> и <tex>\operatorname{snd}</tex>. В <tex>\operatorname{fst}</tex> и <tex>\operatorname{snd}</tex> вместо <tex>t</tex> в <tex>\operatorname{pair}</tex> будет подставлено <tex>\operatorname{true}</tex> или <tex>\operatorname{false}</tex>, возвращающие, соответственно, первый и второй аргументы, то есть <tex>a</tex> или <tex>b</tex>, соответственно.
minus' = Lam "n" $ Lam "m" $ Var "m" `App` pred' `App` Var "n"
 
\end{code}
 
  
<<$m$ раз вычесть единицу из $n$>>.
+
===Вычитание===
 +
В отличие от всех предыдущих функций, вычитание для натуральных чисел определено только в случае, если уменьшаемое больше вычитаемого. Положим в противном случае результат равным нулю. Пусть уже есть функция, которая вычитает из числа единицу. Тогда на её основе легко сделать, собственно, вычитание.
  
Осталось, собственно, функция для вычитания единицы. Однако, это не так просто,
+
<tex>\operatorname{minus} = \lambda n \to \lambda m \to m\ \operatorname{pred} n</tex>
как может показаться на первый взгляд. Проблема в том, что, имея функцию, которую
 
нужно применить для того, чтобы продвинуться вперёд, продвинуться назад будет
 
проблематично. Если попробовать воспользоваться идеей о том, чтобы, начав от
 
нуля, идти вперёд, и пройти на один шаг меньше, то будет не очень понятно, как
 
же остановиться ровно за один шаг до конца. Для реализации вычитания единицы
 
сделаем следующее. $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}
+
Это то же самое, что <tex>m</tex> раз вычесть единицу из <tex>n</tex>.
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}
 
  
Если вы ничего не поняли, не огорчайтесь. Вычитание придумал Клини, когда
+
Осталось, собственно, функция для вычитания единицы. Однако, это не так просто, как может показаться на первый взгляд. Проблема в том, что, имея функцию, которую нужно применить для того, чтобы продвинуться вперёд, продвинуться назад будет проблематично. Если попробовать воспользоваться идеей о том, чтобы, начав от нуля, идти вперёд, и пройти на один шаг меньше, то будет не очень понятно, как же остановиться ровно за один шаг до конца. Для реализации вычитания единицы сделаем следующее. <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>, которое и хочется получить.  
ему вырывали зуб мудрости. А сейчас наркоз уже не тот!
 
  
\subsection{Сравнение}
+
<tex>\operatorname{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$ считаются,
+
    )\ (\operatorname{pair}\ z\ z)</tex>
если $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{Комбинатор неподвижной точки}
+
===Сравнение===
Попробуем выразить в лямбда-исчислении какую-нибудь рекурсивную функцию.
+
Так как вычитание определено таким способом, чтобы для случая, в котором уменьшаемое больше, чем вычитаемое, возвращать ноль, можно определить сравнение на больше-меньше через него. Равными же числа <tex>a</tex> и <tex>b</tex> считаются, если <tex>a - b = 0 \wedge b - a = 0</tex>.
Напрмер, факториал.
 
  
\begin{spec}
+
<tex>\operatorname{le} = \lambda n \to \lambda m \to \operatorname{isZero}\ (\operatorname{minus}\ n\ m)</tex>
fact = \x -> if (isZero x) one (fact (pred x))
 
\end{spec}
 
  
Мы столкнулись с проблемой. В определении функции $fact$ используется функция
+
<tex>\operatorname{less} = \lambda n \to \lambda m \to \operatorname{le}\ n\ (\operatorname{pred} m)</tex>
$fact$. При формальной замене, получим бесконечную функцию. Можно попытаться решить
 
эту проблему следующим образом
 
  
\begin{spec}
+
<tex>\operatorname{eq} = \lambda n \to \lambda m \to \operatorname{and}\ (\operatorname{isZero}\ (\operatorname{minus}\ n\ m))\
fact = (\f -> \x -> if (isZero x) one (f (pred x))) fact
+
(\operatorname{isZero}\ (\operatorname{minus}\ m\ n))</tex>
\end{spec}
 
  
\emph{Неподвижной точкой} лямбда-функции $f$ назовём такую функцию $x$, что
+
===Комбинатор неподвижной точки===
$f x \to_\beta x$. Лямбда исчисление обладаем замечательным свойством: у каждой
+
Попробуем выразить в лямбда-исчислении какую-нибудь функцию, использующую рекурсию. Напрмер, факториал.
функции есть неподвижная точка!
 
  
Рассмотрим такую функцию.
+
<tex>\operatorname{fact} = \lambda x \to \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))</tex>
  
\begin{code}
+
Мы столкнулись с проблемой. В определении функции <tex>\operatorname{fact}</tex> используется функция <tex>\operatorname{fact}</tex>. При формальной замене, получим бесконечную функцию. Можно попытаться решить эту проблему следующим образом
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)))$.
+
<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>.
 
Или, что то же самое,  
 
Или, что то же самое,  
$\lambda f \to (\lambda x \to f (x x)) (\lambda x \to f (x x)) \to_\beta
+
<tex>\lambda f \to (\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)) \to_\beta</tex>
\lambda f \to f ((\lambda x \to f (x x)) (\lambda x \to f (x x)))$
+
<tex>\lambda f \to f\ ((\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)))</tex>
  
 
Рассмотрим функцию
 
Рассмотрим функцию
  
\begin{code}
+
<tex>\operatorname{fact'} = \lambda f \to \lambda x \to \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{mult}\ x\ (f\ (\operatorname{pred}\ x)))</tex>
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)$, то есть,  
+
Как было показано выше, <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> {{---}} искомая функция, считающая факториал.
$fix fact'' \to_\beta fact'$, где $fact'$~--- искомая функция, считающая факториал.
 
  
\begin{code}
+
<tex>\operatorname{fact} = \operatorname{fix}\ \operatorname{fact'}</tex>
fact' = fix' `App` fact''
 
\end{code}
 
  
Это даст функцию, которая посчитает факториал числа. Но делать она это будет  
+
Это даст функцию, которая посчитает факториал числа. Но делать она это будет мееедленно-меееедленно. Для того, чтобы посчитать <tex?5!</tex> потребовалось сделать 66066 <tex>\beta</tex>-редукций.
мееедленно-меееедленно. Для того, чтобы посчитать $5!$ потребовалось сделать
 
66066 $\beta$-редукций.
 
  
 
Тут правда ничего не понятно? :'(
 
Тут правда ничего не понятно? :'(
  
\subsection{Деление}
+
===Деление===
Воспользовавшись идеей о том, что можно делать рекурсивные функции, сделаем  
+
Воспользовавшись идеей о том, что можно делать рекурсивные функции, сделаем функцию, которая будет искать частное двух чисел.
функцию, которая будет искать частное двух чисел.
 
  
\begin{code}
+
<tex>\operatorname{div'} = \lambda div \to \lambda n \to \lambda m \to \operatorname{if}\ (\operatorname{less}\ n\ m)\ \bar 0\ (\operatorname{succ}\ (div\ (\operatorname{minus}\ n\ m)\ m))</tex>
div'' = Lam "div" $ Lam "n" $ Lam "m" $ if'' `App` (less' `App` Var "n" `App` Var "m")
+
 
        `App` zero'
+
<tex>\operatorname{div} = \operatorname{fix}\ \operatorname{div'}</tex>
        `App` (succ' `App` (Var "div" `App` (minus' `App` Var "n" `App` Var "m") `App` Var "m"))
 
div' = fix' `App` div''
 
\end{code}
 
  
 
И остатка от деления
 
И остатка от деления
  
\begin{code}
+
<tex>\operatorname{mod'} = \lambda mod \to \lambda n \to \lambda m \to \operatorname{if}\ (\operatorname{less}\ n\ m)\ n\ (mod\ (\operatorname{minus}\ n\ m)\ m)</tex>
mod'' = Lam "mod" $ Lam "n" $ Lam "m" $ if'' `App` (less' `App` Var "n" `App` Var "m")
+
 
        `App` Var "n"
+
<tex>\operatorname{mod} = \operatorname{fix}\ \operatorname{mod'}</tex>
        `App` (Var "mod" `App` (minus' `App` Var "n" `App` Var "m") `App` Var "m")
+
 
mod' = fix' `App` mod'';
+
===Проверка на простоту===
\end{code}
+
 
 +
<tex>\operatorname{isPrimeHelp}</tex> {{---}} принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от 2 до <tex>p-1</tex>. Если на что-нибудь разделилось, то число {{---}} составное, иначе {{---}} простое.
 +
 
 +
<tex>\operatorname{isPrimeHelp'} =</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>\operatorname{nextPrime}</tex> {{---}} следующее, большее заданного.
  
\subsection{Проверка на простоту}
+
<tex>\operatorname{nextPrime''} = \lambda f \to \lambda p \to \operatorname{if}\ (\operatorname{isPrime}\ p)\ p\ (f\ (\operatorname{succ}\ p)) </tex>
  
$isPrimeHelp$~--- принимает число, которое требуется проверить на простоту и
+
<tex>\operatorname{nextPrime'} = \operatorname{fix}\ \operatorname{nextPrime'}</tex>
то, на что его надо попытаться поделить, перебирая это от 2 до $p-1$. Если на
 
что-нибудь разделилось, то число~--- составное, иначе~--- простое.
 
  
\begin{code}
+
<tex>\operatorname{nextPrime} = \lambda p \to \operatorname{nextPrime'}\ (\operatorname{succ}\ p)</tex>
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'$~--- следующее, больше либо равное заданного,
+
<tex>\operatorname{ithPrimeStep}</tex> пропрыгает <tex>i</tex> простых чисел вперёд. <tex>\operatorname{ithPrime}</tex> принимает число <tex>i</tex> и пропрыгивает столько простых чисел вперёд, начиная с двойки.
$nextPrime$~--- следующее, большее заданного.
 
  
\begin{code}
+
<tex>\operatorname{ithPrimeStep'} = \lambda f \to \lambda p \to \lambda i \to \operatorname{if}\ (\operatorname{isZero}\ i)\ p\ (f(\operatorname{nextPrime}\ p)\ (\operatorname{pred}\ i))</tex>
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$ принимает число
+
<tex>\operatorname{ithPrimeStep} = \operatorname{fix}\ \operatorname{ithPrimeStep'}</tex>
$i$ и пропрыгивает столько простых чисел вперёд, начиная с двойки.
 
  
\begin{code}
+
<tex>\operatorname{ithPrime} = \lambda i \to \operatorname{ithPrimeStep}\ \bar 2\ i</tex>
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$-редукций вы узнаете, что третье простое число~---
+
...и всего через 314007 <tex>\beta</tex>-редукций вы узнаете, что третье простое число {{---}} семь!
семь!
 
  
 
\subsection{Списки}
 
\subsection{Списки}

Версия 20:41, 6 декабря 2012

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

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

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

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

Определение:
[math] \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} [/math]


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

Рассмотрим, например, функцию [math]id = \lambda x \to x[/math]. Эта функция принимает аргумент и возвращает его неизменённым. Например, [math]id 2 \equiv 2[/math]. Аналогично, [math]id y == y[/math].

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

Приоритет операций

  • Применение левоассоциативно: [math]x y z w == ((x y) z) w[/math]
  • Аппликация забирает себе всё, до чего дотянется: [math]\lambda x \to \lambda y \to \lambda z \to z y x \equiv \lambda x \to (\lambda y \to (\lambda z \to ((z y) x)))[/math]
  • Скобки играют привычную роль группировки действий

Свободные и связанные переменные

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

Например, в [math]\lambda x \to \lambda y \to x[/math], [math]x[/math] связана, а [math]y[/math]— свободна. А в [math]\lambda y \to x (\lambda x \to x)[/math] в своём первом вхождении переменная [math]x[/math] свободна, а во втором — связана.

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

[math]\alpha[/math]-конверсия

Рассмотрим функции [math](\lambda x \to x) z[/math] и [math](\lambda y \to y) z[/math]. Интуитивно понятно, что они являются одинаковыми.


Определение:
[math]\alpha[/math]-конверсия — переименование связанной переменной. Выражение

[math]\lambda x \to f[/math] можно заменить на [math]\lambda y \to f[x := y][/math], если [math]y[/math] не входит свободно в [math]f[/math],

где [math]f[x:=y][/math] означает замену всех свободных вхождений [math]x[/math] в [math]f[/math] на [math]y[/math].


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

Функции [math]\lambda x \to \lambda y \to x y z[/math] и [math]\lambda a \to \lambda x \to a x z[/math] являются [math]\alpha[/math]-эквивалентными, а [math]\lambda x \to \lambda y \to y z[/math] и [math]\lambda y \to \lambda x \to y z[/math] — нет.

[math]\beta[/math]-редукция

Определение:
[math]\beta[/math]-редукция олицетворяет идею счёта значения функции. Выражение вида

[math](\lambda x \to f) y[/math] можно заменить на [math]f[x := y][/math], где [math]f[x:=y][/math], как и ранее, означает

замену всех свободных вхождений [math]x[/math] в [math]f[/math] на [math]y[/math].


Определение:
Через [math]f \to_\beta g[/math] обозначают сведение [math]f[/math] к [math]g[/math] с помощью одной [math]\beta[/math]-редукции. А через [math]f \to_\beta^* g[/math] — за ноль или более.


[math]\eta[/math]-редукция

Рассмотрим выражение вида [math]\lambda x \to f x[/math]. Если подставить в эту функцию значение [math]y[/math], то получим: [math](\lambda x \to f x) y \to_\beta f y[/math]. Но если просто подставить [math]y[/math] в [math]f[/math], то получится то же самое.


Определение:
[math]\eta[/math]-редукция — преобразование [math]\lambda x \to f x[/math] в [math]f[/math].


Нотация Де Брюина

Существует также альтернативное эквивалентное определение [math]\lambda[/math]-исчисления. В оригинальном определении для обозначения переменных использовались имена, и была проблема с тем, что не были запрещены одинаковые имена в разных абстракциях.

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

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

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

Нумералы Чёрча и программирование на [math]\lambda[/math]-исчислении

Определение

Введём на основе лямбда-исчисления аналог натуральных чисел, основанный на идее, что натуральное число — это или ноль, или увеличенное на единицу натуральное число.

  • [math]\bar 0 = \lambda s \to \lambda z \to z[/math]
  • [math]\bar 1 = \lambda s \to \lambda z \to s z[/math]
  • [math]\bar 2 = \lambda s \to \lambda z \to s (s z)[/math]
  • [math]\bar 3 = \lambda s \to \lambda z \to s (s (s z))[/math]

Каждое число будет функцией двух аргументов: какой-то функции и начального значения. Число [math]n[/math] будет [math]n[/math] раз применять функцию к начальному значению и возвращать результат. Если такому <<числу>> дать на вход функцию [math](+1)[/math] и [math]0[/math] в качестве начального значения, то на выходе как раз будет ожидаемое от функции число: [math]\bar 3 (+1) 0 \equiv 3[/math].

+1

Функция, прибавляющая 1 к числу, должна принимать первым аргументом число. Но число — функция двух аргументов. Значит, эта функция должна принимать три аргумента: <<число>> [math]n[/math], которое хочется увеличить, функция, которую надо будет [math]n+1[/math] раз применить, и начальное значение.

[math]\operatorname{succ} = \lambda n \to \lambda s \to \lambda z \to s (n s z)[/math]

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

Сложение

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

[math]\operatorname{plus} = \lambda n \to \lambda m \to \lambda s \to \lambda z \to n s (m s z)[/math]

[math]n[/math] раз применить [math]s[/math] к применённому [math]m[/math] раз [math]s[/math] к [math]z[/math]

[math](\operatorname{plus} \bar 3 \bar 3) (+1) 0 \equiv 6[/math]

Умножение

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

[math]\operatorname{mult} = \lambda n \to \lambda m \to \lambda s \to n (m s)[/math]

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

[math]\operatorname{mult} = \lambda n \to \lambda m \to \lambda s \to n (m s)[/math]

[math](\operatorname{mult} \bar 3 \bar 3) (+1) 0 \equiv 9[/math]

Возведение в степень

It's a kind of magic

[math]\operatorname{power} = \lambda n \to \lambda m \to m n[/math]

[math](\operatorname{power} \bar 3 (\operatorname{succ} \bar 3)) (+1) 0 \equiv 81[/math]

Логические значения

[math]\operatorname{true} = \lambda a \to \lambda b \to a[/math]

[math]\operatorname{false} = \lambda a \to \lambda b \to b[/math]

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

[math]\operatorname{if} = \lambda p \to \lambda t \to \lambda e \to p\ t\ e[/math]

Если ей в качестве первого аргумента дадут [math]\operatorname{true}[/math], то вернётся [math]t[/math], иначе — [math]e[/math].

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

[math]\operatorname{and} = \lambda n \to \lambda m \to \operatorname{if} n\ m\ \operatorname{false}[/math]

[math]\operatorname{or} = \lambda n \to \lambda m \to \operatorname{if} n\ \operatorname{true} m[/math]

[math]\operatorname{not} = \lambda b \to \operatorname{if} b\ \operatorname{false} \operatorname{true}[/math]

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

[math]\operatorname{isZero} = \lambda n \to n\ (\lambda c \to \operatorname{false})\ \operatorname{true}[/math]

Функция выглядит несколько странно. [math]\lambda c -\gt \operatorname{false}[/math] — функция, которая независимо от того, что ей дали на вход, возвращает [math]\operatorname{false}[/math]. Тогда, если в качестве [math]n[/math] будет дан ноль, то функция, по определению нуля, не выполнится ни разу, и будет возвращено значение по умолчанию [math]\operatorname{true}[/math]. Иначе же функция будет запущено, и вернётся [math]\operatorname{false}[/math].

Пара

[math]\operatorname{pair} = \lambda a \to \lambda b \to \lambda t \to t\ a\ b[/math]

[math]\operatorname{fst} = \lambda p \to p\ \operatorname{true}[/math]

[math]\operatorname{snd} = \lambda p \to p\ \operatorname{false}[/math]

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

Вычитание

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

[math]\operatorname{minus} = \lambda n \to \lambda m \to m\ \operatorname{pred} n[/math]

Это то же самое, что [math]m[/math] раз вычесть единицу из [math]n[/math].

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

[math]\operatorname{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) )\ (\operatorname{pair}\ z\ z)[/math]

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

Сравнение

Так как вычитание определено таким способом, чтобы для случая, в котором уменьшаемое больше, чем вычитаемое, возвращать ноль, можно определить сравнение на больше-меньше через него. Равными же числа [math]a[/math] и [math]b[/math] считаются, если [math]a - b = 0 \wedge b - a = 0[/math].

[math]\operatorname{le} = \lambda n \to \lambda m \to \operatorname{isZero}\ (\operatorname{minus}\ n\ m)[/math]

[math]\operatorname{less} = \lambda n \to \lambda m \to \operatorname{le}\ n\ (\operatorname{pred} m)[/math]

[math]\operatorname{eq} = \lambda n \to \lambda m \to \operatorname{and}\ (\operatorname{isZero}\ (\operatorname{minus}\ n\ m))\ (\operatorname{isZero}\ (\operatorname{minus}\ m\ n))[/math]

Комбинатор неподвижной точки

Попробуем выразить в лямбда-исчислении какую-нибудь функцию, использующую рекурсию. Напрмер, факториал.

[math]\operatorname{fact} = \lambda x \to \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))[/math]

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

[math]\operatorname{fact} = (\lambda f \to \lambda x \to \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (f\ (\operatorname{pred}\ x)))\ \operatorname{fact}[/math]


Определение:
Неподвижной точкой лямбда-функции [math]f[/math] назовём такую функцию [math]x[/math], что [math]f\ x \to_\beta x[/math].


Лямбда исчисление обладаем замечательным свойством: у каждой функции есть неподвижная точка!

Рассмотрим следующую функцию.

[math]\operatorname{fix} = \lambda f \to (\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x))[/math]

Заметим, что [math]\operatorname{fix} \to_\beta \lambda f \to f\ ((\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)))[/math]. Или, что то же самое, [math]\lambda f \to (\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)) \to_\beta[/math] [math]\lambda f \to f\ ((\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)))[/math]

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

[math]\operatorname{fact'} = \lambda f \to \lambda x \to \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{mult}\ x\ (f\ (\operatorname{pred}\ x)))[/math]

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

[math]\operatorname{fact} = \operatorname{fix}\ \operatorname{fact'}[/math]

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

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

Деление

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

[math]\operatorname{div'} = \lambda div \to \lambda n \to \lambda m \to \operatorname{if}\ (\operatorname{less}\ n\ m)\ \bar 0\ (\operatorname{succ}\ (div\ (\operatorname{minus}\ n\ m)\ m))[/math]

[math]\operatorname{div} = \operatorname{fix}\ \operatorname{div'}[/math]

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

[math]\operatorname{mod'} = \lambda mod \to \lambda n \to \lambda m \to \operatorname{if}\ (\operatorname{less}\ n\ m)\ n\ (mod\ (\operatorname{minus}\ n\ m)\ m)[/math]

[math]\operatorname{mod} = \operatorname{fix}\ \operatorname{mod'}[/math]

Проверка на простоту

[math]\operatorname{isPrimeHelp}[/math] — принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от 2 до [math]p-1[/math]. Если на что-нибудь разделилось, то число — составное, иначе — простое.

[math]\operatorname{isPrimeHelp'} =[/math][math]\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)))[/math]

[math]\operatorname{isPrimeHelp} = \operatorname{fix}\ \operatorname{isPrimeHelp'}[/math]

[math]\operatorname{isPrime} = \lambda p \to \operatorname{isPrimeHelp}\ p\ \bar 2[/math]

Следующее простое число. [math]\operatorname{nextPrime'}[/math] — следующее, больше либо равное заданного, [math]\operatorname{nextPrime}[/math] — следующее, большее заданного.

[math]\operatorname{nextPrime''} = \lambda f \to \lambda p \to \operatorname{if}\ (\operatorname{isPrime}\ p)\ p\ (f\ (\operatorname{succ}\ p)) [/math]

[math]\operatorname{nextPrime'} = \operatorname{fix}\ \operatorname{nextPrime'}[/math]

[math]\operatorname{nextPrime} = \lambda p \to \operatorname{nextPrime'}\ (\operatorname{succ}\ p)[/math]

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

[math]\operatorname{ithPrimeStep'} = \lambda f \to \lambda p \to \lambda i \to \operatorname{if}\ (\operatorname{isZero}\ i)\ p\ (f\ (\operatorname{nextPrime}\ p)\ (\operatorname{pred}\ i))[/math]

[math]\operatorname{ithPrimeStep} = \operatorname{fix}\ \operatorname{ithPrimeStep'}[/math]

[math]\operatorname{ithPrime} = \lambda i \to \operatorname{ithPrimeStep}\ \bar 2\ i[/math]

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

\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]