Insight

Боже мой! Неужели ординал функции это просто лексикографический порядок на бесхвостых* конфигурациях сети взаимодействия, реализующей функцию?

Upd: Поясню. Существует эквивалентный машинам Тьюринга, лямбда-исчислению, алгорифмам Маркова и т.д. способ формализации алгоритмов: через правила редукции (rewriting rules) на графах. Данные = помеченные графы определённого типа, называемые конфигурациями сети взаимодействия, переходы = редукции. Алгоритм завершается тогда и только тогда, когда никаких правил редукции к конфигурации уже нельзя применить. Доказать, что алгоритм завершается = найти фундированный порядок на конфигурациях, такой, что все правила редукции строго уменьшают конфигурацию.

В явном виде такой порядок можно получить только задав семейство конфигураций при помощи свободного набора правил порождения (т. е. задав его /семейство/ как (обобщённый) индуктивный тип данных). Порядок индуцированный правилами порождения называется лексикографическим.

Для примера можно взять складывающую сеть из http://www.pps.univ-paris-diderot.fr/~danos/dcm07/pdf/mackie.pdf, стр. 3. Там бесхвостые конфигурации соответствуют словам нехитрого регулярного языка [ASZ]* с лексикографическим порядком 3·ω = ω, а правила строго уменьшают бесхвостую часть конфигурации в лексикографическом смысле.

_____
Бесхвостая конфигурация = такая, где свободные переменные не присоеденены к главным портам.


______
Сигнатура Nat = {Zero: Nat, Succ(n: Nat): Nat}

Складывающая система взаимодействий:
— Сигнатура: Nat ++ {Sub(n: Nat, m: Nat): Nat}
— Правила:
—— Sub(n, n) = Zero
—— Sub(Succ(n), m) = Succ(Sub(n, m))

Правило перевода терма с функцией сложения в конфигурацию умножающей сети:
Add(a, b) := find(r) {Sub(r, a) = b}

Утверждение, что Add — тотальная функция соответствует утверждению, что у {Sub(r, a) = b} есть головная нормальная форма.