Entry tags:

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

Лямбда-исчисление.
Коротко и неформально.

Лямбда-исчисление - это правила построения и вычисления безымянных функций.

И перейдем сразу к примерам.

Вот запись функции, которая получает на вход число и вычисляет значение, большее его на единицу:

    (\x.x+1)

Что здесь к чему? Сама функция записана в скобочках. Символ '\' будет впредь обозначать строчную греческую букву λ (кстати, в Haskell использется именно это обозначение, и такая безымянная функция в Haskell будет выглядеть \x -> x+1). Далее, до точки, идут аргументы функции, а после точки -- выражение.

Применение функций к аргументам записывается просто -- через пробел. Вот так:

    (\x.x+1) 2

Мы можем упрощать записанное нами выражение, подставляя вместо переменных их значения (бета-упрощение, бета-редукция):

    (\x.x+1) 2 -- применяем бета-редукцию, подстановку значений аргументов.
==> (2+1) -- применяем дельта-редукцию, то есть, вычисление функции от аргументов.
==> 3

Так оно и происходит. И даже в реальной жизни, когда идет рассуждение о программе.

Еще немного поупражняемся. Сделаем-ка функцию от двух аргументов, все ту же сумму:

    (\x y.x+y)

Ага, сделали. Что будет, если мы применим ее к одному аргументу? Сейчас выясним:

    (\x y.x+y) 1 -- примением бета-редукцию, заменим x на 1.
==> (\y.1+y)

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

И, в лучших традициях формальной математики, перепишем только что обнаруженный нами факт:

    (\x y.x+y) эквивалентно (\x.(\y.x+y))

Этот прием назвается карринг (currying), и именно он не стал шонфикелингом. ;)

Я еще упомяну о необходимости переименовывать переменные, чтобы после подстановки значений не возникало проблем, какой это y -- этот y является нашей переменной, или результатом подстановки?

Вот. А пока займемся другой проблемой. Посмотрим на выражение (\x.x x)(\x.x x). Попробуем его упростить:

    (\x.x x) (\x.x x) -- переименуем x в самом левом выражении в z.
    (\z.z z) (\x.x x) -- затем подставим вместо z его значение (\x.x x).
    ((\x.x x) (\x.x x)) -- где-то мы это уже видели.

Мы получили невычислимое выражение. Оно настолько просто, что его можно вычислять до бесконечности. ;) И оно чуть-чуть интереснее, чем банальное деление на ноль.

Зато это дает возможность продемонстрировать еще кое-что. На этот раз мы возьмем в качестве кандидата на упрощение следующее выражение -- (\x.1)((\x.x x) (\x.x x)).

Если мы начнем вычислять аргумент, то никогда не остановимся. Однако, если мы начнем сразу с тела функции ((\x.1) -- функция, которая всегда вычисляется в 1), то сразу придем к ответу -- 1. Отличие разительно, не находите?

Это пример того, как порядок вычисления выражений может оказать влияние на результат вычислений одного и того же выражения. Обычно выделяют два порядка вычислений: сперва упрощаем самый правый член в записи вычисления или сперва упрощаем самый левый член вычисления. Первый вариант приводит к тому, что сперва вычисляются все аргументы, а потом само выражение, а второй -- к тому, что мы откладываем вычисление аргументов до тех пор, пока они нам не понадобятся.

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

В свою очередь, первый вариант применяется энергичными (жадными) языками и легче для реализации. OCaml и LISP используют именно его.

Вообще, никакая современная программа не может обойтись без ленивых вычислений. Тот же if..then..else.. откладывает вычисления.

Кстати, а давайте сочиним условную конструкцию с помощью лямбда-исчисления? Хорошо, тем более, что это очень просто.

Что делает if c then a else b? В зависимости от значения c (condition, условия) оно выбирает либо значение a, либо значение b. Итак, конструкия if c then a else b -- это функция с тремя параметрами:

    (\c.a.b.???)

Нам надо выяснить, что может находиться вместо знаков вопроса.

Во-первых, там не может быть никаких if c then a else b, поскольку мы именно это и определяем. Во-вторых, там должен находится выбор значений a или b в зависимости от c, при этом на структуру самого c ограничений нет. Если мы примем значение (\a.b.a) за логическую истину, а значение (\a.b.b) -- за ложь, то можно подставить вместо знаков вопроса выражение c a b. Сейчас проверим:

    (\c.a.b.c a b) (\a.b.a) 1 2 -- то же, что if true then 1 else 2.
==> (\a.b.(\x.y.x) a b) 1 2
==> (\a.b.a) 1 2
==> 1

Вроде, правильно. Как записать if false then 1 else 2, и во что это раскроется, я оставлю в качестве упражнения.

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

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

Ну, и в качестве заключения.

Я довольно долго исследовал всякие системы на предмет упрощения труда программиста. На данный момент я считаю, что лямбда-исчисление с ленивым порядком вычислений позволяет записать решения самым коротким способом при самой лучшей эффективности исполнения. То есть, если надо записать решение задачи короче, то будет значительно менее эффективно, при разнице в длине записи порядка десятка процентов, и не всегда в пользу не-Haskell записи (см. сравнение Haskell vs. Maude, есть такое в сети). А если надо эффективнее, то получится значительно длинее (Haskell vs. C, такое тоже есть).

На этом, пожалуй, все. ;)