Átírás - Rewriting

A matematika , számítástechnika , és a logika , újraírás széles körét öleli fel (potenciálisan nem-determinisztikus ) módszerek helyett subterms egy formula más kifejezésekkel. A cikk középpontjában az átírási rendszerek (más néven átírási rendszerek , átírási motorok vagy redukciós rendszerek ) állnak. A legalapvetőbb formában objektumokból állnak, valamint az objektumok átalakításának összefüggéseiből.

Az átírás nem lehet determinisztikus . A kifejezés átírásának egyetlen szabálya sokféleképpen alkalmazható erre a kifejezésre, vagy több szabály is alkalmazható. Az átírási rendszerek ezután nem algoritmust biztosítanak az egyik kifejezés másikra való cseréjéhez, hanem a lehetséges szabályalkalmazások halmazát. Megfelelő algoritmussal kombinálva azonban az átírási rendszerek számítógépes programoknak tekinthetők , és számos tétel -fejlesztő és deklaratív programozási nyelv a kifejezések átírásán alapul.

Példa esetek

Logika

A logika szerint a képlet konjunktív normál formájának (CNF) megszerzésére irányuló eljárás átírási rendszerként valósítható meg. Egy ilyen rendszerre vonatkozó szabályok a következők:

${\ displaystyle \ neg \ neg A \ - A}$( kettős tagadás megszüntetése )

${\ displaystyle \ neg (A \ land B) \ to \ neg A \ lor \ neg B}$( De Morgan törvényei )

${\ 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)}$( eloszthatóság )

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

ahol a szimbólum ( ) azt jelzi, hogy a szabály bal oldalához illeszkedő kifejezés átírható a jobb oldal alkotta kifejezésre, és a szimbólumok mindegyike egy részkifejezést jelöl. Egy ilyen rendszerben minden szabály úgy van megválasztva, hogy a bal oldal egyenértékű legyen a jobb oldallal, és következésképpen, ha a bal oldal illeszkedik egy részkifejezéshez, akkor az alkifejezés balról jobbra történő átírása megtartja a teljes kifejezés logikai következetességét és értékét . ${\ displaystyle \ to}$

Számtan

Kifejezések átírási rendszerei alkalmazhatók számtani műveletek számítására természetes számokkal . Ebből a célból minden egyes ilyen számot kell kódolni, mint a kifejezést . A legegyszerűbb kódolás az egyik alkalmazott a Peano axiómák alapján az állandó 0 (nulla), és az utódja funkció S . például a 0, 1, 2 és 3 számokat a 0, S (0), S (S (0)) és S (S (S (0))) kifejezések jelentik. A következő kifejezés -átírási rendszer használható az adott természetes számok összegének és szorzatának kiszámítására.

${\ displaystyle {\ begin {aligned} A+0 & \ - A & {\ textrm {(1)}}, \\ A+S (B) & \ to S (A+B) & {\ textrm {(2) }}, \\ A \ cdot 0 & \ to 0 & {\ textrm {(3)}}, \\ A \ cdot S (B) & \ to A+(A \ cdot B) & {\ textrm {(4)} }. \ end {igazítva}}}$

Például a 2+2 kiszámítása 4 -gyel megismételhető a kifejezés átírásával az alábbiak szerint:

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

ahol a szabályszámok az átírási nyíl fölött vannak megadva .

Másik példaként a 2⋅2 számítása így néz ki:

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

ahol az utolsó lépés az előző példaszámítást tartalmazza.

Nyelvészet

A nyelvészet , frázisszerkezet szabályok , más néven átírási szabályokat , alkalmaznak néhány rendszerek generatív grammatika , mint azt a generáló nyelvtanilag helyes mondatokat egy nyelvet. Egy ilyen szabály általában A → X formát ölt, ahol A egy szintaktikai kategóriacímke , például főnévi kifejezés vagy mondat , X pedig az ilyen címkék vagy morfémák sorozata , kifejezve azt a tényt, hogy A helyettesíthető X -el a a mondat alkotó szerkezete. Például a szabály S → NP VP azt jelenti, hogy a mondat állhat főnév kifejezést, majd egy igei ; a további szabályok meghatározzák, hogy a főnévi kifejezés és az igefordulat milyen alkotóelemekből állhat stb.

