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

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

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

Лямбда-исчисление — формальная система, придуманная в 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]~--- за ноль или более. \subsection{$\eta$-редукция} Рассмотрим выражение вида

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