Lambda resources

Lambda Calculus and Lambda Calculators (implementation)

http://okmij.org/ftp/Computation/lambda-calc.html

Type system

The Lambda-calculus, Combinatory Logic, and Type Systems

Комбинаторы - это просто!

Практика функционального программирования
Выпуск 1, 2009
http://www.scribd.com/doc/44147436/Functional-Programming-Russian

Lambda in short

From: http://thesz.livejournal.com

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








Вот запись функции, которая получает на вход число и вычисляет значение, большее его на единицу:
(\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, такое тоже есть).
1. Деревья решений. Прямая и обратная цепочка рассуждений. Алгоритм CLS
2. Логика предикатов. Основные понятия. Особенности использования кванторов.
3. Индуктивный вывод. Виды математической индукции.
4. Рекурсия. Виды рекурсий.
5.  Метод доказательства от противного.
6. Приведение к префиксной нормальной форме. Основные правила.
7. Скалемизация.
8. Приведение к клаузальной нормальной форме.
9. Метод резолюции для высказываний.
10. Алгоритм унификации. НОУ. Правила допустимости подстановок.
11. Метод резолюции для предикатов. Особенности метода при использовании равенств.
12.  Генетические алгоритмы. Основные характеристики. Примеры. Разновидности алгоритмов
13. Нейронные сети. Основные понятия. Вероятностные сети. Карта Кохонена. LVQ. Сети Хоппфилда и BAM. Сеть BP – SOM