Absztrakt átírási rendszerek

A fenti példákból egyértelműen kiderül, hogy absztrakt módon gondolhatunk a rendszerek átírására. Meg kell adnunk egy objektumhalmazt és az átalakításra alkalmazható szabályokat. Ennek a fogalomnak a legáltalánosabb (egydimenziós) beállítását nevezik absztrakt redukciós rendszernek vagy absztrakt átírási rendszernek (rövidítve ARS ). Az ARS egyszerűen objektumok A halmaza , bináris relációval együtt → A -n , amelyet redukciós relációnak , átírási relációnak vagy éppen redukciónak neveznek .

Az ARS általános beállításaiban sok fogalom és jelölés definiálható. a visszaható tranzitív lezárása a . a szimmetrikus lezárása a . a visszaható tranzitív szimmetrikus bezárása a . A szöveges feladatok egy ARS meghatározó, hiszen x és y , akár . Egy tárgy x az A nevezzük redukálható , ha létezik néhány más y in A , hogy ; egyébként redukálhatatlannak vagy normál formának nevezik . Az y objektumot "normál x formájának" nevezzük, ha és y redukálhatatlan. Ha az x normál formája egyedi, akkor ezt általában a -val jelöljük . Ha minden objektumnak van legalább egy normál formája, akkor az ARS -t normalizálásnak nevezzük . vagy x és y összekapcsolhatónak mondható, ha létezik néhány z a tulajdonsággal . Az ARS állítólag birtokolja az egyház – Rosser tulajdont, ha erre utal . ARS konfluens , ha minden w , x , és y a A , magában foglalja . ARS helyben összefolynak akkor és csak ha minden w , x és y az A , magában foglalja . Azt mondják, hogy az ARS befejező vagy nemetikus, ha nincs végtelen lánc . Az összefolyó és végződő ARS -t konvergensnek vagy kanonikusnak nevezik . ${\ 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}$

Fontos tételei elvont újraírása rendszerek, amelyek ARS összefolyó IFF azt az egyház-Rosser ingatlanok, Newman-lemma , amely kimondja, hogy egy lezáró ARS van összefolyó akkor és csak akkor, ha a helyi összefolyó, és hogy a szöveges feladat egy ARS van eldönthetetlen általánosságban.

Karakterlánc -átíró rendszerek

A húr újraírás rendszer (SRS), más néven félig Thue rendszer , kihasználja a szabad monoid szerkezetét húrok (szó) több mint egy ábécé kiterjeszteni átírási kapcsolatban, , hogy minden húrok az ábécé, amelyek bal- és jobb volt -egyes szabályok kézi oldalai alláncokként . Formálisan a félig-szerű rendszer egy olyan sor, ahol egy (általában véges) ábécé van, és bináris kapcsolat az ábécé egyes (rögzített) karakterláncai között, az úgynevezett átírási szabályok halmazának . A egylépéses újraírás kapcsolatban által indukált a definíció szerint: bármely húrok , ha, és csak akkor, ha létezik olyan, hogy , , és a . Mivel a reláció be van kapcsolva , a pár illeszkedik az absztrakt átírási rendszer definíciójához. Nyilvánvalóan a részhalmaza . Ha a kapcsolat nem szimmetrikus , akkor a rendszert nevezzük Thue rendszer . ${\ displaystyle R}$ ${\ 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}$

