Az elméleti számítógép-tudomány , újraírás (vagy átírásával ) egy számítógépes modellt , amelyben arról van szó, átalakításának szintaktikai tárgyak ( szavak , kifejezések , lambda-kifejezések, programok , igazolások , grafikonok , stb) alkalmazásával nagyon pontos szabályokat..
Az átírást az informatikában , az algebrában , a matematikai logikában és a nyelvészetben használják . Az átírást a gyakorlatban használják az e-mailek kezelésére (a sendmail szoftverben az e- mail fejléceket átírási rendszerek kezelik) vagy a kódgenerálásra és az optimalizálásra a fordítókban .
Íme néhány klasszikus példa az átírás használatára:
Az átírási rendszer az r → r ' alakú átírási szabályok összessége . Egy ilyen szabály vonatkozik a szintaktikus objektumot t , ha az utóbbi tartalmaz egy például a bal tag R , azaz egy al-objektum, amely azonosítható r . A tárgy t van , majd átírt egy új objektumot t „kapott helyett a példány r által megfelelő példánya a jobb tag R” . Jelölés: t → t ' .
Ezt az általános elvet elmagyarázzuk az átírás három klasszikus keretének mindegyikében.
Ilyen szabály vonatkozik a t szóra, ha az urv alakú, ahol u és v bármely (esetleg üres) szó. A t szót ezután átírják az ur'v-be . Más szóval, mi vonatkozik a szabály R → R " a keretében alakult előtag u és az utótag v . Példa: u = a és v = bc esetén aabbc → acaabc-t kapunk .
A bal oldali példány egy olyan s tagszó, amelyet úgy kapunk, hogy r változóit bármilyen kifejezéssel helyettesítjük. A megfelelő tag megfelelő példányát úgy kapjuk meg, hogy r ' változóit ugyanazokkal a feltételekkel helyettesítjük. Példa: (x + 0) (x + 1) az x (y + z) példánya, az x y + x z megfelelő példánya pedig (x + 0) x + (x + 0) 1 . Tehát van (x + 0) · (x + 1) → (x + 0) · x + (x + 0) · 1 , és ((x + 0) · (x + 1)) + y → ( (x + 0) x + (x + 0) 1) + y .
Megjegyzés: Ha az aláírás csak egynemű műveleti szimbólumokból áll, akkor minden szabály egyetlen változót tartalmaz, amely egyszer balra, egyszer pedig jobbra jelenik meg. Példa: a (b (x)) → c (a (a (x))) . Így a szavak átírása a kifejezések átírásának speciális esete.
A lambda-számítás mind a kiszámíthatóság modellje, mind az összes funkcionális programozási nyelv prototípusa, mind pedig a természetes dedukcióhoz szükséges vágások megszüntetésének tipizálatlan változata . Valójában a másodrendű kifejezések átírásának speciális esete . A fő különbség az előző kerettel szemben az, hogy a kifejezések kapcsolódó változókat tartalmaznak, amelyek finomabbá teszik a helyettesítési mechanizmust.
Jelölés: ha t 0 → t 1 → t 2 → ··· → t n , akkor t 0 → * t n- t írunk . Más szóval, a → * a tranzitív reflexív bezárását a → .
Definíció: ha nincs szabály vonatkozik t , azt mondjuk, hogy t is kiküszöbölhetetlen vagy normál formában , és ha t → * u , ahol u jelentése az általános formában, azt mondjuk, hogy u egy szokásos formája t .
Azt mondjuk, hogy az átírási rendszer nem éteri , vagy kielégíti a befejező tulajdonságot , ha nincs végtelen szekvencia t 0 → t 1 → t 2 → ··· → t n → ···
Példák (szavak átírása):
Általánosságban elmondható, hogy a felmondási tulajdonság egy felmondási megbízás , azaz egy megalapozott szigorú sorrend összeállításával < oly módon mutat be, hogy t → t ' t> t' implikál .
Noetherian esetben minden objektumnak normális formája van. Ezenkívül van egy noetheri indukciós elvünk : ha minden t esetében a P (t) tulajdonság igaz, amikor minden t ' -re P (t') van, úgy, hogy t → t ' , akkor P (t) igaz mindenre t .
Megjegyzés: A (véges) szóírási rendszer megszüntetési tulajdonsága eldönthetetlen probléma . Ugyanez vonatkozik a ciklusok hiányára is.
Terminológia: A terminációt néha erős normalizációnak is nevezik például a lambda-calculusban .
Az átírás nem determinisztikus jellege azt jelenti, hogy több szabály is alkalmazható ugyanarra az objektumra, így több különböző eredményt érhet el.
Egy adott átírási rendszer esetében az összefolyás tulajdonság a következőképpen van megadva: ha t → * u és t → * v , akkor létezik olyan w , hogy u → * w és v → * w . Ez megegyezik a Church-Rosser tulajdonával .
Példák (szavak átírása):
A Noetherian-ügyben Newman lemma szerint az összefolyás egyenértékű a helyi összefolyással , amelyet gyenge összefolyásnak is nevezünk : ha t → u és t → v , akkor létezik olyan w , hogy u → * w és v → * w .
A véget érő és összefolyó átírási rendszerről azt mondják, hogy konvergens . Ebben az esetben már a létezése és egyedisége a szokásos formában , úgy, hogy a szöveges feladat is eldönthető , legalábbis akkor, ha a rendszer véges.
Megjegyzés: Noetherian-ügyben egy (véges) szó vagy kifejezés átírási rendszer összefolyási tulajdonsága eldönthető probléma . Valójában elegendő egy kritikus párnak nevezett véges számú konfiguráció összefolyásának tesztelése . Például az ab → ε és a ba → ε két szabály által alkotott rendszer esetében elegendő az aba és a bab szavak helyi összefolyásának tulajdonságát ellenőrizni . Ezek a kritikus párok analógak a kommutatív algebrában használt Gröbner-bázisokkal .
Ha az átírási rendszer Noether-típusú, de nem összefolyó, megpróbáljuk konvergenssé tenni a Knuth-Bendix befejezési eljárás segítségével .
Szóírás esetén az átírási rendszer meghatározza a generátorok bemutatását és a monoid viszonyait . Ez monoid a hányados Σ * / * ↔ , ahol Σ * a szabad monoid által generált ábécé Σ és ↔ * a kongruencia által generált újraírás szabályok, vagyis a reflexív, szimmetrikus és tranzitív a → . Példa: Z = Σ * / ↔ * ahol Σ = {a, b} az ab → ε és a ba → ε két szabállyal ( szabad csoport egy generátorral).
Mivel az M monoidnak sok prezentációja van, érdekelnek bennünket az invariánsok , vagyis az M monoid belső tulajdonságai , amelyek nem függenek a prezentáció megválasztásától. Példa: A eldönthetőség a szó probléma az M .
Egy finoman prezentálható M monoidnak eldönthető szövegproblémája lehet, de véges konvergens átírási rendszer nem mutat be. Valóban, ha van ilyen rendszer, a H (M) homológ csoport véges típusú. Most összeállíthatunk egy végérvényesen bemutatható monoidot, amelynek szóproblémája eldönthető és olyan, hogy a H (M) csoport nem véges típusú.
Valójában ezt a csoportot a kritikus párok generálják , és általában véve a konvergens átírási rendszer lehetővé teszi a monoid homológiájának kiszámítását bármely dimenzióban. Vannak homotóp invariánsok is : ha létezik konvergens átírási rendszer egy monoidra, akkor megmutatjuk, hogy ennek véges levezetési típusa van . Ez megint egy olyan tulajdonság, amelyet egy (véges) prezentáció határoz meg, de nem függ a bemutató választásától. Ez a tulajdonság azt jelenti, hogy a H (M) csoport véges típusú, de fordítva nem igaz.
Egy szó, mint például aabbc is értelmezhető, mint egy utat a grafikonon , amely egyetlen csúcs, amelynek egyik széle az egyes szimbólumokra a, b, c . Ha bármelyik gráfból indulunk ki, akkor egy monoid helyett egy kategóriát kapunk . Az olyan számításokat, mint az aabbc → acaabc → acacaac , ezután az utak közötti útként értelmezhetjük , más néven 2-utat :
Ez a megjegyzés azt sugallja általánosítása átírásának szavakat, ahol a tárgyak 2-utak, amely szintén képviseli sík diagramok :
Kiderült, hogy az újraírás kifejezések lehet fordítani egy ilyen rendszerben, azzal a feltétellel bevezetésének explicit műveletek párhuzamos , törlés és cseréje (analóg szerkezeti szabályokat a kiszámítása sequents ):
De ez a megközelítés sokkal általánosabb, mint a kifejezések átírása. Íme néhány olyan terület, ahol egy ilyen formalizmus alkalmazható:
Végül megvizsgálhatjuk az n- utak átírását, amely n + 1- utak felépítéséből áll. Ehhez használjuk a elmélet kategóriák és poligráf (más néven computades ), amely meghatározza a hidat elméleti számítási és algebrai topológia .
Az első átíráson alapuló nyelv a Hope , Burstall, McQueen és Sanella miatt, bár két ős megtalálható Burge és O'Donnell műveiben. Azóta számos programozási nyelv az átírást tekinti belső mechanizmusnak, köztük az ASF + SDF , az ELAN , a Maude , a Stratego és a Tom . Ez utóbbi azért érdekes, mert összekeveri az átírásból származó konstrukciókat a Java nyelvvel .
Bár tartozó kategóriába funkcionális nyelvek , Haskell és OCaml is támaszkodnak alapelve újraírása: minta szűrés .
(hu) A honlap átírása