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

У математиці, комп'ютерній науці та в логіці термін рерайтинг (англ. rewriting) означає широкий діапазон способів (потенційно не детермінованих) заміни елементів формули таким чином, що зміст не міняється.

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

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

Інтуїтивні приклади

Логіка

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

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

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

$\neg (A\lor B)\to \neg A\land \neg B$

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

$A\lor (B\land C)\to (A\lor B)\land (A\lor C)$,

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

Лінгвістика

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

Типи систем рерайтинга

Абстрактні системи рерайтинга

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

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

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

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

Рядкові системи рерайтинга

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

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

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

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

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

Системи рерайтингу термів

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

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

Системи рерайтинга слідів

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

Філософія

Системи рерайтинга можуть розглядатися як програми, які виводять кінцеві ефекти зі списку причинно-наслідкових зв'язків. Таким чином, системи рерайтинга можуть розглядатись як системи автоматичного доведення причинності.

Див. також

• Критична пара (логіка)
• Алгоритм завершення Knuth-Bendix
• L-системи вказують на перезапис, який виконується паралельно.
• Прозорість посилань в галузі інформатики
• Регульований рерайтинг
• Rho calculus

Подальше читання

• Marc Bezem, Jan Willem Klop, Roel de Vrijer ("Terese"), Term Rewriting Systems ("TeReSe"), Cambridge University Press, 2003, ISBN 0-521-39115-6.
• Nachum Dershowitz and Jean-Pierre Jouannaud "Rewrite Systems", Chapter 6 in Jan van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics., Elsevier and MIT Press, 1990, ISBN 0-444-88074-7, pp. 243–320.
• Nachum Dershowitz and David Plaisted. "Rewriting", Chapter 9 in John Alan Robinson and Andrei Voronkov (Eds.), Handbook of Automated Reasoning, Volume 1.
• Gérard Huet et Derek Oppen, Equations and Rewrite Rules, A Survey (1980) Stanford Verification Group, Report N° 15 Computer Science Department Report N° STAN-CS-80-785
• Jan Willem Klop. "Term Rewriting Systems", Chapter 1 in Samson Abramsky, Dov M. Gabbay and Tom Maibaum (Eds.), Handbook of Logic in Computer Science, Volume 2: Background: Computational Structures.
• David Plaisted. "Equational reasoning and term rewriting systems", in Dov M. Gabbay, C. J. Hogger and John Alan Robinson (Eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 1.
• Jürgen Avenhaus and Klaus Madlener. "Term rewriting and equational reasoning". In Ranan B. Banerji (Ed.), Formal Techniques in Artificial Intelligence: A Sourcebook, Elsevier (1990).

Рерайтинг рядків

• Ronald V. Book and Friedrich Otto, String-Rewriting Systems, Springer (1993).
• Benjamin Benninghofen, Susanne Kemmerich and Michael M. Richter, Systems of Reductions. LNCS 277, Springer-Verlag (1987).

Інші

• Martin Davis, Ron Sigal, Elaine J. Weyuker, (1994) Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science – 2nd edition, Academic Press, ISBN 0-12-206382-1.