# λ-исчисление

Фишки функционального программирования проникли в большинство современных императивных языков, таких как Java, C#, C++, Python и так далее. Я предлагаю вам изучить основы λ-исчисления, т.к. уместное применения тех же лямбд в своем коде улучшает его читаемость и простоту в поддержке.

λ-исчисление само по себе - это очень простая штука. Оно является некой абстракцией, позволяющей описывать вычисления в декларативном программировании. В нем нет условий, циклов и каких-либо jump'ов в целом, типов данных и встроенных операторов, только функции и их примение. Однако для простоты изложения, я предлагаю на время расширить λ-исчисление натуральными числами и простыми операциями над ними.

## Введение

Термы λ-исчисления бывают 3 видов:

| Описание | Терм |
| -------------- | ----------------------------------- |
| Переменная | x |
| λ-абстракция | (λx.M) (x - переменная, M - тело) |
| Аппликация | (M N) (M - функция) |

Маленькими буквами мы будем обозначать переменные в привычном смысле, большими -- мета-переменные, вместо которых можно подставить любой другой λ-терм.

Проводя аналогии с языками программирования, становится понятно, что **λ-абстракция** -- это просто создание функции, а **аппликация** (от слова apply) -- это вызов функции.

Если формально определять аппликацию, то это просто подстановка аргумента функции вместо всех его вхождений в тело, обозначается как M[x:=N]

## Примеры

Рассмотрим пару примеров, чтобы было понятнее.

Самая простая функция которую мы можем придумать: `(λx.(x))`, т.н. **identity function**, обычно сокращается до id. Результат ее выполнения очевиден: `(λx.(x)) N => N`

Рассмотрим более сложную функцию: `(λx.(x+2))` (как вы помните, мы договорились расширить λ-исчисление натуральными числами). `(λx.(x+2)) 3 => 3 + 2`. В рамках λ-исчисления мы считаем вычисление завершенным, хотя конечно, зная то, как работает сложение, мы можем довести все до конца и получить 5.

Играясь так с разными функциями, вы, рано или поздно, зададитесь вопросом о том, как в λ-исчислении выражать функции от 2 и более переменных. Сначала может показаться, что для этого нужно расширить определение, но это совсем не так.

Как мы знаем, λ-абстракция может вернуть нам любой λ-терм, в т.ч. другую λ-абстракцию. Давайте воспользуемся этим свойством и напишем функцию для сложения: `(λa.(λb.(a+b)))`. Взглянем на ее применение: `((λa.(λb.(a+b))) 5) 7 => (λb.(5+b)) 7 => 5 + 7` -- мы получили ровно то, что хотели! Подобная операция называется **каррированием** (currying), и это первая важная мысль, которую можно подчерпнуть из λ-исчисления.

## Скобки

Если только вы не любитель lisp'a, то предыдущий пример должен был оставить неприятное послевкусие от обилия скобок, и не зря. Существуют правила, по которым эти скобки можно убирать, не меняя смысл выражения.

1) Очевидно, скобки вокруг всего терма можно опускать
2) Аппликация левоассоциативна: `x y z` это `(x y) z`
3) Абстракция ведет себя жадно -- без скобок считается, что тело функции идет настолько вправо, насколько это возможно. Например, `λx.λy.x y x` это тоже самое, что и `λx.(λy.(x y x))`

Тогда наш пример каррирования можно переписать как: `λa.λb.a + b`. Еще, когда у нас есть несколько λ-абстракций подряд, можно опускать вторую λ и ставить пробел между аргументами: `λa b.a + b`

## Связанность и комбинаторы

Введем еще пару определений. Переменную x назовем **связанной** для данной λ-абстракции с телом M, если λ-абстракция выглядит так: λx.M. Если переменная не связанная, тогда она **свободная**. Например, в выражении `λy.x y` x входит свободно, т.к. нет λ-абстракции, которая его определяет. Но, в функции `λx.λy.x y` x уже связан относительно внешней λ. Другой пример: `(λx.x) x` - вхождение x в левой λ-абстракции связанное, а правое вхождение свободное.

