Lambda Calculus и вычислимость

Машина Тьюринга - не единственный способ формализовать вычисления. В том же 1936 году Чёрч предложил lambda-исчисление - систему переписывания без состояния и памяти. Оба подхода оказались эквивалентными, и это открытие изменило понимание природы вычислений.

• **Haskell, ML, Lisp** - функциональные языки выросли напрямую из lambda-исчисления
• **Типовые системы** - System F и просто типизированное lambda-исчисление лежат в основе Haskell, Scala, Rust
• **Proof assistants** (Coq, Agda) - используют зависимо типизированное lambda-исчисление
• **Компиляторы** - CPS и A-нормальная форма - стандартные трансформации lambda-выражений

Lambda-исчисление: синтаксис и редукции

В 1936 году Алонзо Чёрч предложил полностью другой ответ на вопрос «что значит вычислить?» - не машина с лентой, а система переписывания выражений. Никакого состояния, никаких ячеек памяти - только функции и их применение. Lambda-исчисление строится из трёх правил и помещается на одну страницу.

Вычисление - это редукция. Три вида: **alpha** (переименование переменной), **beta** (подстановка аргумента в тело функции) и **eta** (сокращение избыточной обёртки). Beta-редукция - главная:

**Нормальная форма** - выражение, к которому нельзя применить бета-редукцию. Омега-комбинатор `(λx. x x)(λx. x x)` редуцируется в себя - аналог бесконечного цикла. Не каждое выражение имеет нормальную форму.

Тезис Чёрча-Тьюринга

В 1936 году Чёрч и Тьюринг независимо пришли к одному и тому же выводу разными путями. Чёрч формализовал вычислимость через lambda-исчисление. Тьюринг - через машины с лентой. Когда они сравнили результаты, классы функций совпали. Это навело на гипотезу, которую невозможно доказать формально.

Тезис не говорит о скорости. Машина Тьюринга может решить задачу за экспоненциальное время, реальный компьютер - за линейное. Вычислимость и вычислительная сложность - разные вопросы.

**Физический тезис Чёрча-Тьюринга** - более сильное и спорное утверждение: любой физический процесс во Вселенной может быть смоделирован машиной Тьюринга. Квантовые вычисления его не опровергают - они меняют сложность, но не класс вычислимых функций.

Эквивалентность вычислительных моделей

Lambda-исчисление и машина Тьюринга описывают одно и то же множество функций. Доказательство эквивалентности - трансляция в обе стороны. Числа Чёрча показывают, как натуральные числа и арифметика возникают из чистых функций без каких-либо примитивов.

**Числа Чёрча** - одна из элегантных конструкций теории вычислений: число n кодируется как функция «применить f ровно n раз». Арифметика возникает из чистой функциональной композиции - без специальных числовых примитивов.

Комбинаторы S, K, I

Хаскелл Карри в 1920-х задал провокационный вопрос: нужны ли переменные вообще? Он показал, что из трёх базовых комбинаторов - S, K, I - выражается любое lambda-выражение. Это комбинаторная логика - lambda-исчисление без переменных.

**SKI-исчисление полно по Тьюрингу** - из двух примитивов S и K вычисляется всё то, что вычисляет МТ. Это минимально возможный универсальный вычислительный базис. Эзотерические языки Unlambda и Iota построены на этом принципе.

Lambda Calculus и вычислимость

• Три конструкции: переменная, абстракция (λx. e), аппликация (e₁ e₂)
• Beta-редукция: (λx. e₁) e₂ → e₁[x := e₂] - подстановка аргумента в тело
• Тезис Чёрча-Тьюринга: все разумные модели вычислений эквивалентны по мощности
• Числа Чёрча: натуральные числа как функции высшего порядка n = λf.λx. f^n(x)
• Комбинаторы S, K, I: lambda-исчисление без переменных, полное по Тьюрингу
• Y-комбинатор: рекурсия через неподвижную точку без именования функций

Связанные темы

Lambda-исчисление связывает теорию вычислимости с функциональным программированием и математической логикой.

• Машина Тьюринга — Эквивалентная модель вычислений
• Recursive Functions и mu-recursion — Третья эквивалентная формализация вычислимости
• Проблема останова — Омега-комбинатор - аналог незавершающейся программы

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

• Почему Y-комбинатор позволяет выражать рекурсию в системе, где функции не имеют имён?
• Чем числа Чёрча концептуально отличаются от чисел в обычных языках программирования?
• Если S и K достаточно для любых вычислений, зачем в языках программирования переменные и имена?

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

• fl-20-church-turing