Uudelleenkirjoittaminen

Uudelleenkirjoitus  - laaja valikoima tekniikoita, menetelmiä ja teoreettisia tuloksia, jotka liittyvät muodollisen kielen kaavojen tai termien osien peräkkäiseen korvaamiseen tietyn järjestelmän mukaisesti - uudelleenkirjoitussääntöjen järjestelmä . Yleisimmässä muodossaan puhumme tietyn objektien ja sääntöjen kokoelmasta - näiden objektien välisistä suhteista, jotka osoittavat, kuinka tämä joukko muutetaan.

Uudelleenkirjoitus voi olla epädeterministinen. Esimerkiksi uudelleenkirjoitussääntöjen järjestelmä voi sisältää säännön, jota voidaan soveltaa samaan termiin usealla eri tavalla, mutta joka ei sisällä samaan aikaan viittausta siitä, mitä menetelmää tietyssä tapauksessa tulisi soveltaa. Jos uudelleenkirjoitusjärjestelmä on kuitenkin kehystetty yksiselitteisesti ymmärrettäväksi algoritmiksi, sitä voidaan pitää tietokoneohjelmana. Useat interaktiiviset lauseiden todistamisjärjestelmät [1] ja deklaratiiviset ohjelmointikielet [2] [3] perustuvat uudelleenkirjoitustekniikoihin .

Peruskäsitteet ja esimerkit

Uudelleenkirjoitusjärjestelmien tärkeimmät ominaisuudet voidaan muotoilla turvautumatta niiden erityiseen toteutukseen operaatioiden muodossa. Tätä varten käytetään usein käsitettä Abstract Reduction System tai ARS ( englanninkielisestä  Abstract Reduction Systemsistä ) . ARS koostuu joukosta A ja joukosta siinä olevia binäärisuhteita , joita kutsutaan vähennyksiksi . A:n sanotaan pienennettävän tai kirjoitetun uudelleen b : ksi yhdessä vaiheessa suhteessa annettuun ARS:iin, jos pari ( a , b ) kuuluu johonkin . Pelkistysjärjestelmien tärkeimmät ominaisuudet ovat:

On selvää, että yhtymä tarkoittaa heikkoa yhtymäkohtaa ja pysähtyminen, vastaavasti, heikkoa pysähtymistä. Yhtymä ja pysähtyminen eivät kuitenkaan liity toisiinsa. Esimerkiksi järjestelmä, joka koostuu yhdestä säännöstä a•b → b•a, on konfluentti, mutta ei pysähtyvä. Järjestelmä, joka koostuu kahdesta säännöstä a → b ja a → c , on pysähtyvä, mutta ei yhtyvä, ja kaikki kolme sääntöä yhdessä muodostavat järjestelmän, joka ei ole pysähtyvä eikä yhtyvä.

Pelkistysjärjestelmän pysäytysluonne mahdollistaa sen, että jokaiselle elementille voidaan määrittää sen normaalimuoto  - elementti, johon se voidaan pelkistää, mutta jota itse ei enää pelkistetä. Jos lisäksi havaitaan konfluenssi, niin tällainen normaalimuoto on aina ainutlaatuinen tai kanoninen . Tässä suhteessa Church-Rosserin ominaisuus on erityisen arvokas, koska sen avulla voit nopeasti ja tehokkaasti ratkaista kahden elementin a ja b yhtäläisyyden ongelman suhteessa yhtäläisyysjärjestelmään, joka vastaa vähennysjoukkoa ilman suuntaa . Tätä varten riittää laskea molempien elementtien normaalimuodot. Koska tässä tapauksessa normaalimuoto on myös kanoninen, elementit ovat samanarvoisia silloin ja vain, jos tulokset täsmäävät.

Klassinen uudelleenkirjoitusteoria

Vaikka uudelleenkirjoituksen käsite otettiin alun perin käyttöön lambda-laskennassa , suurin osa tuloksista ja sovelluksista koskee tällä hetkellä ensimmäisen asteen uudelleenkirjoitusta. Tällaisia ​​uudelleenkirjoitusjärjestelmiä kutsutaan termien uudelleenkirjoitusjärjestelmiksi tai TRS :ksi ( englanniksi  Term rewriting systems ).

Katso myös

Muistiinpanot

  1. ↑ Jieh Hsiang, Helène Kirchner, Pierre Lescanne, Michaël Rusinowitch. Termi uudelleenkirjoitus lähestymistapa automatisoituun lauseen todistamiseen  //  The Journal of Logic Programming. - 1992-10-01. — Voi. 14 , iss. 1 . — s. 71–99 . — ISSN 0743-1066 . - doi : 10.1016/0743-1066(92)90047-7 . Arkistoitu 6. toukokuuta 2021.
  2. ↑ Rajoitusten käsittelysääntöjen teoria ja käytäntö  //  The Journal of Logic Programming. - 1998-10-01. — Voi. 37 , iss. 1-3 . — s. 95–138 . — ISSN 0743-1066 . - doi : 10.1016/S0743-1066(98)10005-5 . Arkistoitu alkuperäisestä 5. heinäkuuta 2022.
  3. ↑ Maude: määritys ja ohjelmointi uudelleenkirjoituslogiikassa  //  Teoreettinen tietojenkäsittelytiede. - 28.8.2002. — Voi. 285 , iss. 2 . — s. 187–243 . — ISSN 0304-3975 . - doi : 10.1016/S0304-3975(01)00359-0 . Arkistoitu alkuperäisestä 7. maaliskuuta 2022.