Az SRS -ben a redukciós reláció kompatibilis a monoid művelettel, ami azt jelenti, hogy minden sztringre vonatkozik . Hasonlóképpen, a reflexív tranzitív szimmetrikus zárás , jelölve , kongruencia , azaz ekvivalencia reláció (definíció szerint), és kompatibilis a karakterlánc -összefűzéssel is. A relációt a generált Thue kongruenciának nevezzük . Egy Thue rendszerben, azaz ha szimmetrikus, az átírási reláció egybeesik a Thue kongruenciával . ${\ 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 {*} {\ underet {R} {\ leftrightarrow}}}}$${\ displaystyle {\ overset {*} {\ underet {R} {\ leftrightarrow}}}}$${\ displaystyle R}$${\ displaystyle R}$${\ displaystyle {\ xrightarrow [{R}] {*}}}$${\ displaystyle {\ overset {*} {\ underet {R} {\ leftrightarrow}}}}$

A félig Thue rendszer fogalma lényegében egybeesik a monoid bemutatásával . Mivel kongruencia, a szabad monoid faktor monoidját a Thue kongruencia segítségével határozhatjuk meg . Ha egy monoid van izomorf azzal , majd a félig Thue rendszer nevezzük monoid bemutatása az . ${\ displaystyle {\ overset {*} {\ underet {R} {\ leftrightarrow}}}}$ ${\ displaystyle {\ mathcal {M}} _ {R} = \ Sigma ^{*}/{\ overset {*} {\ underet {R} {\ leftrightarrow}}}}$${\ displaystyle \ Sigma ^{*}}$${\ displaystyle {\ mathcal {M}}}$${\ displaystyle {\ mathcal {M}} _ {R}}$${\ displaystyle (\ Sigma, R)}$${\ displaystyle {\ mathcal {M}}}$

Azonnal nagyon hasznos kapcsolatokat kapunk az algebra más területeivel. Például az { a , b } ábécé az { ab → ε, ba → ε} szabályokkal, ahol ε az üres karakterlánc , a szabad csoport bemutatása egy generátoron. Ha ehelyett a szabályok csak { ab → ε}, akkor a biciklikus monoid bemutatását kapjuk . Így félig Thue rendszerek képezik a természetes keretet megoldásához szöveges feladat az monoids és csoportok. Valójában minden monoidnak megvan a formája , azaz mindig egy félig-szerű rendszerben, esetleg végtelen ábécén keresztül. ${\ displaystyle (\ Sigma, R)}$

A félprobléma rendszer szöveges problémája általában eldönthetetlen; ezt az eredményt néha Post-Markov-tételnek nevezik .

Term átíró rendszerek

A kifejezés-átírási rendszer ( TRS ) olyan átírási rendszer, amelynek tárgyai kifejezések , amelyek egymásba ágyazott részkifejezésekkel rendelkező kifejezések. Például a fenti § Logika alatt bemutatott rendszer egy kifejezés -átírási rendszer. A kifejezések ebben a rendszerben állnak bináris operátorok és a egyoperandusú operátor . A szabályokban olyan változók is jelen vannak, amelyek bármilyen lehetséges kifejezést képviselnek (bár egyetlen változó mindig ugyanazt a kifejezést jelenti egyetlen szabályban). ${\ displaystyle (\ vee)}$${\ displaystyle (\ ék)}$${\ displaystyle (\ neg)}$

Ellentétben a karakterlánc -átíró rendszerekkel, amelyek objektumai szimbólumok sorozatai, a kifejezés -átíró rendszer objektumai kifejezés algebrát alkotnak . Egy kifejezés szimbólumok fájaként jeleníthető meg, az elfogadott szimbólumok halmazát egy adott aláírás rögzíti .

Formális meghatározás

