Przepisywanie - Rewriting

W matematyce , informatyce i logiki , przepisywania obejmuje szeroki zakres (potencjalnie niedeterministycznego ) metody zastępowania subterms o wzorze z innymi terminami. Przedmiotem uwagi do tego artykułu obejmują systemy nadpisywania (znane również jako systemy przepisywania , silników przepisywania lub systemy redukcji ). W swojej najbardziej podstawowej formie składają się z zestawu obiektów oraz relacji dotyczących sposobu przekształcania tych obiektów.

Przepisywanie może być niedeterministyczne . Jedna reguła przepisywania terminu może być zastosowana do tego terminu na wiele różnych sposobów lub może mieć zastosowanie więcej niż jedna reguła. Systemy przepisywania nie zapewniają wtedy algorytmu zmiany jednego terminu na inny, ale zestaw możliwych zastosowań reguł. Jednak w połączeniu z odpowiednim algorytmem systemy przepisywania mogą być postrzegane jako programy komputerowe , a kilka dowodzących twierdzeń i deklaratywnych języków programowania opiera się na przepisaniu terminów.

Przykładowe przypadki

Logika

W logice procedura uzyskiwania spójnej postaci normalnej (CNF) formuły może być zaimplementowana jako system przepisywania. Reguły przykładu takiego systemu to:

${\ Displaystyle \ neg \ neg A \ do A}$( eliminacja podwójnej negacji )

${\ Displaystyle \ neg (A \ ziemia B) \ do \ neg A \ lub \ neg B}$( Prawa De Morgana )

${\ Displaystyle \ neg (A \ lub B) \ do \ neg A \ ziemia \ neg B}$

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

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

gdzie symbol ( ) wskazuje, że wyrażenie pasujące do lewej strony reguły może zostać przepisane na wyrażenie utworzone przez prawą stronę, a każdy z symboli oznacza podwyrażenie. W takim systemie każda reguła jest dobierana tak, aby lewa strona była równoważna prawej stronie, a co za tym idzie, gdy lewa strona pasuje do podwyrażenia, przepisanie tego podwyrażenia od lewej do prawej zachowuje logiczną spójność i wartość całego wyrażenia . ${\ Displaystyle \ do}$

Arytmetyka

Systemy przepisywania terminów mogą być stosowane do obliczania operacji arytmetycznych na liczbach naturalnych . W tym celu każdy taki numer musi być zakodowany jako termin . Najprostszym kodowaniem jest kodowanie stosowane w aksjomatach Peano , oparte na stałej 0 (zero) i funkcji następcy S . na przykład liczby 0, 1, 2 i 3 są reprezentowane odpowiednio przez terminy 0, S(0), S(S(0)) i S(S(S(0))). Do obliczenia sumy i iloczynu danych liczb naturalnych można użyć następującego systemu przepisywania terminów.

${\ Displaystyle {\ zacząć {wyrównany} A + 0 i \ do A i {\ textrm {(1)}}, \ \ A + S (B) i \ do S (A + B) i {\ textrm {(2) }},\\A\cdot 0&\do 0&{\textrm {(3)}},\\A\cdot S(B)&\do A+(A\cdot B)&{\textrm {(4)} }.\end{wyrównany}}}$

Na przykład, obliczenie 2+2 dające wynik 4 może zostać zduplikowane przez przepisanie terminu w następujący sposób:

${\ Displaystyle S (S (0)) + S (S (0))}$ ${\displaystyle \;\;{\stackrel {(2)}{\do}}\;\;}$ ${\displaystyle S(\;S(S(0))+S(0)\;)}$ ${\displaystyle \;\;{\stackrel {(2)}{\do}}\;\;}$ ${\displaystyle S(S(\;S(S(0))+0\;))}$ ${\displaystyle \;\;{\stackrel {(1)}{\do}}\;\;}$ ${\displaystyle S(S(S(S(0)))),}$

gdzie numery reguł są podane nad strzałką przepisywania .

Jako inny przykład, obliczenie 2⋅2 wygląda tak:

