Мы вводим определения, внутри которых только создаем и применяем функции. И этого уже достаточно, чтобы реализовать что угодно! Но можно ли еще что-то выбросить, чтобы дальше упросить нашу модель?
Теперь мы начнем работать в неожиданную и, можно сказать, противоположную сторону: мы будем избавляться от присваиваний. Ну, то есть, пусть мы хотим вычислить выражение, а оно использует какие-то другие функции, которые определены раньше через f := .... От такого мы будем избавляться. Пусть, например, у нас было что-то в духе:
rep := \x. \g. g(g(g x)) f := \x. add (rep x sin) (rep x cos)
И нас интересует значение f 3. Тогда определение f я заменю на такое:
f := (\rep. \x. add (rep x sin) (rep x cos)) (\x. \g. g(g(g x)))
Что тут произошло: мы сначала сделали функцию, которая принимает параметр rep, а затем в качестве этого параметра передали ей собственно функцию rep. Ясно, что программа все еще работает. При этом код даже почти не увеличился в объеме.
Далее, раскроем f 3:
(\rep. \x. add (rep x sin) (rep x cos)) (\x. \g. g(g(g x))) (3)
Теперь получилась "программа", в которой нет присвоения переменных, то есть просто выражение. Вообще, в общем случае это:
a := E1 E2 ->> ?
Эквивалентно этому:
(\a. E2)(E1) ->> ?
Но с рекурсивными функциями это становится нетривиальной задачей. Кстати, на счет рекурсивных функций. Давайте для примера реализуем вычисление факториала.
fact := \n. ...
Если число n — нуль, сразу можно закончить и вернуть единицу:
fact := \n. (iszero n) 1 ...
Если нет — вызовемся рекурсивно от n - 1 и умножим результат на n:
fact := \n. (iszero n) 1 (mul n (fact (pred n)))
Ну и теперь осталось избавиться от присвоений. Пусть, например, мы хотим посчитать fact 4:
fact := \n. (iszero n) 1 (mul n (fact (pred n))) fact 4
Пробуем:
(\fact. fact 4) (\n. (iszero n) 1 (mul n (fact (pred n))))
Нда. Теперь у нас семантическая ошибка. Функция-то рекурсивная, а переменная fact внутри самой функции не определена. Проблемка. Придется что-нибудь придумывать.
На этом моменте я предлагаю немного отвлечься и вспомнить про похожие проблемы в других языках. Например, в C++. Точно так же я определю рекурсивную функцию:
void dfs(int u) {
for (int v : adj[u]) {
dfs(v, u);
}
}
void solve() {
dfs(0);
}
Теперь попробую ее перенести внутрь solve в виде лямбда-функции:
void solve() {
auto dfs = [](int u) {
for (int v : adj[u]) {
dfs(v, u);
}
};
dfs(0);
}
И ничего у меня не получится, потому что auto пытается определить тип лямбда-функции, а она использует внутри себя переменную dfs, тип которой еще не определен. Рекурсия.
Тогда я воспользуюсь широко известным в узких кругах трюком: я передам dfs'у в качестве нового первого параметра его самого:
void solve() {
auto dfs = [](auto dfs, int u) {
for (int v : adj[u]) {
dfs(dfs, v, u);
}
};
dfs(dfs, 0);
}
Вернемся к факториалу.
С этого мы начинали:
fact := \n. (iszero n) 1 (mul n (fact (pred n))) fact 4
Сделаем замену, как с dfs'ом, чтобы факториал мог вызывать сам себя изнутри:
fact1 := \fact1. \n. (iszero n) 1 (mul n (fact1 fact1 (pred n))) fact1 fact1 4
fact1 fact1 писать каждый раз при вызове неудобно — вынесем это отдельно в функцию fact:
fact1 := \fact1. \n. (iszero n) 1 (mul n (fact1 fact1 (pred n))) fact := fact1 fact1 fact 4
Для удобства и симметрии fact1 fact1 внутри определения функции тоже оптимизируем. Здесь можно было бы написать fact, но тогда мы от рекурсии никак не избавимся. Вместо этого просто вынесем fact1 fact1 в параметр функции, которую мы тут же вызываем, как раньше делали в нерекурсивными функциями:
fact1 := \fact1. (\fact. \n. (iszero n) 1 (mul n (fact (pred n)))) (fact1 fact1) fact := fact1 fact1 fact 4
Вставим определение fact1 внутрь fact:
fact := (\fact1. fact1 fact1) (\fact1. (\fact. \n. (iszero n) 1 (mul n (fact (pred n)))) (fact1 fact1)) fact 4
В принципе, здесь уже можно было бы остановиться, но мы пойдем дальше. Внутренняя часть определения fact смахивает на изначальное (рекурсивное) определение, так что вынесем-ка его ради интереса пока в отдельную переменную.
factrec := \factrec. \n. (iszero n) 1 (mul n (factrec (pred n))) fact := (\fact1. fact1 fact1) (\fact1. factrec (fact1 fact1)) fact 4
Немного переименуем переменные:
factrec := \factrec. \n. (iszero n) 1 (mul n (factrec (pred n))) fact := (\x. x x) (\x. factrec (x x)) fact 4
Смотрите-ка, что произошло. Мы реализовали factrec, как реализовывали бы обычную рекурсивную функцию, но с одним исключением — добавили в начале \factrec.. Это, можно считать, неожиданный синтаксический прием. Затем мы по определенному правилу преобразовали factrec в функцию fact, которую можно использовать как любую обычную функцию. А нельзя ли это проделать не только для факториала, но и для других функций? Можно. Чтобы яснее это увидеть и понять, что вообще произошло, вынесем это правило преобразования в отдельную функцию.
factrec := \factrec. \n. (iszero n) 1 (mul n (factrec (pred n))) Y := \f. (\x. x x) (\x. f (x x)) fact := Y factrec fact 4
Вообще говоря, такая функция (Y, в этом примере) — комбинатор. Напомню, комбинаторы — это такие функции, которые не используют никакие внешние (свободные) переменные. Давайте для красоты проведем еще один раз β-редукцию функции Y:
Y := \f. (\x. f (x x)) (\x. f (x x))
И последний шаг, избавимся от factrec. Как удивительно просто стало писать рекурсивные функции без рекурсивных определений, а?
Y := \f. (\x. f (x x)) (\x. f (x x)) fact := Y (\fact. \n. (iszero n) 1 (mul n (fact (pred n)))) fact 4
Рефлексия. Была рекурсивная функция fact := ... fact ..., которая использовала свое имя внутри себя. Мы ее заменили на функцию fact := Y (\fact. ... fact ...), которая с точки зрения пользователя выглядит и работает так же и синтаксис использует очень похожий, но зато не использует внутри себя свое же имя. А значит, теперь можно использовать наши старые методы для того, чтобы окончательно избавиться от присвоений.
Теперь мы можем писать программы, используя только создание и применение λ-функций!
По сути, в нашем примере мы сначала сделали функцию, принимающую факториал и реализующую на его основе сам же факториал, после чего передали ее в Y-комбинатор, и получили готовый факториал:
fact_generator := \fact. \n. (iszero n) 1 (mul n (fact (pred n))) fact := Y fact_generator
То есть Y-комбинатор принимает функцию, создающую объект на основе самого себя, и возращает нам готовый объект. Рекурсия в самом ее общем виде.
Y-комбинатор позволяет не только рекурсивно вычислять что-то конечное, но и рекурсивно создавать бесконечные структуры данных. Например, список всех натуральных чисел, или список всех простых чисел.
Есть и другой способ посмотреть на Y-комбинатор. Пусть у нас есть какая-нибудь функция f, и мы хотим вычислить Y f. Проведем β-редукцию:
Y f -> -> (\x. f (x x)) (\x. f (x x)) -> -> f ((\x. f (x x)) (\x. f (x x))) -> -> f (Y f)
Просто задумайтесь: Y-комбинатор доказывает, что у любой абсолютно произвольной функции существует неподвижная точка! Более того, он конструирует эту неподвижную точку в меньше, чем 30 символов! Поэтому, кстати, Y-комбинатор также называется комбинатором неподвижной точки и в коде нередко обозначается fix. Y и fix — одно и то же, но мы будем различать их с точки зрения семантики: для задания рекурсивных функций будем использовать Y, для получения неподвижной точки — fix.