Переменная может быть связанной несколько раз: `(λx.(λx.x z) x) x` - в этом примере x связан 2 раза и один раз свободен, z свободна.

Термы, в которых все переменные связанные называют **комбинаторами**. Парочка примеров:

- I = `λx.x` - знакомая нам id
- K = `λx.λy.x` - функция принимает 2 аргумента и отбрасывает второй
- K* = `λx.λy.y` - как K, только наоборот
- Y = `λf.(λx.f (x x)) (λx.f (x x))` - довольно известный комбинатор, т.н. комбинатор неподвижной точки
- ω = `λx. x x` - самоприменение
- Ω = ω ω = `(λx. x x) (λx. x x)` - забавный терм, попозже рассмотрим почему

И т.д. (их довольно много)

## Редукция и стратегии редукции

λ-исчисление было создано как формализация понятия вычисления (кстати, до машины Тьюринга, но они эквивалентны, поэтому λ-исчисление в каком-то смысле язык программирования). Но, если подумать, то единственное вычисление которое мы можем проводить - это аппликация λ-абстракций. λ-термы которые мы можем вычислить имеют специальное название: **редексы**. Это выражения вида: `(λx.t) M`, т.е. те, в которых мы можем провести аппликацию. Вычисление редекса еще называют **β-редукцией** (почему не α будет понятно позже).

Терм без редексов называется термом в **нормальной форме**. Существуют разные **стратегии вычисления** редексов. Рассмотрим на примере: `id (id (λz. id z))`.

1) **Полная β-редукция** - вычисляем редексы в случайном порядке: `id (id (λz. id z))` -> `id (id (λz.z))` -> `id id` -> `id`
2) **Нормальный порядок вычислений** - вычисляем самый левый редекс: `id (id (λz. id z))` -> `id (λz. id z)` -> `λz. id z` -> `λz.z` -> `id`
3) **Вызов по имени** - как и прошлый порядок, но с запретом на вычисление внутри абстракций, т.е. мы остановим вычисление на `λz. id z` (модифицированная версия используется в Haskell, называется ленивым вычислением, в следующем посте рассмотрим подробнее)
4) **Вызов по значению** - вычисляем самый левый редекс, у которого мы уже вычислили значение справа: `id (id (λz. id z))` -> `id (λz. id z)` -> `λz. id z` (аналогично тому, как поступает большинство языков программирования - сначала считаем аргументы функции, потом саму функцию, в следующем посте тоже рассмотрим внимательнее)

Уже здесь становится понятно, что от порядка вычисления зависит конечный результат. Более того, мы можем найти такой терм, который не будет иметь нормальной формы. Например, Ω = `(λx. x x) (λx. x x)` -> `(λx. x x) (λx. x x)` = Ω (существуют термы, которые будут только увеличиваться при попытке их вычислить)

## α-эквивалентность и η-преобразование

Узнаем еще пару полезных операций над λ-функциями. Так, α-эквивалентностью мы будем называть переименование аргумента `λx.M -> λy.M[x:=y]`. η-преобразование заключается в следующем: `λx.t x` -> `t` (x конечно в t не входит). И действительно, ясно, что исходное выражение - это функция одного аргумента, которая передает свой аргумент в t; но ведь t это тоже функция одного аргумента, поэтому исходное выражение можно упростить. В следующем посте мы рассмотрим η-преобразования на практике.

## Вывод

В целом, это тот минимум знаний по λ-исчислению, который уже может быть полезен в прикладном коде. Стоит уточнить, что для простоты восприятия многие вещи я вводил неаккуратно, но за более точными определениями я предлагаю обратиться в источники, которые я оставлю в комментариях. Можно было еще много о чем рассказать: индексы Де Брауна, почему Y-комбинатор настолько известен, определение чисел/условий и прочего в чистом λ-исчислении, типизированное λ-исчисление и так далее. Что-то из этого разбирается в источниках, которые я приложу, что-то может стать материалом следующих постов.