${\ Displaystyle S (S (0)) \ cdot S (S (0))}$ ${\displaystyle \;\;{\stackrel {(4)}{\do}}\;\;}$ ${\ Displaystyle S (S (0)) + S (S (0)) \ cdot S (0)}$ ${\displaystyle \;\;{\stackrel {(4)}{\do}}\;\;}$ ${\ Displaystyle S (S (0)) + S (S (0)) + S (S (0)) \ cdot 0}$ ${\displaystyle \;\;{\stackrel {(3)}{\do}}\;\;}$ ${\ Displaystyle S (S (0)) + S (S (0)) + 0)}$ ${\displaystyle \;\;{\stackrel {(1)}{\do}}\;\;}$ ${\ Displaystyle S (S (0)) + S (S (0))}$ ${\displaystyle \;\;{\stackrel {\textrm {sa}}{\do}}\;\;}$ ${\displaystyle S(S(S(S(0)))),}$

gdzie ostatni krok obejmuje poprzednie przykładowe obliczenia.

Językoznawstwo

W językoznawstwie , zasady struktur frazowych , zwane także zasady przepisywania , są używane w niektórych systemach gramatyki generatywnej , jako sposobu generowania gramatycznie poprawnych zdań języka. Taka reguła zazwyczaj przyjmuje postać A → X, gdzie A jest etykietą kategorii składniowej , taką jak fraza rzeczownikowa lub zdanie , a X jest sekwencją takich etykiet lub morfemów , wyrażającą fakt, że A może być zastąpione przez X przy generowaniu składowa budowa zdania. Na przykład reguła S → NP VP oznacza, że ​​zdanie może składać się z frazy rzeczownikowej, po której następuje fraza czasownikowa ; dalsze zasady określą, z jakich części składowych może składać się fraza rzeczownikowa i fraza czasownikowa, i tak dalej.

Abstrakcyjne systemy przepisywania

Z powyższych przykładów jasno wynika, że ​​możemy myśleć o przepisaniu systemów w sposób abstrakcyjny. Musimy określić zestaw obiektów i zasady, które można zastosować do ich przekształcenia. Najbardziej ogólne (jednowymiarowe) ustawienie tego pojęcia nazywa się abstrakcyjnym systemem redukcji lub abstrakcyjnym systemem przepisywania (w skrócie ARS ). ARS jest po prostu zbiorem obiektów wraz z relacji binarnej → na zwana relacja redukcja , przepisać relacja lub po prostu redukcja .

W ogólnym ustawieniu ARS można zdefiniować wiele pojęć i notacji. jest odruchowy domknięcie przechodnie z . jest symetryczny zamknięcie od . jest odruchowy przechodnia symetryczny zamknięcie od . Zadanie tekstowe dla ARS polega na określeniu, przy danym x i y , czy . Obiekt x w A nazywamy redukcyjnym, jeśli istnieje jakieś inne y w A takie, że ; inaczej nazywa się to nieredukowalną lub normalną formą . Obiekt y nazywamy „formą normalną x ”, jeśli , a y jest nieredukowalne. Jeśli forma normalna x jest unikalna, to jest zwykle oznaczana przez . Jeśli każdy obiekt ma co najmniej jedną formę normalną, ARS nazywa się normalizowaniem . lub x i y są uważane za możliwe do połączenia, jeśli istnieje pewna część z z właściwością, która . Mówi się, że ARS posiada własność Church-Rosser, jeśli implikuje . ARS jest zlewające się , gdy dla wszystkich wagowo , x i y w A , oznacza . ARS jest lokalnie zrastania wtedy i tylko wtedy, gdy dla wszystkich w , x i y w A , zakłada . Mówi się, że ARS jest kończący się lub noetherian, jeśli nie ma nieskończonego łańcucha . Konfluentny i kończący się ARS nazywa się zbieżnym lub kanonicznym . ${\displaystyle {\stackrel {*}{\rightarrow}}}$${\displaystyle \rightarrow}$${\displaystyle \leftrightarrow}$${\displaystyle \rightarrow}$${\displaystyle {\stackrel {*}{\,\leftrightarrow \,}}}$${\displaystyle \rightarrow}$${\displaystyle x{\stackrel {*}{\\leftrightarrow \,}}y}$${\displaystyle x\rightarrow y}$${\displaystyle x{\stackrel {*}{\\rightarrow \,}}y}$${\displaystyle x{\downarrow}}$${\displaystyle x\downarrow y}$${\displaystyle x{\stackrel {*}{\\rightarrow \,}}z{\stackrel {*}{\\leftarrow \,}}y}$${\displaystyle x{\stackrel {*}{\\leftrightarrow \,}}y}$${\displaystyle x\downarrow y}$${\displaystyle x{\stackrel {*}{\,\leftarrow \,}}w{\stackrel {*}{\,\rightarrow \,}}y}$${\displaystyle x\downarrow y}$${\displaystyle x\leftarrow w\rightarrow y}$${\displaystyle x{\mathbin {\downarrow}}y}$${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots}$