Az átírási szabály egy kifejezéspár , amelyet általában úgy írnak , hogy jelezze, hogy a bal oldali l helyettesíthető a jobb oldali r oldallal . A kifejezés átírása rendszer egy sor R ilyen szabályok. A szabály akkor alkalmazható az s kifejezésre, ha a bal l tag egyezik az s néhány alosztályával , vagyis ha van olyan helyettesítés , amely azt jelenti, hogy a p bizonyos pozícióban gyökerező alosztály a helyettesítésnek az l kifejezésre történő alkalmazása eredménye . A szabály bal oldalához illeszkedő altermet redex vagy redukálható kifejezésnek nevezzük . Az eredmény távú t e szabály alkalmazás, akkor az eredmény a cseréje subterm pozícióban p in s a kifejezés a helyettesítés alkalmazott, lásd a képen 1. Ebben az esetben, azt mondják, hogy átírt egy lépésben , vagy átírt közvetlenül , hogy a rendszer által hivatalosan jelöljük , vagy ahogy egyes szerzők. ${\ 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}$

Ha egy kifejezés átírható több lépésben egy kifejezés , vagyis, ha a kifejezés azt mondják, hogy átírt a hivatalosan jelöljük . Más szavakkal, a kapcsolat a tranzitív lezárása az összefüggés ; gyakran, továbbá a jelölést jelölésére használjuk a reflexív-tranzitív lezárását az , hogy van, ha s = t vagy . A kifejezés átírása adott egy sor szabályt lehet tekinteni, mint egy absztrakt átírása meghatározott rendszer felett , olyan kifejezéseket, mint a tárgyak és mint a rewrite kapcsolatban. ${\ 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}] {}}}$

Például egy átírási szabály, amelyet általában használnak egy normál űrlap létrehozására a (z) asszociativitása tekintetében . Ez a szabály alkalmazható a számlálónál a kifejezésben a megfelelő helyettesítéssel , lásd a 2. ábrát. Ha ezt a helyettesítést alkalmazza a szabály jobb oldalára, akkor a ( a *( a + 1)) *( a +2) kifejezést kapja , és a számláló lecserélése erre a kifejezésre hoz , ami az átírási szabály alkalmazásának eredménye. Összességében, alkalmazva a rewrite szabály ért az úgynevezett „alkalmazása asszociatív törvény az ” elemi algebra. Alternatív megoldásként a szabály alkalmazható lett volna az eredeti kifejezés nevezőjére, a hozamra . ${\ 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}}}$

Felmondás

A terminálás és konvergencia szakaszon kívül további finomságokat kell figyelembe venni a kifejezés -átírási rendszereknél.

Még az egyetlen szabályból álló rendszer megszüntetése sem, amelynek bal oldala lineáris . A megszüntetés nem eldönthető azoknál a rendszereknél sem, amelyek csak egységes függvényszimbólumokat használnak; azonban ez eldönthető véges földi rendszerek.

A következő kifejezés átírási rendszer normalizálódik, de nem fejeződik be, és nem összefolyó:

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

${\ displaystyle f (x, g (x)) \ b jobbra mutató nyíl,}$

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

A következő két példa a terminus -átírási rendszerek leállítására a Toyamának köszönhető:

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

és

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

${\ displaystyle g (x, y) \ y jobbra mutató nyíl.}$

Szövetségük nem szűnő rendszer, hiszen . Ez az eredmény cáfolja Dershowitz sejtését , aki azt állította, hogy két befejező kifejezés átírási rendszer egyesülése, és ismét véget ér, ha a bal és a jobb oldalak mindegyike lineáris , és nincsenek " átfedések " a balkezesek között oldalai és jobb oldalai . Toyama példái mindezeket a tulajdonságokat kielégítik. ${\ 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)) \ jobbra mutató nyila f (g (0,1), g (0,1), g (0,1)) \ jobbra nyíl \ ldots}$${\ displaystyle R_ {1}}$${\ displaystyle R_ {2}}$${\ displaystyle R_ {1}}$${\ displaystyle R_ {2}}$${\ displaystyle R_ {1}}$${\ displaystyle R_ {2}}$

Lásd: Átírási sorrend és Útvonalrendelés (kifejezés -átírás) a terminus -átírási rendszerek felmondási igazolásaiban használt rendezési kapcsolatokról.

Magasabb rendű átírási rendszerek

