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

1936: два человека закрыли главный вопрос математики

Гильберт мечтал об алгоритме, который доказывает всё. В 1936 году Алан Тьюринг и Алонзо Чёрч - независимо, за несколько месяцев друг от друга - доказали, что такого алгоритма нет. Тьюринг через машину с лентой и головкой. Чёрч через три символа и одно правило подстановки. Когда они встретились и сравнили результаты - оказалось, что оба описали одно и то же. Этот факт стал тезисом Чёрча-Тьюринга. Но именно модель Чёрча дала язык для функционального программирования: Lisp 1958, ML 1973, Haskell 1990 - прямые потомки тех трёх правил.

Три правила, которые заменили всю математику вычислений

Лямбда-исчисление - это формальная система с тремя синтаксическими конструкциями и одним правилом вычисления. Никаких чисел, никаких строк, никаких типов данных - только функции и их применение. Хаскелл Карри говорил, что это 'алгебра функций'. Современный Haskell - это лямбда-исчисление с синтаксическим сахаром поверх.

**Три конструкции лямбда-исчисления:** 1. **Переменная**: `x` - имя 2. **Абстракция**: `λx.M` - функция с параметром `x` и телом `M` 3. **Аппликация**: `M N` - применение функции `M` к аргументу `N` Всё остальное - синтаксический сахар или кодирование через эти три.

Связанные и свободные переменные - ключевое понятие. В `λx.x y` переменная `x` **связана** (введена λ), а `y` - **свободная** (пришла извне). Именно это разделение лежит в основе лексических замыканий в JavaScript, Python и Rust.

PyTorch autograd знает лямбда-исчисление - в буквальном смысле. Каждый слой `nn.Module` - это функциональное отображение. Каждый `lambda x: x * 2` в Python - это `λx.x * 2` по Чёрчу. Когда модель строит вычислительный граф, она строит дерево аппликаций - именно так, как Чёрч описал вычисление в 1936.

β-редукция: единственное правило вычисления

Одно правило управляет всем. β-редукция: `(λx.M) N → M[x := N]` - подставить `N` вместо `x` в теле `M`. Никакой стек вызовов, никакая память - только текстовая подстановка. Все вычисления сводятся к одному шагу, повторяемому до тех пор, пока нельзя редуцировать дальше (нормальная форма).

**α-эквивалентность** (переименование): `λx.x ≡ λy.y` - имя параметра не важно, важна структура. **η-редукция**: `λx.f x → f` если `x` не встречается в `f` - убрать лишнюю обёртку. Вместе с β-редукцией это три закона, которые определяют равенство лямбда-термов.

Стратегия редукции имеет значение. **Call-by-value** (строгое вычисление, Python/JavaScript) - сначала вычислить аргумент, потом передать. **Call-by-name** - передать невычисленный аргумент, вычислять только при использовании. **Call-by-need** (ленивое вычисление, Haskell) - то же что call-by-name, но результат запоминается. Один и тот же лямбда-терм, три разные стратегии исполнения.

XLA (компилятор TensorFlow/JAX) реализует call-by-need для тензоров - вычисление откладывается до `jit.run()`. Именно поэтому JAX позволяет писать `jax.grad(jax.grad(f))` - двойной градиент работает потому что трансформации функций ленивы, они строят граф редукций, а не выполняют их.

**Расходящиеся термы**: не каждое лямбда-выражение имеет нормальную форму. Классический пример - Омега-комбинатор: `(λx.x x)(λx.x x) → (λx.x x)(λx.x x) → ...` бесконечный цикл. Это то, что соответствует `while True: pass` в Python - вычисление без остановки.

Church encoding: числа, булевы и Y-комбинатор из ничего

Алонзо Чёрч показал нечто шокирующее: числа не нужны как примитивы. Число `n` - это функция, которая применяет другую функцию `n` раз. Ноль применяет ноль раз. Один - один раз. Сложение - это применить `f` `m+n` раз. Вся арифметика из чистых функций, без чисел.

Булевы значения кодируются так же элегантно. `true` - выбирает первый из двух аргументов. `false` - выбирает второй. `if-then-else` - просто применение булева к двум ветвям. Структуры данных? Пара `(a, b)` - это функция, которая возвращает нужный элемент по запросу. Чёрч в 1936 году построил всю математику из трёх конструкций.

**Y-комбинатор** - самая странная вещь в лямбда-исчислении. Он позволяет писать рекурсию без имён функций. В чистом лямбда-исчислении нет именованных функций - нельзя написать `f = λx.f x`. Y-комбинатор обходит это: он принимает функцию и возвращает её фиксированную точку. `Y = λf.(λx.f(x x))(λx.f(x x))` Применение: `Y f → f (Y f)` - бесконечная рекурсия через подстановку.

Связь с современными языками прямая. Haskell - это типизированное лямбда-исчисление System F с синтаксическим сахаром. OCaml и F# - это ML, который Робин Милнер в 1973 году построил именно как практическую реализацию лямбда-исчисления с типами. Lisp 1958 года - первый язык, где s-expressions - это λ-термы в скобочной нотации. TypeScript `type F<T> = (a: T) => T` - это точная запись типа тождественного функтора из системы типов, восходящей к Чёрчу.

Три идеи, которые остаются

• Лямбда-исчисление - три конструкции (переменная, абстракция, аппликация) и одно правило (β-редукция). Этого достаточно для любых вычислений.
• β-редукция: `(λx.M) N → M[x := N]` - подстановка аргумента в тело. Всё вычисление сводится к этому шагу.
• Church encoding: числа, булевы, пары - всё из функций. Число n - это 'применить функцию n раз'. Рекурсия - через Y-комбинатор.
• Стратегия редукции - это семантика языка: call-by-value (Python/JS), call-by-need (Haskell). Один терм, разные стратегии - разное поведение.
• Haskell, OCaml, Scala, TypeScript - это лямбда-исчисление с типами и синтаксическим сахаром. Не метафора - буквально.

Где лямбда-исчисление продолжается

Три правила 1936 года живут в каждом современном функциональном языке и системе типов.

• Функциональное программирование — Прямая реализация лямбда-исчисления с синтаксическим сахаром
• Вывод типов — Hindley-Milner типизирует лямбда-термы, System F - полиморфные
• Theorem Provers — Curry-Howard: типы - это теоремы, лямбда-термы - это доказательства
• IO и монады — Монадическое IO в Haskell - лямбда-термы с эффектами в типах

Вопросы для размышления

• Когда в JavaScript пишут `arr.map(x => x * 2).filter(x => x > 3)` - это цепочка лямбда-аппликаций. Видна ли эта связь в повседневном коде?
• TypeScript тип `<T>(f: (a: T) => T) => (a: T) => T` - это точный тип лямбда-терма в System F. Как это меняет чтение типовых сигнатур?
• JAX позволяет `jax.grad(jax.grad(loss))` потому что трансформации ленивы - строят граф редукций. Какие ещё 'ленивые' паттерны встречаются в современных фреймворках?

Связанные уроки

• plt-18-fp — Лямбда-исчисление - математическая база функционального программирования
• plt-04-type-inference — Типизированное лямбда-исчисление (System F) лежит под Hindley-Milner
• plt-20-logic-programming — Prolog и лямбда - две альтернативные модели вычислений за пределами Тьюринга
• plt-35-theorem-provers — Curry-Howard: программы - это доказательства, лямбда-термы - это типы
• plt-30-io-monads — Монады - ленивый IO в Haskell строится поверх лямбда-абстракции
• ml-01