Ważnymi twierdzeniami dla abstrakcyjnych systemów przepisywania jest to, że ARS jest konfluentny, jeśli ma własność Church-Rosser, lemat Newmana, który mówi, że kończący ARS jest konfluentny wtedy i tylko wtedy, gdy jest konfluentny lokalnie, oraz że problem tekstowy dla ARS jest nierozstrzygalny ogólnie.

Systemy przepisywania ciągów

System przepisywania ciągów (SRS), znany również jako system semi-Thue , wykorzystuje wolną strukturę monoidów ciągów (słów) w alfabecie, aby rozszerzyć relację ponownego zapisywania , , na wszystkie ciągi w alfabecie, które zawierają lewy i odpowiednio prawy -strony niektórych reguł jako podciągi . Formalnie system semi-Thue to krotka, w której jest (zazwyczaj skończonym) alfabetem i jest binarną relacją między niektórymi (stałymi) ciągami w alfabecie, zwanym zbiorem reguł przepisywania . Jednoetapowa przepisywanie związek wywołane na definiuje się następująco: do strun , wtedy i tylko wtedy, gdy istnieje taka, że , i . Ponieważ jest relacją na , para pasuje do definicji abstrakcyjnego systemu przepisywania. Oczywiście jest podzbiorem . Jeśli relacja jest symetryczna , to system nazywa się systemem Thue . ${\ Displaystyle R}$ ${\displaystyle (\Sigma,R)}$${\ Displaystyle \ Sigma}$${\ Displaystyle R}$ ${\ Displaystyle {\ xrightarrow [{R}] {}}}$${\ Displaystyle R}$${\ Displaystyle \ Sigma ^ {*}}$${\ Displaystyle s, t \ w \ Sigma ^ {*}}$ ${\ Displaystyle s \ {\ xrightarrow [{R}] {}} \ t}$${\ Displaystyle x, y, u, v \ w \ 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}$

W SRS relacja redukcji jest zgodna z operacją monoidu, co oznacza, że oznacza to dla wszystkich łańcuchów . Podobnie, zwrotne przechodnie symetryczne domknięcie , oznaczane , jest kongruencją , co oznacza, że ​​jest relacją równoważności (z definicji) i jest również zgodne z konkatenacją strun. Relacja nazywana jest kongruencją Thue generowaną przez . W systemie Thue, tj. jeśli jest symetryczny, relacja przepisywania pokrywa się z kongruencją Thue . ${\ Displaystyle {\ xrightarrow [{R}] {*}}}$${\ Displaystyle x \, {\ xrightarrow [{R}] {*}} \, y}$${\ Displaystyle uxv \ {\ xrightarrow [{R}] {*}} \ uyv}$${\ Displaystyle x, y, u, v \ w \ Sigma ^ {*}}$${\ Displaystyle {\ xrightarrow [{R}] {}}}$${\ Displaystyle {\ overset {*} {\ underset {R} {\ leftrightarrow}}}}$${\ Displaystyle {\ overset {*} {\ underset {R} {\ leftrightarrow}}}}$${\ Displaystyle R}$${\ Displaystyle R}$${\ Displaystyle {\ xrightarrow [{R}] {*}}}$${\ Displaystyle {\ overset {*} {\ underset {R} {\ leftrightarrow}}}}$

Pojęcie systemu semi-Thue zasadniczo pokrywa się z przedstawieniem monoidu . Ponieważ jest kongruencją, możemy zdefiniować czynnik monoidu wolnego monoidu przez kongruencję Thue. Jeśli monoid jest izomorficzna z , wówczas system semi-Thue nazywa się monoid prezentację o . ${\ Displaystyle {\ overset {*} {\ underset {R} {\ leftrightarrow}}}}$ ${\ Displaystyle {\ mathcal {M}} _ {R} = \ Sigma ^ {*} / {\ przesunięty {*} {\ zaniżony {R} {\ leftrightarrow}}}}$${\ Displaystyle \ Sigma ^ {*}}$${\ Displaystyle {\ Mathcal {M}}}$${\ Displaystyle {\ Mathcal {M}} _ {R}}$${\displaystyle (\Sigma,R)}$${\ Displaystyle {\ Mathcal {M}}}$

