Рерайтинг (математика)

У логіці, процедура одержання формули кон'юнктивної нормальної форми (КНФ) може бути зручно написана за допомогою системи рерайтинга.[4] Правила такої системи будуть:

${\displaystyle \neg \neg A\to A}$ (Подвійне заперечення)

${\displaystyle \neg (A\land B)\to \neg A\lor \neg B}$ (Закон де Моргана)

${\displaystyle \neg (A\lor B)\to \neg A\land \neg B}$

${\displaystyle (A\land B)\lor C\to (A\lor C)\land (B\lor C)}$ (Дістрибутивність)

${\displaystyle A\lor (B\land C)\to (A\lor B)\land (A\lor C)}$,

де символ (${\displaystyle \to }$) вказує на те, що зміст лівої частини може бути поданий як рерайтинг у правій частині.

У лінгвістиці правила рерайтинга, які також називаються правилами фразової структури, використовуються в деяких системах генеративної граматики, як засіб генерування граматично правильних речень мови. Таке правило зазвичай приймає форму A → X, де A є міткою синтаксичної категорії, наприклад, іменником або реченням, а X є послідовністю таких міток або морфем, що виражає той факт, що A може бути замінений на X при генеруванні складової структури речення. Наприклад, правило S → NP VP означає, що пропозиція може складатися з іменника, що супроводжується дієсловом; подальші правила вказують, з яких субкомпонентів можуть складатися іменник та дієслово, і так далі.

З наведених вище прикладів зрозуміло, що ми можемо думати про переписування систем абстрактно. Потрібно вказати набір об'єктів та правила, які можуть бути застосовані для їх перетворення. Найбільш загальна (однозначна) установка цього поняття називається абстрактною системою скорочення (англ. ARS), хоча останнім часом автори використовують абстрактну систему рерайтинга.[5]

ARS — це просто набір A, елементи якого називаються об'єктами та разом з бінарним відношенням на A, традиційно позначаються →, і називаються відношенням зменшення, відношенням рерайтинга[5] або просто зменшенням.[6]

Приклад. Припустимо, що набір об'єктів T = {a, b, c} і бінарне співвідношення задано правилами a → b, b → a, a → c, і b → c. Зауважте, що ці правила можуть бути застосовані як до a, так і до b, щоб отримати терм c. Така властивість явно важлива. Зауважте також, що c є, в певному сенсі, «найпростішим» термом у системі, оскільки нічого не може бути застосовано до c, щоб перетворити його далі. Цей приклад веде нас до визначення деяких важливих понять у загальному налаштуванні ARS.[7]

• ${\displaystyle {\stackrel {*}{\rightarrow }}}$ це транзитивне замикання ${\displaystyle \rightarrow \cup =}$, де = є відношення рівності, тобто ${\displaystyle {\stackrel {*}{\rightarrow }}}$ є найменшим передпорядком (рефлексивним і транзитивним відношенням), що містить ${\displaystyle \rightarrow }$. Його також називають рефлексивним транзитивним замиканням ${\displaystyle \rightarrow }$.
• ${\displaystyle \leftrightarrow }$ це ${\displaystyle \rightarrow \cup \ {\xrightarrow {-1}}}$, що є об'єднанням співвідношення ${\displaystyle \rightarrow }$ з його зворотним співвідношенням, також відомим як симетричне замикання ${\displaystyle \rightarrow }$.
• ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$ це транзитивне замикання ${\displaystyle \leftrightarrow \cup =}$, де ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$ є найменшим відношенням еквівалентності, що містить ${\displaystyle \rightarrow }$. Він також відомий як рефлексивне транзитивне симетричне замикання ${\displaystyle \rightarrow }$.

