Начнем с несколько отстраненной темы. В математике полно функций — алгебраических вроде exp, тригонометрических вроде sin и других. Функции можно задавать и руками, например:
f(x) = 2x + 1
Эта запись появилась еще в 18 веке, когда никакой речи об анализе функций с той точки зрения, с которой мы их рассмотрим, идти не могло. Все, что означает эта запись — это что
f(1) = 2*1 + 1 f(2) = 2*2 + 1 f(3) = 2*3 + 1 ...
и так далее.
Но есть одно "но", которое перечеркивает все удобства. Проблема в том, что f(x) = 2x + 1 утверждает, что буква f, за которой следует открывающая скобка, затем какое-то выражение, затем закрывающая скобка, обозначает такое-то значение. О том, что означает сама буква f по отдельности — речи не идет, и даже из контекста это не всегда понятно.
Попробуйте как программист упростить следующую запись:
f(x) = sin(sin(sin(x))) + cos(cos(cos(x))) + tg(tg(tg(x))) + ctg(ctg(ctg(x)))
У этой задачи есть очевидное (для программиста), изящное и понятное решение:
rep(x, g) = g(g(g(x))) f(x) = rep(x, sin) + rep(x, cos) + rep(x, tg) + rep(x, ctg)
Вот только неправильное. Потому что в алгебре сами по себе три буквы sin ничего не означают, тем более — если они подаются как параметр какой-то еще функции. Перефразируя: в классической математике нет способа воспользоваться функцией, кроме как сразу ее применить к какому-либо аргументу. Говоря формально: в классической математике нет функций высшего порядка.
Для того, чтобы названия функций имели смысл сами по себе, а не только при применении к какому-либо аргументу, вводят дополнительную нотацию. Было:
f(x) = 2x+1
Стало:
f := \x. 2x+1
Знак λ (лямбда) обозначает функцию. После него идет название аргумента, затем точка, затем — выражение, по которому функция вычисляется. Дальше с функциями можно работать, как в обычной математике:
double := \x. x*2 triple := \x. x*3 x_five := \x. (double(x)) + (triple(x))
Если мы попробуем теперь правильно расписать функцию "rep", нас ожидает сюрприз. λ-функция всегда принимает ровно один аргумент. А если нужно больше? Для этого мы используем трюк, называемый каррированием. Мы определим функцию, которая принимает первый аргумент и возвращает новую функцию, которая принимает второй аргумент и возвращает еще одну функцию, которая принимает третий аргумент, и так далее. Последняя функция примет последний аргумент и вернет собственно результат. Вот так, например, можно определить сложение:
add := \a. \b. a + b
Если, например, формально посчитать add 1, то получится \b. 1 + b — функция возвращает другую функцию. Теперь, если эту новую функцию опять применить к числу, скажем, два, получится 1 + 2, то есть 3.
(add(1))(2) = 3
Поскольку много скобок ставить неудобно, есть два упрощения. Во-первых, f x — это то же самое, что f(x). Во-вторых, поскольку каррирование используется очень часто, то f x y — это то же самое, что (f x) y. Упрощая:
add 1 2 = 3
Вот, кстати, как тот пример с rep записывается правильно:
rep := \x. \g. g(g(g x)) f := \x. (rep x sin) + (rep x cos) + (rep x tg) + (rep x ctg)
В λ-исчислении выражения составляются при помощи создания λ-функций и применения их друг к другу.
Давайте формально определим, что значит "вычислить выражение". Для этого можно проводить над выражением друг за другом следущие операции:
\x. x*2+t можно заменить на \y. y*2+t.(\x.E1)(E2) можно заменить на E1, в котором все вхождения x заменяются на E2. Например: (\x. 2*x+1)(1+2) можно заменить на 2*(1+2)+1.\x.(E x) разрешается заменить на E (конечно, только если x не используется внутри E). Например: \x.(sin x) — это то же самое, что sin. К слову, почему это интуитивно очевидное правило нужно вводить отдельно: в некоторых областях математики для задания функции недостаточно ее значений во всех точках. Например, если мы исследуем полиномы по модулю именно как полиномы, а не как функции. Например, если вычисления проводятся по модулю 2, x^2 + x + 1 — это не то же самое, что 1.Для вычисления значений выражений мы будем применять в каком-то порядке эти операции. Вообще говоря, в большинстве случаев достаточно β-редукции, но об этом чуть позже. Применять эти операции мы будем, пока не получится выражение, в котором нет вызовов функций. Такое выражение называется β-нормальной формой.
Теперь предлается немного расширить границы применимости λ-исчисления. В самом деле, у нас такая стройная теория, а 5 + 7 мы все еще считаем используя какую-то арифметику. Пора от этого избавляться.
Итак, отныне каждый раз, когда в коде будут использоваться числа, мы будем интерпретировать их как специальные λ-функции, а именно:
0 := \f. \x. x 1 := \f. \x. f x 2 := \f. \x. f(f x) 3 := \f. \x. f(f(f x) 4 := \f. \x. f(f(f(f x)) ...
Словом, число n — это λ-функция, которая принимает два аргумента (ну, через каррирование): f и x, а затем n раз применяет f к x. Например: 3 g y = g(g(g y))), а 3 g = \x. g(g(g x)) (так сказать, утроение функции).
Теперь мы можем реализовать, например, инкремент (succ — сокращение от successor, следующий):
succ := \n. \f. \x. n f (f x)
Иными словами, succ принимает число n, и возвращает нечто. Когда это нечто вызывается от f и x, оно не сразу передает эти два аргумента числу n, а сначала лишний раз применяет f к x — вот и получается на один больше. Если вы любите формальности, вот вам пример с вычислением β-редукциями:
succ 3 -> -> \f. \x. 3 f (f x) -> -> \f. \x. (\g. \y. g(g(g y))) f (f x) -> -> \f. \x. (\y. f(f(f y))) (f x) -> -> \f. \x. f(f(f(f x))) = 4
Теперь можно реализовать и сложение. Сложение a и b — это значит a раз применить succ к b. Записывается это на удивление просто:
add := \a. \b. a succ b = \a. a succ
Дальше по списку идет умножение. Здесь проще воспользоваться пониманием числа как умножителя функции. Произведение a на b — это нечто, принимающее функцию и повторяющее ее a*b раз. Для этого достаточно ее сначала повторить b раз, затем результат — a раз:
mul := \a. \b. \f. a (b f)
Например:
mul 2 3 -> -> \f. 2 (3 f) -> -> \f. 2 ((\g. \y. g(g(g y))) f) -> -> \f. 2 (\y. f(f(f y))) -> -> \f. (\g. \x. g(g x)) (\y. f(f(f y))) -> -> \f. \x. (\y. f(f(f y))) ((\y. f(f(f y))) x) -> -> \f. \x. (\y. f(f(f y))) (f(f(f x))) -> -> \f. \x. f(f(f(f(f(f x))))) = 6
Чтобы вы почувствовали всю красоту λ-исчисления, реализуем еще возведение в степень pow a b. pow a b — это то же самое, что \f. a (a (... (a f))), где a повторяется b раз. Погодите-ка, повторение функции — это же ровно то, как числа и определены!
pow := \a. \b. b a
Несколько сложнее ввести декремент и вычитание: проблема в том, что понять, что значит "применить функцию -1 раз" — не самое простое дело. К этой задаче мы вернёмся чуть позже. А в следующей части займёмся логикой.