Od razu otrzymujemy bardzo przydatne połączenia z innymi dziedzinami algebry. Na przykład alfabet { a , b } z regułami { ab → ε, ba → ε }, gdzie ε jest ciągiem pustym , jest prezentacją wolnej grupy na jednym generatorze. Jeśli zamiast tego reguły są po prostu { ab → ε }, to otrzymujemy prezentację bicyklicznego monoidu . W ten sposób systemy semi-Thue stanowią naturalne ramy dla rozwiązania zadania tekstowego dla monoidów i grup. W rzeczywistości każdy monoid ma prezentację formy , tzn. zawsze może być przedstawiony w systemie semi-Thue, być może po nieskończonym alfabecie. ${\displaystyle (\Sigma,R)}$

Problem tekstowy dla systemu semi-Thue jest w ogólności nierozstrzygalny; wynik ten jest czasami nazywany twierdzeniem Post-Markowa .

Systemy przepisywania terminów

Rys.1: Schematyczny trójkątny diagram zastosowania reguły przepisywania na pozycji w wyrażeniu, z dopasowaniem podstawienia${\displaystyle l\longrightarrow r}$${\displaystyle p}$${\displaystyle \sigma}$

Rys.2: Reguła lhs dopasowywanie terminów w terminach${\ Displaystyle x * (y * z)}$${\ Displaystyle {\ Frac {a * ((a + 1) * (a + 2) {1 * (2 * 3)}}}$

System przepisywania terminów ( TRS ) to system przepisywania, którego obiektami są terminy , które są wyrażeniami z zagnieżdżonymi wyrażeniami podrzędnymi. Na przykład system przedstawiony w § Logika powyżej jest systemem przepisywania terminów. Terminy w tym systemie składają się z operatorów binarnych i operatora jednoargumentowego . W regułach obecne są również zmienne, które reprezentują dowolny możliwy termin (chociaż pojedyncza zmienna zawsze reprezentuje ten sam termin w jednej regule). ${\displaystyle (\vee)}$${\displaystyle (\klin )}$${\displaystyle (\neg)}$

W przeciwieństwie do systemów przepisywania łańcuchów, których obiektami są sekwencje symboli, obiekty systemu przepisywania terminów tworzą algebrę terminów . Termin można zwizualizować w postaci drzewa symboli, przy czym zbiór dopuszczonych symboli jest ustalony przez daną sygnaturę .

Formalna definicja

Reguła przepisywania jest parę terminów , jak powszechnie napisany , aby wskazać, że lewa strona l może być zastąpiony przez prawej bocznej r . System termin przepisywanie jest zbiorem R od tych zasad. Reguła może być zastosowana do wyrazu s, jeśli lewy wyraz l pasuje do jakiegoś podterminu z s , to znaczy, jeśli istnieje takie podstawienie , że podtermin zakorzenionego w pewnej pozycji p jest wynikiem zastosowania podstawienia do wyrazu l . Termin podrzędny odpowiadający lewej stronie reguły nazywany jest wyrażeniem redeks lub wyrażeniem redukowalnym . Wyraz wynikowy t tego zastosowania reguły jest zatem wynikiem zastąpienia podwyrazu w pozycji p in s wyrazem z zastosowanym podstawieniem , patrz rysunek 1. W tym przypadku mówi się, że jest przepisany w jednym kroku lub przepisany bezpośrednio , aby przez system , formalnie oznaczona jako , albo jak przez niektórych autorów. ${\displaystyle l\rightarrow r}$${\displaystyle l\rightarrow r}$ ${\displaystyle \sigma}$${\displaystyle s}$ ${\displaystyle \sigma}$${\ Displaystyle r}$${\displaystyle \sigma}$${\displaystyle s}$${\displaystyle t}$${\ Displaystyle R}$${\displaystyle s\rightarrow _{R}t}$${\ Displaystyle s \ {\ xrightarrow [{R}] {}} \ t}$${\displaystyle s\,{\xrightarrow {R}}\,t}$

Jeśli termin może być przepisany w kilku krokach w termin , to znaczy, jeśli , termin ma zostać przepisany na , formalnie oznaczony jako . Innymi słowy, relacja jest przechodnim zamknięciem relacji ; Często również oznaczenie jest używany do oznaczenia zamknięcie zwrotne-przechodni z , to znaczy, jeśli s = T lub . Termin przepisywania określony przez zbiór reguł może być postrzegany jako abstrakcyjny system przepisywania zdefiniowany powyżej , z terminami jako jego przedmiotami i jako jego relacja przepisywania. ${\displaystyle t_{1}}$${\displaystyle t_{n}}$${\ Displaystyle t_ {1} \ {\ xrightarrow [{R}] {}} \ t_ {2} \ {\ xrightarrow [ {R}] {}} \ \ ldots \ {\ xrightarrow [{ R}]{}}\,t_{n}}$${\displaystyle t_{1}}$${\displaystyle t_{n}}$${\ Displaystyle t_ {1} \ {\ xrightarrow [{R}] {+}} \ t_ {n}}$${\ Displaystyle {\ xrightarrow [{R}] {+}}}$${\ Displaystyle {\ xrightarrow [{R}] {}}}$${\ Displaystyle {\ xrightarrow [{R}] {*}}}$${\ Displaystyle {\ xrightarrow [{R}] {}}}$${\ Displaystyle s \, {\ xrightarrow [{R}] {*}} \ t}$${\ Displaystyle s \, {\ xrightarrow [{R}] {+}} \ t}$${\ Displaystyle R}$${\ Displaystyle {\ xrightarrow [{R}] {}}}$

Na przykład jest regułą przepisywania, powszechnie używaną do ustanowienia normalnej formy w odniesieniu do zespolenia . Ta reguła może być zastosowana w liczniku w terminie z pasującym podstawieniem , patrz rysunek 2. Zastosowanie tego podstawienia do prawej strony reguły daje w wyniku termin ( a *( a + 1))*( a +2) i zastąpienie licznika tym terminem daje , co jest wynikiem zastosowania reguły przepisywania. Ogólnie rzecz biorąc, zastosowanie zasady przepisywania osiągnęło to, co nazywa się „stosowaniem prawa łączności do ” w elementarnej algebrze. Alternatywnie reguła mogła być zastosowana do mianownika pierwotnego terminu, ustępując . ${\displaystyle x*(y*z)\rightarrow (x*y)*z}$${\ Displaystyle *}$${\ Displaystyle {\ Frac {a * ((a + 1) * (a + 2) {1 * (2 * 3)}}}$${\ Displaystyle \ {x \ mapsto a \; y \ mapsto a +1 \; z \ mapsto a +2 \}}$${\ Displaystyle {\ Frac {(a*(a+1))*(a+2)}{1*(2*3)}}}$${\ Displaystyle *}$${\ Displaystyle {\ Frac {a * ((a + 1) * (a + 2) {1 * (2 * 3)}}}$${\ Displaystyle {\ Frac {a * (((a+1)*(a+2))}{(1*2)*3}}}$

Zakończenie

Poza sekcją Terminacja i konwergencja należy rozważyć dodatkowe subtelności dotyczące systemów przepisywania terminów.

Wypowiedzenie nawet systemu składającego się z jednej reguły z liniową lewą stroną jest nierozstrzygnięte. Terminacja jest również nierozstrzygnięta dla systemów używających tylko jednoargumentowych symboli funkcji; jednak jest to decydujące dla skończonych systemów gruntowych .

Poniższy termin system przepisywania jest normalizujący, ale nie kończący się i nie zlewny:

${\displaystyle f(x,x)\rightarrow g(x),}$

${\displaystyle f(x,g(x))\rightarrow b,}$

${\displaystyle h(c,x)\rightarrow f(h(x,c),h(x,x)).}$

Poniższe dwa przykłady zakończenia systemów przepisywania terminów są spowodowane przez firmę Toyama:

${\displaystyle f(0,1,x)\rightarrow f(x,x,x)}$

oraz

${\displaystyle g(x,y)\rightarrow x,}$

${\displaystyle g(x,y)\rightarrow y.}$

Ich związek jest systemem niekończącym się, ponieważ . Ten wynik obala przypuszczenie Dershowitza , który twierdził, że połączenie dwóch końcowych systemów przepisywania terminów i ponownie kończy się, jeśli wszystkie lewe i prawe strony są liniowe i nie ma „ nakładania się ” między lewą stroną boki i prawe strony . Wszystkie te właściwości spełniają przykłady firmy Toyama. ${\displaystyle f(g(0,1),g(0,1),g(0,1))\rightarrow f(0,g(0,1),g(0,1))\rightarrow f( 0,1,g(0,1))\rightarrow f(g(0,1),g(0,1),g(0,1))\rightarrow \ldots }$${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$

Zobacz Kolejność przepisywania i Zamawianie ścieżek (przepisywanie terminów) dla relacji porządkowania używanych w dowodach zakończenia dla systemów przepisywania terminów.

Systemy przepisywania wyższego rzędu

Systemy przepisywania wyższego rzędu są uogólnieniem systemów przepisywania terminów pierwszego rzędu na wyrażenia lambda , umożliwiając funkcje wyższego rzędu i zmienne powiązane. Różne wyniki dotyczące TRS pierwszego rzędu można również przeformułować dla HRS.

Systemy przepisywania grafów

Systemy przepisywania grafów są kolejnym uogólnieniem systemów przepisywania terminów, operujących na grafach zamiast terminów ( podstawowych -) / odpowiadających im reprezentacji drzewiastych .

Systemy przepisywania śladów

Teoria śledzenia dostarcza środków do omawiania wieloprocesowości w bardziej formalnych kategoriach, takich jak monoid śledzenia i monoid historii . Przepisywanie można również wykonać w systemach śledzenia.

Filozofia

Systemy przepisywania mogą być postrzegane jako programy, które wywnioskują skutki końcowe z listy związków przyczynowo-skutkowych. W ten sposób systemy przepisywania można uznać za zautomatyzowane dowody przyczynowości .

Zobacz też

• Para krytyczna (logika)
• Kompilator
• Algorytm uzupełniania Knutha-Bendixa
• Systemy L określają przepisywanie, które odbywa się równolegle.
• Przejrzystość referencyjna w informatyce
• Przepisywanie regulowane
• rachunek Rho

Uwagi

Bibliografia

Dalsza lektura

• Baader, Franz ; Nipkow, Tobiasz (1999). Przepisywanie terminów i tak dalej . Wydawnictwo Uniwersytetu Cambridge. Numer ISBN 978-0-521-77920-3.316 stron. Podręcznik odpowiedni dla studentów.
• Marc Bezem , Jan Willem Klop , Roel de Vrijer ("Teresa"), Systemy przepisywania terminów ("TeReSe"), Cambridge University Press, 2003, ISBN  0-521-39115-6 . Jest to najnowsza obszerna monografia. Wykorzystuje jednak sporo niestandardowych jeszcze notacji i definicji. Na przykład właściwość Church–Rosser definiuje się jako identyczną z konfluencją.
• Nachum Dershowitz i Jean-Pierre Jouannaud „Przepisz systemy” , rozdział 6 w Jan van Leeuwen (red.), Podręcznik informatyki teoretycznej , tom B: Modele formalne i semantyka. , Elsevier i MIT Press, 1990, ISBN  0-444-88074-7 , s. 243-320. Preprint tego rozdziału jest swobodnie dostępny od autorów, ale brakuje danych liczbowych.
• Nachuma Dershowitza i Davida Plaisteda . „Przepisywanie” , rozdział 9 w John Alan Robinson i Andrei Voronkov (red.), Handbook of Automated Reasoning , tom 1 .
• Gérard Huet et Derek Oppen, Equations and Rewrite Rules, A Survey (1980) Stanford Verification Group, Raport nr 15 Raport Departamentu Informatyki nr STAN-CS-80-785
• Jan Willem Klop . „Term Rewriting Systems”, rozdział 1 w Samson Abramsky , Dov M. Gabbay i Tom Maibaum (red.), Handbook of Logic in Computer Science , tom 2: Background: Computational Structures .
• David Plaisted. „Rozumowanie równoważne i systemy przepisywania terminów” , w: Dov M. Gabbay , CJ Hogger i John Alan Robinson (red.), Handbook of Logic in Artificial Intelligence and Logic Programming , tom 1 .
• Jürgen Avenhaus i Klaus Madlener. „Przepisywanie terminów i rozumowanie równania”. W Ranan B. Banerji (red.), Techniki formalne w sztucznej inteligencji: podręcznik źródłowy , Elsevier (1990).

Przepisywanie ciągów

• Ronald V. Book i Friedrich Otto, Systemy przepisywania strun , Springer (1993).
• Benjamin Benninghofen, Susanne Kemmerich i Michael M. Richter , Systemy redukcji . LNCS 277 , Springer-Verlag (1987).

Inne

• Martin Davis , Ron Sigal , Elaine J. Weyuker , (1994) Obliczalność, złożoność i języki: Podstawy informatyki teoretycznej – wydanie 2 , Academic Press, ISBN  0-12-206382-1 .

Zewnętrzne linki

• Przepisywanie Strona główna
• Grupa Robocza IFIP 1.6
• Naukowcy w przepisaniu przez Aart Middeldorp , University of Innsbruck
• Portal wypowiedzenia