Полнота по Тьюрингу

Полнота по Тьюрингу — это наличие конструкций ветвления, повтора и данных. Все ингредиенты уже собраны в предыдущих разделах:

• данные — кодирование Чёрча (раздел «Кодирование Чёрча»): булевы значения, пары, нумералы, списки;
• ветвление — булево значение Чёрча само выбирает ветку: $\mathrm{if}$ $\equiv \lambda b\,t\,e.\,b\,t\,e$;
• циклы — комбинатор неподвижной точки (раздел «Комбинатор Карри»): $\mathrm{Y}\,F$ $=_\beta F\,(\mathrm{Y}\,F)$, рекурсия без имён и без счётчиков.

Этого хватает, чтобы смоделировать машину Тьюринга: лента — список, состояние — нумерал, шаг — ветвление, повторение шагов — $\mathrm{Y}$. У полноты по Тьюрингу есть цена — неразрешимость. Нет алгоритма, который по терму определяет, есть ли у него нормальная форма: это λ-аналог проблемы останова.

Теперь про тотальность. Язык называется тотальным, если каждая его программа завершается на каждом входе. Полнота по Тьюрингу с тотальностью несовместима. В λ-исчислении возможны бесконечные циклы:

Языки, выбравшие тотальность, существуют — например, Agda. Компилятор Agda проверяет каждую функцию: все случаи входа должны быть разобраны, а рекурсивные вызовы — идти по структурно меньшим аргументам. Сложение натуральных чисел проверку проходит — рекурсивный вызов идёт на $n$ — строго меньшую часть $\mathtt{suc}\ n$:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero  + m = m
suc n + m = suc (n + m)   -- вызов на n: строго меньше, чем suc n

А вот это Agda отвергнет:

loop : ℕ → ℕ
loop n = loop n           -- Termination checking failed: n не убывает

Плата симметрична: Agda не Тьюринг-полна — $\Omega$ в ней не написать. Зато каждая программа — тотальная функция, и по соответствию Карри — Ховарда (раздел «Соответствие Карри — Ховарда») её можно читать как доказательство. Haskell выбирает середину: типизированное ядро плюс общая рекурсия ($\mathtt{fix}$, рекурсивный let) — полнота возвращается, а с ней и вечные циклы.