Omskrivning

Omskrivning  - en bred vifte af teknikker, metoder og teoretiske resultater forbundet med procedurerne for sekventiel udskiftning af dele af formler eller termer i et formelt sprog i henhold til et givet skema - et system af omskrivningsregler . I sin mest generelle form taler vi om samlingen af ​​et bestemt sæt af objekter og regler - forholdet mellem disse objekter, der indikerer, hvordan man transformerer dette sæt.

Omskrivningen kan være ikke-deterministisk. For eksempel kan et system med omskrivningsregler omfatte en regel, der kan anvendes på det samme udtryk på flere forskellige måder, men som ikke på samme tid indeholder en indikation af, hvilken bestemt metode, der skal anvendes i et bestemt tilfælde. Hvis omskrivningssystemet ikke desto mindre er indrammet som en utvetydigt forstået algoritme, kan det betragtes som et computerprogram. En række interaktive teorembevissystemer [1] og deklarative programmeringssprog [2] [3] er baseret på omskrivningsteknikker .

Grundlæggende begreber og eksempler

Hovedegenskaberne ved omskrivningssystemer kan formuleres uden at ty til en specifik implementering af dem i form af operationer på vilkår. Til dette bruges ofte konceptet Abstract Reduction System eller ARS (fra det engelske  Abstract Reduction Systems ) . ARS består af et sæt A og et sæt binære relationer på det, som kaldes reduktioner . A siges at blive reduceret eller omskrevet til b i et trin i forhold til den givne ARS, hvis parret ( a , b ) tilhører nogle . De vigtigste egenskaber ved reduktionssystemer er:

Det er klart, at sammenløb indebærer svagt sammenløb, og stop, henholdsvis svagt stop. Sammenløb og stop hænger dog ikke sammen. For eksempel er et system bestående af én regel a•b → b•a sammenflydende, men ikke standsende. Et system bestående af to regler a → b og a → c er stoppende, men ikke sammenflydende, og alle tre regler danner tilsammen et system, der hverken er stoppende eller konfluent.

Et reduktionssystems standsende natur gør det muligt at tildele hvert element dets normale form  - et element, som det kan reduceres til, men som i sig selv ikke længere er reduceret. Hvis der desuden observeres konfluens, vil en sådan normal form altid være unik eller kanonisk . I denne henseende er Church-Rosser-ejendommen særlig værdifuld, da den giver dig mulighed for hurtigt og effektivt at løse problemet med ligheden mellem to elementer a og b med hensyn til systemet af ligheder svarende til sættet af reduktioner uden hensyn til retning . For at gøre dette er det tilstrækkeligt at beregne de normale former for begge elementer. Da normalformen i dette tilfælde også vil være kanonisk, vil elementerne være ens, hvis og kun hvis resultaterne stemmer overens.

Klassisk omskrivningsteori

Selvom begrebet omskrivning oprindeligt blev introduceret for lambda-regningen , vedrører hovedparten af ​​resultaterne og applikationerne i øjeblikket første-ordens omskrivning. Omskrivningssystemer af denne art kaldes Term Rewriting Systems eller TRS (fra engelsk.  Term rewriting systems ).

Se også

Noter

  1. ↑ Jieh Hsiang, Helène Kirchner, Pierre Lescanne, Michaël Rusinowitch. Termen omskrivningstilgang til automatiseret teorembevis  //  The Journal of Logic Programming. — 1992-10-01. — Bd. 14 , udg. 1 . — S. 71–99 . — ISSN 0743-1066 . - doi : 10.1016/0743-1066(92)90047-7 . Arkiveret 6. maj 2021.
  2. ↑ Teori og praksis for begrænsningsregler  //  The Journal of Logic Programming. — 1998-10-01. — Bd. 37 , udg. 1-3 . — S. 95–138 . — ISSN 0743-1066 . - doi : 10.1016/S0743-1066(98)10005-5 . Arkiveret fra originalen den 5. juli 2022.
  3. ↑ Maude: specifikation og programmering i omskrivningslogik  //  Teoretisk datalogi. - 2002-08-28. — Bd. 285 , udg. 2 . — S. 187–243 . — ISSN 0304-3975 . - doi : 10.1016/S0304-3975(01)00359-0 . Arkiveret fra originalen den 7. marts 2022.