У математиці, комп'ютерній науці та в логіці термін рерайтинг (англ. rewriting) означає широкий діапазон способів (потенційно не детермінованих) заміни елементів формули таким чином, що зміст не міняється.
У самому базовому вигляді системи рерайтинга складаються з набору об'єктів, плюс відносин про те, як перетворити ці об'єкти.
Рерайтинг може бути недетермінованим. Одне правило рерайтинга терму може застосовуватися багатьма різними способами до цього терму, або може бути застосовано більше одного правила. Тоді системи рерайтинга не забезпечують алгоритм зміни одного терму на інший, але забезпечують набір можливих правил програми. Проте у поєднанні з відповідним алгоритмом системи рерайтинга можуть розглядатися як комп'ютерні програми, на рерайтингу термів засновано декілька систем доведення теорем та декларативних мов програмування.
Інтуїтивні приклади
Логіка
У логіці, процедура одержання формули кон'юнктивної нормальної форми (КНФ) може бути зручно написана за допомогою системи рерайтинга. Правила такої системи будуть:
де символ () вказує на те, що зміст лівої частини може бути поданий як рерайтинг у правій частині.
Лінгвістика
У лінгвістиці правила рерайтинга, які також називаються правилами фразової структури, використовуються в деяких системах генеративної граматики, як засіб генерування граматично правильних речень мови. Таке правило зазвичай приймає форму 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.
- це транзитивне замикання , де = є відношення рівності, тобто є найменшим передпорядком (рефлексивним і транзитивним відношенням), що містить . Його також називають рефлексивним транзитивним замиканням .
- це , що є об'єднанням співвідношення з його зворотним співвідношенням, також відомим як .
- це транзитивне замикання , де є найменшим відношенням еквівалентності, що містить . Він також відомий як рефлексивне транзитивне симетричне замикання .
Рядкові системи рерайтинга
Рядкова система рерайтинга (англ. SRS), також відома як система semi-Thue, використовує вільну моноїдну структуру рядків (слів) над алфавітом, щоб розширити відношення рерайтинга для всіх рядків у алфавіті, що містять ліву і відповідно праву сторону деяких правил як підрядка. Формально semi-Thue системи це пара , де — (найчастіше кінцевий) алфавіт, а це бінарне відношення між деякими (фіксованими) строками в алфавіті, що називаються правилами рерайтинга. Однокрокове відношення рерайтинга відносини викликаної на визначається так: для будь-яких строк якщо і тільки якщо є такі, що , , і . Так як є відношенням на , пара підходить до визначення абстрактної системи рерайтинга. Очевидно, що є підмножиною з . Якщо відношення є симетричним, тоді система називається системою Thue.
У SRS, відношення скорочення сумісне з моноїдною операцією, що означає, що з витікає для усіх рядків . Аналогічним чином, рефлексивне транзитивне симетричне замикання , позначене , є конгруентність, тобто вона є відношенням еквівалентності (за визначенням), і також сумісна з конкатенацією рядків. Відношення називається конгруентністю Thue що породжується з . У системі Thue, тобто якщо іє симетричним, переписане відношення збігається з конгруентністю Thue .
Поняття системи semi-Thue по суті збігається з представленням моноїда.Так як це конгруентність, ми можемо визначити фактор моноїд вільного моноїда за допомогою конгруентністі Thue звичайним чином. Якщо моноїд ізоморфний з , то система semi-Thue називається моноїдним представленням .
Ми відразу отримуємо деякі дуже корисні зв'язки з іншими областями алгебри. Наприклад, алфавіт {a, b} з правилами { ab → ε, ba → ε }, де ε це порожній рядок, є представленням вільної групи на одному генераторі. Якщо замість цих правил є лише { ab → ε }, то ми отримуємо уявлення про біциклічний моноїд. Таким чином, системи Thue є природною основою для вирішення проблеми слів для моноїдів та груп. По суті, кожен моноїд має представлення форми , тобто він завжди може бути представлен системою semi-Thue, можливо, над нескінченним алфавітом.
Проблема слів для системи semi-Thue в цілому нерозв'язна; цей результат іноді називають теоремою Пост-Маркова.
Системи рерайтингу термів
Система рерайтингу термів (TRS) — це система рерайтингу, де об'єктами є терми або вирази з вкладеними підвиразами. Наприклад, система, показана у розділі (Логіка) вище, є системою рерайтингу термів. Умови в цій системі складаються з бінарних операторів і і універсального оператора . Також у правилах є змінні, кожна з яких представляє будь-який можливий терм (хоча одна змінна завжди представляє один і той же терм в одному правилі).
На відміну від рядкової системи рерайтингу, об'єктами якої є плоскі послідовності символів, об'єкти, на яких працює система переписування, тобто терми, утворюють алгебру термів. Терм можна візуалізувати як дерево символів, набір прийнятих символів фіксується даним підписом.
Системи рерайтинга слідів
Теорія слідів дає змогу обговорювати багатопроцесорність формальними термінами, наприклад, через моноїд сліду та моноїд історії. Рерайтинг можна виконувати і в системах слідів.
Філософія
Системи рерайтинга можуть розглядатися як програми, які виводять кінцеві ефекти зі списку причинно-наслідкових зв'язків. Таким чином, системи рерайтинга можуть розглядатись як системи автоматичного доведення причинності.
Див. також
- вказують на перезапис, який виконується паралельно.
- Прозорість посилань в галузі інформатики
Подальше читання
- 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.
Примітки
- Hsiang, Jieh, et al. "The term rewriting approach to automated theorem proving." The Journal of Logic Programming 14.1-2 (1992): 71-99.
- Frühwirth, Thom. "Theory and practice of constraint handling rules." The Journal of Logic Programming 37.1 (1998): 95-138.
- Clavel, Manuel, et al. "Maude: Specification and programming in rewriting logic." Theoretical Computer Science 285.2 (2002): 187-243.
- Kim Marriott; Peter J. Stuckey (1998). Programming with Constraints: An Introduction. MIT Press. с. 436–. ISBN .
- Bezem et al., p. 7,
- Book and Otto, p. 10
- Baader and Nipkow, pp. 8-9
- Martin Davis et al. 1994, p. 178
Це незавершена стаття з логіки. Ви можете проєкту, виправивши або дописавши її. |
Це незавершена стаття з інформатики. Ви можете проєкту, виправивши або дописавши її. |
Це незавершена стаття з математики. Ви можете проєкту, виправивши або дописавши її. |
Ця стаття потребує додаткових для поліпшення її . (грудень 2017) |
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
U Vikipediyi ye statti pro inshi znachennya cogo termina Rerajting media U matematici komp yuternij nauci ta v logici termin rerajting angl rewriting oznachaye shirokij diapazon sposobiv potencijno ne determinovanih zamini elementiv formuli takim chinom sho zmist ne minyayetsya U samomu bazovomu viglyadi sistemi rerajtinga skladayutsya z naboru ob yektiv plyus vidnosin pro te yak peretvoriti ci ob yekti Rerajting mozhe buti nedeterminovanim Odne pravilo rerajtinga termu mozhe zastosovuvatisya bagatma riznimi sposobami do cogo termu abo mozhe buti zastosovano bilshe odnogo pravila Todi sistemi rerajtinga ne zabezpechuyut algoritm zmini odnogo termu na inshij ale zabezpechuyut nabir mozhlivih pravil programi Prote u poyednanni z vidpovidnim algoritmom sistemi rerajtinga mozhut rozglyadatisya yak komp yuterni programi na rerajtingu termiv zasnovano dekilka sistem dovedennya teorem ta deklarativnih mov programuvannya Intuyitivni prikladiLogika U logici procedura oderzhannya formuli kon yunktivnoyi normalnoyi formi KNF mozhe buti zruchno napisana za dopomogoyu sistemi rerajtinga Pravila takoyi sistemi budut A A displaystyle neg neg A to A Podvijne zaperechennya A B A B displaystyle neg A land B to neg A lor neg B Zakon de Morgana A B A B displaystyle neg A lor B to neg A land neg B A B C A C B C displaystyle A land B lor C to A lor C land B lor C Distributivnist A B C A B A C displaystyle A lor B land C to A lor B land A lor C de simvol displaystyle to vkazuye na te sho zmist livoyi chastini mozhe buti podanij yak rerajting u pravij chastini Lingvistika U lingvistici pravila rerajtinga yaki takozh nazivayutsya pravilami frazovoyi strukturi vikoristovuyutsya v deyakih sistemah generativnoyi gramatiki yak zasib generuvannya gramatichno pravilnih rechen movi Take pravilo zazvichaj prijmaye formu A X de A ye mitkoyu sintaksichnoyi kategoriyi napriklad imennikom abo rechennyam a X ye poslidovnistyu takih mitok abo morfem sho virazhaye toj fakt sho A mozhe buti zaminenij na X pri generuvanni skladovoyi strukturi rechennya Napriklad pravilo S NP VP oznachaye sho propoziciya mozhe skladatisya z imennika sho suprovodzhuyetsya diyeslovom podalshi pravila vkazuyut z yakih subkomponentiv mozhut skladatisya imennik ta diyeslovo i tak dali Tipi sistem rerajtingaAbstraktni sistemi rerajtinga Z navedenih vishe prikladiv zrozumilo sho mi mozhemo dumati pro perepisuvannya sistem abstraktno Potribno vkazati nabir ob yektiv ta pravila yaki mozhut buti zastosovani dlya yih peretvorennya Najbilsh zagalna odnoznachna ustanovka cogo ponyattya nazivayetsya abstraktnoyu sistemoyu skorochennya angl ARS hocha ostannim chasom avtori vikoristovuyut abstraktnu sistemu rerajtinga ARS ce prosto nabir A elementi yakogo nazivayutsya ob yektami ta razom z binarnim vidnoshennyam na A tradicijno poznachayutsya i nazivayutsya vidnoshennyam zmenshennya vidnoshennyam rerajtinga abo prosto zmenshennyam Priklad Pripustimo sho nabir ob yektiv T a b c i binarne spivvidnoshennya zadano pravilami a b b a a c i b c Zauvazhte sho ci pravila mozhut buti zastosovani yak do a tak i do b shob otrimati term c Taka vlastivist yavno vazhliva Zauvazhte takozh sho c ye v pevnomu sensi najprostishim termom u sistemi oskilki nichogo ne mozhe buti zastosovano do c shob peretvoriti jogo dali Cej priklad vede nas do viznachennya deyakih vazhlivih ponyat u zagalnomu nalashtuvanni ARS displaystyle stackrel rightarrow ce tranzitivne zamikannya displaystyle rightarrow cup de ye vidnoshennya rivnosti tobto displaystyle stackrel rightarrow ye najmenshim peredporyadkom refleksivnim i tranzitivnim vidnoshennyam sho mistit displaystyle rightarrow Jogo takozh nazivayut refleksivnim tranzitivnim zamikannyam displaystyle rightarrow displaystyle leftrightarrow ce 1 displaystyle rightarrow cup xrightarrow 1 sho ye ob yednannyam spivvidnoshennya displaystyle rightarrow z jogo zvorotnim spivvidnoshennyam takozh vidomim yak displaystyle rightarrow displaystyle stackrel leftrightarrow ce tranzitivne zamikannya displaystyle leftrightarrow cup de displaystyle stackrel leftrightarrow ye najmenshim vidnoshennyam ekvivalentnosti sho mistit displaystyle rightarrow Vin takozh vidomij yak refleksivne tranzitivne simetrichne zamikannya displaystyle rightarrow Ryadkovi sistemi rerajtinga Ryadkova sistema rerajtinga angl SRS takozh vidoma yak sistema semi Thue vikoristovuye vilnu monoyidnu strukturu ryadkiv sliv nad alfavitom shob rozshiriti vidnoshennya rerajtinga R displaystyle R dlya vsih ryadkiv u alfaviti sho mistyat livu i vidpovidno pravu storonu deyakih pravil yak pidryadka Formalno semi Thue sistemi ce para S R displaystyle Sigma R de S displaystyle Sigma najchastishe kincevij alfavit a R displaystyle R ce binarne vidnoshennya mizh deyakimi fiksovanimi strokami v alfaviti sho nazivayutsya pravilami rerajtinga Odnokrokove vidnoshennya rerajtinga vidnosini R displaystyle xrightarrow R viklikanoyi R displaystyle R na S displaystyle Sigma viznachayetsya tak dlya bud yakih strok s t S displaystyle s t in Sigma s R t displaystyle s xrightarrow R t yaksho i tilki yaksho ye x y u v S displaystyle x y u v in Sigma taki sho s x u y displaystyle s xuy t x v y displaystyle t xvy i u R v displaystyle uRv Tak yak R displaystyle xrightarrow R ye vidnoshennyam na S displaystyle Sigma para S R displaystyle Sigma xrightarrow R pidhodit do viznachennya abstraktnoyi sistemi rerajtinga Ochevidno sho R displaystyle R ye pidmnozhinoyu z R displaystyle xrightarrow R Yaksho vidnoshennya R displaystyle R ye simetrichnim todi sistema nazivayetsya sistemoyu Thue U SRS vidnoshennya skorochennya R displaystyle xrightarrow R sumisne z monoyidnoyu operaciyeyu sho oznachaye sho z x R y displaystyle x xrightarrow R y vitikaye u x v R u y v displaystyle uxv xrightarrow R uyv dlya usih ryadkiv x y u v S displaystyle x y u v in Sigma Analogichnim chinom refleksivne tranzitivne simetrichne zamikannya R displaystyle xrightarrow R poznachene R displaystyle overset underset R leftrightarrow ye kongruentnist tobto vona ye vidnoshennyam ekvivalentnosti za viznachennyam i takozh sumisna z konkatenaciyeyu ryadkiv Vidnoshennya R displaystyle overset underset R leftrightarrow nazivayetsya kongruentnistyu Thue sho porodzhuyetsya z R displaystyle R U sistemi Thue tobto yaksho R displaystyle R iye simetrichnim perepisane vidnoshennya R displaystyle xrightarrow R zbigayetsya z kongruentnistyu Thue R displaystyle overset underset R leftrightarrow Ponyattya sistemi semi Thue po suti zbigayetsya z predstavlennyam monoyida Tak yak R displaystyle overset underset R leftrightarrow ce kongruentnist mi mozhemo viznachiti faktor monoyid M R S R displaystyle mathcal M R Sigma overset underset R leftrightarrow vilnogo monoyida S displaystyle Sigma za dopomogoyu kongruentnisti Thue zvichajnim chinom Yaksho monoyid M displaystyle mathcal M izomorfnij z M R displaystyle mathcal M R to sistema semi Thue S R displaystyle Sigma R nazivayetsya monoyidnim predstavlennyam M displaystyle mathcal M Mi vidrazu otrimuyemo deyaki duzhe korisni zv yazki z inshimi oblastyami algebri Napriklad alfavit a b z pravilami ab e ba e de e ce porozhnij ryadok ye predstavlennyam vilnoyi grupi na odnomu generatori Yaksho zamist cih pravil ye lishe ab e to mi otrimuyemo uyavlennya pro biciklichnij monoyid Takim chinom sistemi Thue ye prirodnoyu osnovoyu dlya virishennya problemi sliv dlya monoyidiv ta grup Po suti kozhen monoyid maye predstavlennya formi S R displaystyle Sigma R tobto vin zavzhdi mozhe buti predstavlen sistemoyu semi Thue mozhlivo nad neskinchennim alfavitom Problema sliv dlya sistemi semi Thue v cilomu nerozv yazna cej rezultat inodi nazivayut teoremoyu Post Markova Sistemi rerajtingu termiv Sistema rerajtingu termiv TRS ce sistema rerajtingu de ob yektami ye termi abo virazi z vkladenimi pidvirazami Napriklad sistema pokazana u rozdili Logika vishe ye sistemoyu rerajtingu termiv Umovi v cij sistemi skladayutsya z binarnih operatoriv displaystyle vee i displaystyle wedge i universalnogo operatora displaystyle neg Takozh u pravilah ye zminni kozhna z yakih predstavlyaye bud yakij mozhlivij term hocha odna zminna zavzhdi predstavlyaye odin i toj zhe term v odnomu pravili Na vidminu vid ryadkovoyi sistemi rerajtingu ob yektami yakoyi ye ploski poslidovnosti simvoliv ob yekti na yakih pracyuye sistema perepisuvannya tobto termi utvoryuyut algebru termiv Term mozhna vizualizuvati yak derevo simvoliv nabir prijnyatih simvoliv fiksuyetsya danim pidpisom Sistemi rerajtinga slidiv Teoriya slidiv daye zmogu obgovoryuvati bagatoprocesornist formalnimi terminami napriklad cherez monoyid slidu ta monoyid istoriyi Rerajting mozhna vikonuvati i v sistemah slidiv FilosofiyaSistemi rerajtinga mozhut rozglyadatisya yak programi yaki vivodyat kincevi efekti zi spisku prichinno naslidkovih zv yazkiv Takim chinom sistemi rerajtinga mozhut rozglyadatis yak sistemi avtomatichnogo dovedennya prichinnosti Div takozhvkazuyut na perezapis yakij vikonuyetsya paralelno Prozorist posilan v galuzi informatikiPodalshe chitannyaMarc 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 Gerard 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 Jurgen Avenhaus and Klaus Madlener Term rewriting and equational reasoning In Ranan B Banerji Ed Formal Techniques in Artificial Intelligence A Sourcebook Elsevier 1990 Rerajting ryadkiv 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 Inshi 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 PrimitkiHsiang Jieh et al The term rewriting approach to automated theorem proving The Journal of Logic Programming 14 1 2 1992 71 99 Fruhwirth Thom Theory and practice of constraint handling rules The Journal of Logic Programming 37 1 1998 95 138 Clavel Manuel et al Maude Specification and programming in rewriting logic Theoretical Computer Science 285 2 2002 187 243 Kim Marriott Peter J Stuckey 1998 Programming with Constraints An Introduction MIT Press s 436 ISBN 978 0 262 13341 8 Bezem et al p 7 Book and Otto p 10 Baader and Nipkow pp 8 9 Martin Davis et al 1994 p 178 Ce nezavershena stattya z logiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi Ce nezavershena stattya z informatiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi Ce nezavershena stattya z matematiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi Cya stattya potrebuye dodatkovih posilan na dzherela dlya polipshennya yiyi perevirnosti Bud laska dopomozhit udoskonaliti cyu stattyu dodavshi posilannya na nadijni avtoritetni dzherela Zvernitsya na storinku obgovorennya za poyasnennyami ta dopomozhit vipraviti nedoliki Material bez dzherel mozhe buti piddano sumnivu ta vilucheno gruden 2017