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

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

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

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

    (\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))

Я еще упомяну о необходимости переименовывать переменные, чтобы после подстановки значений не возникало проблем, какой это 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

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

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

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

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

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