A magasabb rendű átírási rendszerek az elsőrendű terminus-átírási rendszerek lambda kifejezésekre történő általánosítása , lehetővé téve a magasabb rendű függvényeket és a kötött változókat. Az elsőrendű TRS-ekre vonatkozó különböző eredmények a HRS-ekre is átformálhatók.

Grafikon átíró rendszerek

Graph újraírása rendszerek egy másik általánosítása távú újraírása rendszerek, működő grafikonok helyett ( őrölt -) kifejezések / a megfelelő fa ábrázolása.

Nyomkövetési átíró rendszerek

A nyomkövetés elve lehetővé teszi a többfeldolgozás formálisabb megvitatását, például a nyomkövetési monoidon és a történelemmonoidon keresztül . Az átírás nyomkövető rendszerekben is elvégezhető.

Filozófia

Az átírási rendszereket olyan programoknak tekinthetjük, amelyek az ok-okozati összefüggések listájából következtetnek a véghatásokra. Ily módon az átírási rendszereket automatikus ok -okozati bizonyítóknak tekinthetjük.

Lásd még

• Kritikus pár (logika)
• Fordítóprogram
• Knuth – Bendix befejezési algoritmus
• Az L-rendszerek az átírást határozzák meg, amely párhuzamosan történik.
• Referenciális átláthatóság az informatikában
• Szabályozott átírás
• Rho számítás

Megjegyzések

Hivatkozások

További irodalom

• Baader, Franz ; Nipkow, Tobias (1999). Kifejezések átírása és minden . Cambridge University Press. ISBN 978-0-521-77920-3.316 oldal. Egyetemistáknak megfelelő tankönyv.
• Marc Bezem , Jan Willem Klop , Roel de Vrijer ("Terese"), Term Rewriting Systems ("TeReSe"), Cambridge University Press, 2003, ISBN  0-521-39115-6 . Ez a legújabb átfogó monográfia. Ugyanakkor számos, nem szabványos jelölést és meghatározást használ. Például az Egyház – Rosser tulajdonság azonos az összefolyással.
• Nachum Dershowitz és Jean-Pierre Jouannaud "Rewrite Systems" , 6. fejezet, Jan van Leeuwen (szerk.), Az elméleti számítástechnika kézikönyve , B kötet: Formális modellek és szemantika. , Elsevier és MIT Press, 1990, ISBN  0-444-88074-7 , 243–320. Ennek a fejezetnek az előnyomata szabadon hozzáférhető a szerzőknél, de hiányoznak az ábrák.
• Nachum Dershowitz és David Plaisted . "Újraírás" , 9. fejezet John Alan Robinson és Andrei Voronkov (szerk.), Handbook of Automated Reasoning , 1. kötet .
• Gérard Huet et Derek Oppen, Equations and Rewrite Rules, A Survey (1980) Stanford Verification Group, Report No. 15 Computer Science Department Report No. STAN-CS-80-785
• Jan Willem Klop . "Term Rewriting Systems", 1. fejezet Samson Abramsky , Dov M. Gabbay és Tom Maibaum (szerk.), Handbook of Logic in Computer Science , 2. kötet: Background: Computational Structures .
• David Plaisted. " Egyenlő érvelési és kifejezés -átírási rendszerek" , Dov M. Gabbay , CJ Hogger és John Alan Robinson (szerk.), Handbook of Logic in Artificial Intelligence and Logic Programming , Volume 1 .
• Jürgen Avenhaus és Klaus Madlener. "Kifejezések átírása és egyenlőségi érvelés". In Ranan B. Banerji (szerk.), Formal Techniques in Artificial Intelligence: A Sourcebook , Elsevier (1990).

Karakterlánc átírás

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

Egyéb

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

Külső linkek

• Az átírás kezdőlapja
• IFIP munkacsoport 1.6
• Kutatók átírása által Aart Middeldorp , az Innsbrucki Egyetem
• Megszüntetési portál