Átírás

Újraírás  - technikák, módszerek és elméleti eredmények széles skálája, amelyek egy formális nyelv képletei vagy kifejezéseinek egy adott séma szerinti szekvenciális cseréjéhez kapcsolódnak - átírási szabályok rendszere . A legáltalánosabb formájában bizonyos objektumok és szabályok gyűjteményéről beszélünk - az objektumok közötti kapcsolatokról, amelyek jelzik, hogyan kell átalakítani ezt a halmazt.

Az átírás lehet nem determinisztikus. Például egy átírási szabályrendszer tartalmazhat olyan szabályt, amely ugyanarra a kifejezésre többféleképpen is alkalmazható, de ugyanakkor nem tartalmaz utalást arra vonatkozóan, hogy egy adott esetben melyik módszert kell alkalmazni. Ha az átíró rendszer ennek ellenére egyértelműen értelmezett algoritmusként van kialakítva, akkor számítógépes programnak tekinthető. Számos interaktív tételbizonyító rendszer [1] és deklaratív programozási nyelv [2] [3] alapszik újraírási technikákon .

Alapfogalmak és példák

Az átíró rendszerek fő tulajdonságai úgy fogalmazhatók meg, hogy nem folyamodnának konkrét megvalósításukhoz feltételeken alapuló műveletek formájában. Ehhez gyakran használják az Abstract Reduction System vagy ARS (az angol  Abstract Reduction Systems szóból ) fogalmát. Az ARS néhány A halmazból és azon lévő bináris relációk halmazából áll , amelyeket redukcióknak nevezünk . Az A - t egy lépésben redukáljuk vagy átírjuk b - re az adott ARS-hez képest, ha az ( a , b ) pár valamelyikhez tartozik . A redukciós rendszerek legfontosabb tulajdonságai:

Nyilvánvaló, hogy az összefolyás gyenge összefolyást, illetve megállást, gyenge megállást jelent. Az összefolyás és a megállás azonban nincs összefüggésben. Például egy a•b → b•a szabályból álló rendszer konfluens, de nem leáll. A két a → b és a → c szabályból álló rendszer megáll, de nem összefolyó, és mindhárom szabály együttesen egy olyan rendszert alkot, amely sem nem megáll, sem nem összefolyó.

A redukciós rendszer megállító jellege lehetővé teszi, hogy minden elemhez hozzárendeljük a normális formáját – egy olyan  elemet, amelyvé redukálható, de amely önmagában már nem redukálódik. Ha ezen felül egybefolyást is megfigyelünk, akkor egy ilyen normál forma mindig egyedi vagy kanonikus lesz . Ebből a szempontból a Church-Rosser tulajdonság különösen értékes, mivel lehetővé teszi, hogy gyorsan és hatékonyan megoldja a két a és b elem egyenlőségének problémáját a redukciók halmazának megfelelő egyenlőségrendszer tekintetében, az iránytól függetlenül. . Ehhez elegendő mindkét elem normál alakját kiszámítani. Mivel ebben az esetben a normál forma is kanonikus lesz, az elemek akkor és csak akkor lesznek egyenlők, ha az eredmények egyeznek.

Klasszikus átíráselmélet

Bár az újraírás fogalmát eredetileg a lambda-számításhoz vezették be , az eredmények és alkalmazások nagy része jelenleg az elsőrendű átírásra vonatkozik. Az ilyen típusú újraíró rendszereket Term Rewriting Systemsnek vagy TRS -nek (az angol  szóból Term rewriting systems ) nevezik.

Lásd még

Jegyzetek

  1. ↑ Jieh Hsiang, Helène Kirchner, Pierre Lescanne, Michaël Rusinowitch. A kifejezés újraírási megközelítése az automatizált tételbizonyításhoz  //  The Journal of Logic Programming. — 1992-10-01. — Vol. 14 , iss. 1 . — P. 71–99 . — ISSN 0743-1066 . - doi : 10.1016/0743-1066(92)90047-7 . Archiválva : 2021. május 6.
  2. ↑ A kényszerkezelési szabályok elmélete és gyakorlata  //  The Journal of Logic Programming. — 1998-10-01. — Vol. 37 , iss. 1-3 . — P. 95–138 . — ISSN 0743-1066 . - doi : 10.1016/S0743-1066(98)10005-5 . Archiválva az eredetiből 2022. július 5-én.
  3. ↑ Maude: specifikáció és programozás az újraírási logikában  //  Elméleti számítástechnika. - 2002-08-28. — Vol. 285 , iss. 2 . — P. 187–243 . — ISSN 0304-3975 . - doi : 10.1016/S0304-3975(01)00359-0 . Archiválva az eredetiből 2022. március 7-én.