Перегляд вихідного коду сторінки Рерайтинг (математика)

{{otheruses|Рерайтинг (медіа)}}
У [[математика|математиці]], [[інформатика|комп'ютерній науці]] та в [[логіка|логіці]] термін '''рерайтинг''' ({{lang-en|rewriting}}) означає широкий діапазон способів (потенційно [[Детермінованість|не детермінованих]]) заміни елементів формули таким чином, що зміст не міняється.

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

Рерайтинг може бути не[[Недетермінований алгоритм|детермінованим]]. Одне правило рерайтинга терму може застосовуватися багатьма різними способами до цього терму, або може бути застосовано більше одного правила. Тоді системи рерайтинга не забезпечують [[алгоритм]] зміни одного терму на інший, але забезпечують набір можливих правил програми. Проте у поєднанні з відповідним алгоритмом системи рерайтинга можуть розглядатися як [[Комп'ютерна програма|комп'ютерні програми]], на рерайтингу термів засновано декілька систем [[Автоматизоване доведення теорем|доведення теорем]]<ref>Hsiang, Jieh, et al. "[http://www.sciencedirect.com/science/article/pii/0743106692900477 The term rewriting approach to automated theorem proving]." The Journal of Logic Programming 14.1-2 (1992): 71-99.</ref> та [[Декларативне програмування|декларативних мов програмування]].<ref>Frühwirth, Thom. "[http://www.sciencedirect.com/science/article/pii/S0743106698100055 Theory and practice of constraint handling rules.]" The Journal of Logic Programming 37.1 (1998): 95-138.</ref><ref>Clavel, Manuel, et al. "[http://www.sciencedirect.com/science/article/pii/S0304397501003590 Maude: Specification and programming in rewriting logic.]" Theoretical Computer Science 285.2 (2002): 187-243.</ref>

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

==== Логіка ====
У [[Логіка висловлювань|логіці]], процедура одержання формули [[Кон'юнктивна нормальна форма|кон'юнктивної нормальної форми]] (КНФ) може бути зручно написана за допомогою системи рерайтинга.<ref name="MarriottStuckey1998">{{cite book|author1=Kim Marriott|author2=Peter J. Stuckey|title=Programming with Constraints: An Introduction|url=https://books.google.com/books?id=jBYAleHTldsC&pg=PA436&dq=%22conjunctive+normal+form%22+(%22(rewrite+OR+rewriting)+(system+OR+engine)%22+OR+%22term+rewriting%22)+-wikipedia&hl=en&sa=X&ved=0ahUKEwjojLmWzrjVAhXF6iYKHbmgDPEQ6AEIKDAA#v=onepage&q=%22conjunctive%20normal%20form%22%20(%22(rewrite%20OR%20rewriting)%20(system%20OR%20engine)%22%20OR%20%22term%20rewriting%22)%20-wikipedia&f=false|year=1998|publisher=MIT Press|isbn=978-0-262-13341-8|pages=436–}}</ref> Правила такої системи будуть:
: <math>\neg\neg A \to A</math> ([[Подвійне заперечення]])
: <math>\neg(A \land B) \to \neg A \lor \neg B</math> ([[Закон де Моргана]])
: <math>\neg(A \lor B)  \to \neg A \land\neg B</math>
: <math> (A \land B) \lor C \to (A \lor C) \land (B \lor C)</math> ([[Дистрибутивність|Дістрибутивність]])
: <math> A \lor (B \land C) \to (A \lor B) \land (A \lor C)</math>,
де символ (<math>\to</math>) вказує на те, що зміст лівої частини може бути поданий як рерайтинг у правій частині.

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

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

====Абстрактні системи рерайтинга ====
З наведених вище прикладів зрозуміло, що ми можемо думати про переписування систем абстрактно. Потрібно вказати набір об'єктів та правила, які можуть бути застосовані для їх перетворення. Найбільш загальна (однозначна) установка цього поняття називається '''абстрактною системою скорочення''' (англ. '''ARS'''), хоча останнім часом автори використовують '''абстрактну систему рерайтинга.'''<ref name=":0">Bezem et al., p. 7,</ref>

ARS&nbsp;— це просто набір A, елементи якого називаються об'єктами та разом з бінарним відношенням на A, традиційно позначаються →, і називаються '''відношенням зменшення''', '''відношенням рерайтинга'''<ref name=":0"/> або просто '''зменшення'''м.<ref>Book and Otto, p. 10</ref>

'''Приклад'''. Припустимо, що набір об'єктів T = {a, b, c} і бінарне співвідношення задано правилами a → b, b → a, a → c, і b → c. Зауважте, що ці правила можуть бути застосовані як до a, так і до b, щоб отримати терм c. Така властивість явно важлива. Зауважте також, що c є, в певному сенсі, «найпростішим» термом у системі, оскільки нічого не може бути застосовано до c, щоб перетворити його далі. Цей приклад веде нас до визначення деяких важливих понять у загальному налаштуванні ARS.<ref>Baader and Nipkow, pp. 8-9</ref>
* <math>\stackrel{*}{\rightarrow}</math> це [[транзитивне замикання]] <math>\rightarrow \cup =</math>, де = є [[відношення рівності]], тобто <math>\stackrel{*}{\rightarrow}</math> є найменшим [[Передпорядок|передпорядком]] ([[Рефлексивне відношення|рефлексивним]] і [[Транзитивне відношення|транзитивним]] відношенням), що містить <math>\rightarrow</math>. Його також називають рефлексивним транзитивним замиканням <math>\rightarrow</math>.
* <math>\leftrightarrow</math> це <math>\rightarrow \cup \ \xrightarrow{-1}</math>, що є об'єднанням співвідношення <math>\rightarrow</math> з його [[Обернене відношення|зворотним співвідношенням]], також відомим як [[симетричне замикання]] <math>\rightarrow</math>.
* <math>\stackrel{*}{\leftrightarrow}</math> це [[транзитивне замикання]] <math>\leftrightarrow \cup =</math>, де <math>\stackrel{*}{\leftrightarrow}</math> є найменшим [[Відношення еквівалентності|відношенням еквівалентності]], що містить <math>\rightarrow</math>. Він також відомий як рефлексивне транзитивне симетричне замикання <math>\rightarrow</math>.

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

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

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

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

Проблема слів для системи semi-Thue  в цілому нерозв'язна; цей результат іноді називають '''теоремою Пост-Маркова'''.<ref>Martin Davis et al. 1994, p. 178</ref>

==== Системи рерайтингу термів ====
'''Система рерайтингу термів''' (TRS)&nbsp;— це система рерайтингу, де об'єктами є [[Терм (логіка)|терми]] або вирази з вкладеними підвиразами. Наприклад, система, показана у розділі [[Рерайтинг#Логіка|Логіка]] вище, є системою рерайтингу термів. Умови в цій системі складаються з бінарних операторів <math>(\vee)</math> і <math>(\wedge)</math> і універсального оператора <math>(\neg)</math>. Також у правилах є змінні, кожна з яких представляє будь-який можливий терм (хоча одна змінна завжди представляє один і той же терм в одному правилі).

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

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

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

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

== Подальше читання ==
* Marc Bezem, Jan Willem Klop, Roel de Vrijer ("Terese"), ''Term Rewriting Systems'' ("TeReSe"), Cambridge University Press, 2003, <nowiki>ISBN 0-521-39115-6</nowiki>.
* Nachum Dershowitz and Jean-Pierre Jouannaud [http://citeseer.ist.psu.edu/dershowitz90rewrite.html "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, <nowiki>ISBN 0-444-88074-7</nowiki>, pp. 243–320. 
* Nachum Dershowitz and David Plaisted. [http://www.cs.tau.ac.il/~nachum/papers/hand-final.pdf "Rewriting"], Chapter 9 in John Alan Robinson and Andrei Voronkov (Eds.), ''Handbook of Automated Reasoning, Volume 1''.
* Gérard Huet et Derek Oppen, [http://infolab.stanford.edu/pub/cstr/reports/cs/tr/80/785/CS-TR-80-785.pdf 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. [http://rewriting.loria.fr/documents/plaisted.ps.gz "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, <nowiki>ISBN 0-12-206382-1</nowiki>.

== Примітки ==
{{reflist|2}}


{{Логіка-доробити}}
{{Інформатика-доробити}}
{{Математика-доробити}}
{{Refimprove|дата=грудень 2017}}
{{ВП-портали|Програмування|Математика}}

[[Категорія:Формальна логіка]]
[[Категорія:Математична логіка]]
[[Категорія:Формальні мови]]
[[Категорія:Логіка в інформатиці]]