Системы переписывания термов.Завершаемость

Системы переписывания термов. Завершаемость Теория формальных языков 2021 г. ▲ 1 / 21 Основные понятия Определение Сигнатура — множество пар ⟨f, n⟩ из имени конструктора f и его местности n. Нульместные конструкторы выполняют роль констант. Определение Пусть V — множество переменных, F — множество конструкторов; множество термов T (F) над F определяется рекурсивно: все элементы V — термы; если ⟨f, n⟩ — конструктор и t1 ,. . . , tn — термы, то f(t1 , . . . , tn ) — терм; других термов нет. ▲ 2 / 21 Системы переписывания термов TRS Пусть V — множество переменных, F — множество конструкторов (сигнатура); T (F) — множество термов над множеством конструкторов F. TRS — набор правил переписывания вида ⟨Φi → Ψi ⟩, где Φi , Ψi — термы в T (F). Правило переписывания Φi → Ψi применимо к терму t, если t содержит подтерм, который можно сопоставить с Φi . Если к терму t не применимо ни одно правило переписывания TRS, терм называется нормализованным. ▲ 3 / 21 Конфлюэнтность Определение TRS называется конфлюэнтной, если для любых двух термов t, s, которые получаются переписыванием одного и того же терма u, существует терм v такой, что t, s оба переписываются в v. Формально: ∀u, t, s(u →∗ t & u →∗ s ⇒ ∃v(t →∗ v & s →∗ v)) Конфлюэнтные системы поддаются распараллеливанию и легко оптимизируются. → — переписывание за 1 шаг; →∗ — переписывание за произвольное число шагов, начиная с 0. ▲ 4 / 21 Особенности TRS Недетерминированные. Нет ограничений на порядок применения правил. Не обязательно конфлюэнтны. Могут порождать бесконечные цепочки. ▲ 5 / 21 Особенности TRS Недетерминированные. Нет ограничений на порядок применения правил. Не обязательно конфлюэнтны. Могут порождать бесконечные цепочки. Пример Хетта f(x, x) → a f(x, g(x)) → b c → g(c) Терм, где нарушается конфлюэнтность? ▲ 5 / 21 Особенности TRS Недетерминированные. Нет ограничений на порядок применения правил. Не обязательно конфлюэнтны. Могут порождать бесконечные цепочки. Пример Клопа A → CA Cz → Dz(Cz) Dzz → E Способы преобразовать A? ▲ 5 / 21 Особенности TRS Недетерминированные. Нет ограничений на порядок применения правил. Не обязательно конфлюэнтны. Могут порождать бесконечные цепочки. Пример Тойямы TRS 1: f(0, 1, x) → f(x, x, x) TRS 2: g(x, y) → x g(x, y) → y Как можно вычислить f(g(0, 1), g(0, 1), g(0, 1))? ▲ 5 / 21 Фундированность Определение Частичный порядок ⪯ является фундированным (wfo) на множестве M, если в M не существует бесконечных нисходящих цепочек относительно ⪯. Частичный порядок ⪯ является монотонным в алгебре A, если ∀f, t1 , ..., tn , s, s ′ (s ⪯ s ′ ⇒ f(t1 , . . . , s, . . . , tn ) ⪯ f(t1 , . . . , s ′ , . . . , tn )) (строго монотонным, если при этом неверно обратное). ▲ 6 / 21 Завершаемость Определение Фундированная монотонная алгебра (ФуМА) над множеством функциональных символов F — это фундированное множество ⟨A, >⟩ такое, что для каждого функционального символа f ∈ F существует функция fA : An → A, строго монотонная по каждому из аргументов. Определим расширение произвольного отображения σ из множества переменных в A следующим образом: [x, σ] = σ(x); [f(t1 , . . . , tn ), σ] = fA ([t1 , σ], . . . , [tn , σ]). ▲ 7 / 21 Завершаемость Совместность TRS {li → ri } совместна с ФуМА A ⇔ для всех i и для всех σ выполняется условие [li , σ] > [ri , σ]. Теорема TRS не порождает бесконечных вычислений (завершается), если и только если существует совместная с ней ФуМА. ▲ 8 / 21 ФуМА, совместные с TRS Стандартные способы определения fA : лексикографический порядок на множестве имён F + отношение подтерма; построение монотонно возрастающей (по каждому аргументу) числовой функции, соответствующей fA . Оба случая подразумевают, что в построенной модели целое больше части, т.е. всегда выполняется f(t) > t. ▲ 9 / 21 Лексикографический порядок > lo Определение f(t1 , . . . , tn ) >lo g(u1 , . . . , um ) если и только если выполнено одно из условий: 1 ∃i(1 ⩽ i ⩽ n & ti = g(u1 , . . . , um )); 2 ∃i(1 ⩽ i ⩽ n & ti >lo g(u1 , . . . , um )); 3 (f > g) & ∀i(1 ⩽ i ⩽ m ⇒ f(t1 , . . . , tn ) >lo ui ); 4 (f = g) & ∀i(1 ⩽ i ⩽ n ⇒ f(t1 , . . . , tn ) >lo ui ) и n-ка (t1 , . . . , tn ) лексикографически больше, чем (u1 , . . . , un ) (т.е. первый её не совпадающий с ui элемент ti удовлетворяет условию ti >lo ui ). ▲ 10 / 21 Примеры Проверить завершаемость TRS методом >lo : f(g(x)) → g(h(x, x)) g(f(x)) → h(g(x), x) Первое правило переписывания вынуждает либо g(x) >lo g(h(x, x)) (по условию 1 или 2) — что невозможно, потому что x должно лексикографически оказаться больше h(x, x) (по условию 4); либо f > g и f(g(x)) > h(x, x) (по условию 3). В этом случае можно взять также f > h. Неравенство f(g(x)) > x выполняется тривиально. Второе правило переписывания удовлетворяет условию завершаемости по условию 2, например, если показать, что f(x) >lo h(g(x), x). Уже имеем f > h, поэтому достаточно показать f(x) >lo g(x) и f(x) >lo x. Оба условия тривиально выполняются из допущений выше. ▲ 11 / 21 Примеры Проверить завершаемость TRS методом построения монотонной функции: f(g(x, y)) → g(h(y), x) h(f(x)) → f(x). Завершаемость по второму правилу переписывания автоматически выполняется по свойству подтерма. Поэтому то, что функция f стоит на двух его сторонах, не дает никаких указаний относительно того, стоит ли делать fA быстро растущей или медленно. Все подсказки содержатся только в первом правиле переписывания. По первому правилу переписывания видно, что fA надо делать большой (f стоит только слева), а h нет (h есть только справа). Положим fA (x) = 10 ∗ (x + 1), hA (x) = x + 1. Тогда должно выполняться 10 ∗ (gA (x, y) + 1) > g(y + 1, x). Этому неравенству удовлетворяет, например, gA (x, y) = x + y. 12 / 21 ▲ Общие комментарии Не обязательно добиваться выполнения неравенства на образах fA на всём множестве N. Поскольку любой отрезок N от k и до бесконечности фундирован, а все образы fA монотонны, они замкнуты на этом отрезке. Поэтому, если неравенство не выполняется для нескольких первых чисел натурального ряда, этим можно пренебречь. Если не получается применить >lo или подобрать числовую функцию, это ещё не значит, что TRS не завершается. См. пример Зантемы: f(g(x)) → g(f(f(x))). ▲ 13 / 21 Ординалы Определение Рассмотрим множество M с определенным на нем полным (линейным, фундированным) порядком <. Ординал τ — это порядок множества ⟨M, <⟩ (иногда в виде τ рассматривается само это множество). Если существует биекция f из ⟨M, <⟩ в ⟨M ′ , < ′ ⟩, являющаяся гомоморфизмом, то M и M ′ имеют одинаковые порядки. Ординал любого множества {1, 2, ..., k}, где k ∈ N — это k. Ординал N — это ω. ▲ 14 / 21 Математика мыльных пузырей Фон-Неймановское представление ординалов: ^0 = ∅ ^1 = {∅} ^2 = {∅, {∅}} ... ^ 1 = {^0, ^1, . . . , k} ^ k+ ▲ 15 / 21 Предельные ординалы Определение Ординал τ предельный, если не существует τ0 такого, что τ = τ0 + 1. Существование предельных ординалов делает ординальную арифметику некоммутативной, поскольку правый элемент сложения и умножения может поглощать левый. ▲ 16 / 21 Ординальная арифметика Сложение: α + 0 = α; α + (β + 1) = (α + β) + 1; β — предельный ⇒ α + β = limγ<β (α + γ). Умножение: α ∗ 0 = 0; α ∗ (β + 1) = (α ∗ β) + α; β — предельный ⇒ α ∗ β = limγ<β (α ∗ γ). Экспоненциация: α0 = 1; α(β+1) = (αβ ) ∗ α; β — предельный ⇒ αβ = limγ<β (αγ ). Дистрибутивность только левая: α ∗ (β + γ) = α ∗ β + α ∗ γ. ▲ 17 / 21 Трансфинитная индукция Если T (0) и для выполнено ∀β(β < α ⇒ T (β)) ⇒ T (α), тогда ∀α(T (α)). Выбор множества ординалов в качестве ФуМА — лёгкий способ доказывать завершаемость TRS. Не надо подбирать точные значения коэффициентов. Существенно расширяется класс TRS, для которых можно проверить завершаемость методом построения ФуМА. ▲ 18 / 21 Функция Аккермана Функция, растущая быстрее всех элементарных Ack(0,m) = m+1; Ack(n,0) = Ack(n-1, 1); Ack(n,m) = Ack(n-1, Ack(n, m-1)). Положим fAck (n, m) = ωn+1 + m. Проверим условия завершаемости: ω+m>m+1 ωn+1 > ωn + 1 ωn+1 + m > ωn + ωn+1 + m − 1. Воспользуемся левой дистрибутивностью: ωn + ωn+1 = ωn ∗ (1 + ω). Но 1 + ω = ω, откуда следует неравенство выше. ▲ 19 / 21 Гидра Гудстейна Рассмотрим g(N, k) — экспоненциальное представление числа N в алфавите {1, . . . , k}. Пример: g(11, 2) = 2(2+1) + 2 + 1. Рассмотрим G(N, m), где N записана в виде g(N, m + 1). Формально заменим все m + 1 на m + 2 в этом представлении, а затем вычтем из результата 1. Будем шаг за шагом применять к результату преобразование G, увеличивая m. Утверждение ∀N∃m(G(G(...G(N, 2)...), m) = 0). ▲ 20 / 21 Смертность гидры Гудстейна Сопоставим числу N функцию оценки f(N, m), которая рассматривает g(N, m)-представление числа N и заменяет в нём все числа m на ω. Покажем, что f(N, m) > f(G(N, m + 1) − 1, m + 1). ▲ 21 / 21 Смертность гидры Гудстейна Сопоставим числу N функцию оценки f(N, m), которая рассматривает g(N, m)-представление числа N и заменяет в нём все числа m на ω. Покажем, что f(N, m) > f(G(N, m + 1) − 1, m + 1). Рассмотрим терм G(N, m + 1) до вычитания 1, но после замены всех оснований с m на m + 1. Очевидно, f(N, m) = f(G(N, m + 1), m + 1). После вычитания 1 и построения новой m + 1-экспоненциальной формы происходит переход через предельный ординал в f(G(N, m + 1), m + 1) и замена его некоторым заведомо меньшим (предшествующим) ординалом. Если такой переход не происходит, значит, в f(G(N, m + 1), m + 1) есть слагаемое с основанием ω0 , и тогда f(G(N, m + 1) − 1, m + 1) = f(G(N, m + 1), m + 1) − 1. ▲ 21 / 21