Рядкова система рерайтинга (англ. SRS), також відома як система semi-Thue, використовує вільну моноїдну структуру рядків (слів) над алфавітом, щоб розширити відношення рерайтинга ${\displaystyle R}$ для всіх рядків у алфавіті, що містять ліву і відповідно праву сторону деяких правил як підрядка. Формально semi-Thue системи це пара ${\displaystyle (\Sigma ,R)}$, де ${\displaystyle \Sigma }$ — (найчастіше кінцевий) алфавіт, а ${\displaystyle R}$ це бінарне відношення між деякими (фіксованими) строками в алфавіті, що називаються правилами рерайтинга. Однокрокове відношення рерайтинга відносини ${\displaystyle {\xrightarrow[{R}]{}}}$ викликаної ${\displaystyle R}$ на ${\displaystyle \Sigma ^{*}}$ визначається так: для будь-яких строк ${\displaystyle s,t\in \Sigma ^{*}}$ ${\displaystyle s{\xrightarrow[{R}]{}}t}$ якщо і тільки якщо є ${\displaystyle x,y,u,v\in \Sigma ^{*}}$ такі, що ${\displaystyle s=xuy}$, ${\displaystyle t=xvy}$, і ${\displaystyle uRv}$. Так як ${\displaystyle {\xrightarrow[{R}]{}}}$ є відношенням на ${\displaystyle \Sigma ^{*}}$, пара ${\displaystyle (\Sigma ^{*},{\xrightarrow[{R}]{}})}$ підходить до визначення абстрактної системи рерайтинга. Очевидно, що ${\displaystyle R}$ є підмножиною з ${\displaystyle {\xrightarrow[{R}]{}}}$. Якщо відношення ${\displaystyle R}$ є симетричним, тоді система називається системою Thue.

У SRS, відношення скорочення ${\displaystyle {\xrightarrow[{R}]{*}}}$ сумісне з моноїдною операцією, що означає, що з ${\displaystyle x{\xrightarrow[{R}]{*}}y}$ витікає ${\displaystyle uxv{\xrightarrow[{R}]{*}}uyv}$ для усіх рядків ${\displaystyle x,y,u,v\in \Sigma ^{*}}$. Аналогічним чином, рефлексивне транзитивне симетричне замикання ${\displaystyle {\xrightarrow[{R}]{}}}$, позначене ${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$, є конгруентність, тобто вона є відношенням еквівалентності (за визначенням), і також сумісна з конкатенацією рядків. Відношення ${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$ називається конгруентністю Thue що породжується з ${\displaystyle R}$. У системі Thue, тобто якщо ${\displaystyle R}$ iє симетричним, переписане відношення ${\displaystyle {\xrightarrow[{R}]{*}}}$ збігається з конгруентністю Thue ${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$.

Поняття системи semi-Thue по суті збігається з представленням моноїда.Так як ${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$ це конгруентність, ми можемо визначити фактор моноїд ${\displaystyle {\mathcal {M}}_{R}=\Sigma ^{*}/{\overset {*}{\underset {R}{\leftrightarrow }}}}$ вільного моноїда ${\displaystyle \Sigma ^{*}}$ за допомогою конгруентністі Thue звичайним чином. Якщо моноїд ${\displaystyle {\mathcal {M}}}$ ізоморфний з ${\displaystyle {\mathcal {M}}_{R}}$, то система semi-Thue ${\displaystyle (\Sigma ,R)}$ називається моноїдним представленням ${\displaystyle {\mathcal {M}}}$.

Ми відразу отримуємо деякі дуже корисні зв'язки з іншими областями алгебри. Наприклад, алфавіт {a, b} з правилами { ab → ε, ba → ε }, де ε це порожній рядок, є представленням вільної групи на одному генераторі. Якщо замість цих правил є лише { ab → ε }, то ми отримуємо уявлення про біциклічний моноїд. Таким чином, системи Thue є природною основою для вирішення проблеми слів для моноїдів та груп. По суті, кожен моноїд має представлення форми ${\displaystyle (\Sigma ,R)}$, тобто він завжди може бути представлен системою semi-Thue, можливо, над нескінченним алфавітом.

Проблема слів для системи semi-Thue в цілому нерозв'язна; цей результат іноді називають теоремою Пост-Маркова.[8]

Система рерайтингу термів (TRS) — це система рерайтингу, де об'єктами є терми або вирази з вкладеними підвиразами. Наприклад, система, показана у розділі Логіка вище, є системою рерайтингу термів. Умови в цій системі складаються з бінарних операторів ${\displaystyle (\vee )}$ і ${\displaystyle (\wedge )}$ і універсального оператора ${\displaystyle (\neg )}$. Також у правилах є змінні, кожна з яких представляє будь-який можливий терм (хоча одна змінна завжди представляє один і той же терм в одному правилі).

На відміну від рядкової системи рерайтингу, об'єктами якої є плоскі послідовності символів, об'єкти, на яких працює система переписування, тобто терми, утворюють алгебру термів. Терм можна візуалізувати як дерево символів, набір прийнятих символів фіксується даним підписом.

Теорія слідів дає змогу обговорювати багатопроцесорність формальними термінами, наприклад, через моноїд сліду та моноїд історії. Рерайтинг можна виконувати і в системах слідів.