Вычислимость
Вычислительные модели: Lambda-исчисление и комбинаторы
Haskell, Clojure, Scala, Erlang - все функциональные языки основаны на идеях, которым почти 100 лет. Lambda-исчисление Чёрча 1936 года - математическая основа каждого map, filter, reduce. Понять λ-calculus значит понять само вычисление.
- Haskell, ML, OCaml - прямые реализации λ-calculus
- JavaScript: стрелочные функции = λ-абстракции
- React hooks основаны на замыканиях (λ-абстракции)
- Компиляторы: Core в GHC = расширенный λ-calculus
Lambda-исчисление: вычисления без данных
**Lambda-исчисление** (λ-calculus) - минимальная формальная система для вычислений, изобретённая Чёрчем в 1930-х. Содержит только три конструкции: переменная, абстракция (λx.M), применение (M N).
**Тезис Чёрча-Тьюринга:** λ-calculus и Машина Тьюринга вычислительно эквивалентны. Любое вычисление, выразимое на одной, выразимо и на другой. Это самое фундаментальное утверждение в теории вычислений.
Что вычислит (λx. λy. y) a b?
Кодирование Чёрча: числа из функций
**Числа Чёрча** - кодирование натуральных чисел в λ-calculus. Число n представляется как применение функции n раз. Это демонстрирует, что λ-calculus Turing-complete без встроенных типов данных.
**Predecessor - нетривиальная задача:** Вычисление предшествующего числа (n-1) в λ-calculus - это не закономерно. Клини потребовалось время, чтобы найти решение. Это показывает, что несмотря на Turing-completeness, некоторые вычисления в λ-calculus требуют изобретательности.
Число Чёрча n представляет n как:
Комбинаторы S, K, I
**Комбинаторная логика** - система без переменных, только комбинаторы. Шёнфинкель (1920) и Карри показали, что двух комбинаторов S и K достаточно для всех вычислений.
**Unlambda:** Существует esoteric язык программирования Unlambda, основанный только на S, K, I. Любой алгоритм выразим в нём. Это доказательство полноты комбинаторной логики на практике.
Комбинаторы S, K, I - это математическая курьёзность без практической пользы. Реальные программы пишутся на ассемблере, C, Python, а не на двух буквах.
SKI-комбинаторы Тьюринг-полны и лежат в основе бесточечного стиля (point-free) в Haskell, лямбда-лифтинга в компиляторах, supercombinators в STG-машине GHC. Каждое замыкание в функциональном языке внутри транслируется через комбинаторы.
Внешняя простота записи путает с практической ничтожностью. На деле SKI - это нормальная форма для абстрактной машины: GHC при компиляции лямбд проводит lambda lifting, превращая локальные функции в supercombinators, потому что без замыканий легче оптимизировать. Программа на двух буквах не пишется руками, но компилируется в неё.
Чему равно K x y в комбинаторной логике?
Ключевые идеи
- λ-calculus: три конструкции (переменная, абстракция, применение) - Turing-complete
- β-редукция: вычисление = подстановка аргумента
- Числа Чёрча: натуральные числа как n-кратные применения функции
- Комбинаторы S, K: достаточно для всех вычислений без переменных
- Тезис Чёрча-Тьюринга: λ-calculus ≡ Машина Тьюринга
Связанные темы
Lambda-исчисление - теоретическая основа функциональных языков.
- Машина Тьюринга — Эквивалентность по тезису Чёрча-Тьюринга
- Практика вычислимости — Системы типов и λ-calculus связаны
Вопросы для размышления
- Можете ли вы реализовать рекурсию в λ-calculus, если у функций нет имён? (Подсказка: Y-комбинатор)
- Почему в Simply Typed Lambda Calculus все программы завершаются? Что теряется при добавлении типов?
- Каково практическое значение того, что функциональные языки основаны на λ-calculus?
Связанные уроки
- comp-01 — Машина Тьюринга - отправная точка для сравнения с lambda-исчислением
- comp-07 — Теория автоматов показывает более слабые модели вычислений
- comp-15 — Колмогоровская сложность строится на понятии вычислимой функции
- alg-01-big-o — Lambda-редукция и асимптотика: разные языки для одной идеи вычислительных ресурсов
- fl-18-turing-machine