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

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

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

Лямбда-исчисление — формальная система, придуманная в 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 \tp 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\lt tex\gt {{---}} \lt tex\gt n[/math] раз применённая к [math]z[/math] функция [math]s[/math]. Но нужно применить [math]n+1[/math] раз. Отсюда [math]s (n s z)[/math].

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\subsection{Пара}

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

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

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

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

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

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

\begin{code} pred' = Lam "n" $

       Lam "s" $ 
       Lam "z" $ 
           snd `App` (Var "n" 
                           `App` ( 
                                    Lam "p" $ pair' 
                                       `App` (Var "s" `App` (fst `App` Var "p"))
                                       `App` (fst `App` Var "p")
                                 )
                           `App` ( pair' `App` Var "z" `App` Var "z" )
                       )

\end{code}

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

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

\begin{code} le' = Lam "n" $ Lam "m" $ isZero' `App` (minus' `App` Var "n" `App` Var "m") less' = Lam "n" $ Lam "m" $ le' `App` Var "n" `App` (pred' `App` Var "m") eq' = Lam "n" $ Lam "m" $ and'

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

\end{code}

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

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

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

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

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

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

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

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

\end{code}

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

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

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

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

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

\end{code}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\subsection{Списки}

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

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

\end{itemize}

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

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

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

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

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

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

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

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

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

eliminateMultiplier = fix' `App` eliminateMultiplier'

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

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

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

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

\ignore{ \begin{code}

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

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

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

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

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

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

\end{code} }

\end{document} [1]