Přepisování

Přepisování  - široká škála technik, metod a teoretických výsledků spojených s postupy postupného nahrazování částí vzorců nebo termínů formálního jazyka podle daného schématu - systém přepisovacích pravidel . V nejobecnější podobě mluvíme o sbírce určité množiny objektů a pravidel – vztahů mezi těmito objekty, které naznačují, jak tuto množinu transformovat.

Přepis může být nedeterministický. Například systém pravidel přepisování může zahrnovat pravidlo, které lze použít na stejný termín několika různými způsoby, ale zároveň neobsahuje údaj o tom, která konkrétní metoda by měla být v konkrétním případě použita. Pokud je však přepisovací systém koncipován jako jednoznačně srozumitelný algoritmus, lze jej považovat za počítačový program. Řada interaktivních systémů pro dokazování teorémů [1] a deklarativních programovacích jazyků [2] [3] je založena na technikách přepisování .

Základní pojmy a příklady

Hlavní vlastnosti přepisovacích systémů lze formulovat, aniž bychom se uchýlili k jejich specifické implementaci ve formě operací na podmínkách. K tomu se často používá koncept Abstract Reduction System nebo ARS (z anglického  Abstract Reduction Systems ) . ARS se skládá z nějaké množiny A a na ní množiny binárních relací , které se nazývají redukce . Říká se, že A je redukováno nebo přepsáno na b v jednom kroku vzhledem k danému ARS, pokud pár ( a , b ) patří k nějakému . Nejdůležitější vlastnosti redukčních systémů jsou:

Je zřejmé, že soutok znamená slabý soutok, respektive zastavení slabé zastavení. Soutok a zastavení však spolu nesouvisí. Například systém skládající se z jednoho pravidla a•b → b•a je splývající, ale nezastavuje se. Systém sestávající ze dvou pravidel a → b a a → c se zastavuje, ale nesplývají, a všechna tři pravidla dohromady tvoří systém, který není ani zastavující, ani nesplývající.

Zastavující povaha redukčního systému umožňuje přiřadit každému prvku jeho normální formu  — prvek, na který může být redukován, ale který sám již není redukován. Pokud je navíc pozorována konfluence, pak bude taková normální forma vždy jedinečná nebo kanonická . V tomto ohledu je vlastnost Church-Rosser zvláště cenná, protože umožňuje rychle a efektivně vyřešit problém rovnosti dvou prvků a a b s ohledem na systém rovnosti odpovídající množině snížení bez ohledu na směr. . K tomu stačí vypočítat normální tvary obou prvků. Vzhledem k tomu, že v tomto případě bude normální tvar také kanonický, prvky se budou rovnat pouze tehdy, když se výsledky shodují.

Klasická teorie přepisování

Ačkoli pojem přepisování byl původně zaveden pro lambda kalkul , většina výsledků a aplikací se v současnosti týká přepisování prvního řádu. Přepisovací systémy tohoto druhu se nazývají Term Rewriting Systems nebo TRS (z angl.  Term rewriting systems ).

Viz také

Poznámky

  1. ↑ Jieh Hsiang, Helène Kirchner, Pierre Lescanne, Michaël Rusinowitch. Termín přepisovací přístup k automatizovanému dokazování teorémů  //  The Journal of Logic Programming. — 10.10.1992. — Sv. 14 , iss. 1 . — S. 71–99 . — ISSN 0743-1066 . - doi : 10.1016/0743-1066(92)90047-7 . Archivováno 6. května 2021.
  2. ↑ Teorie a praxe pravidel manipulace s omezeními  //  The Journal of Logic Programming. — 10. 10. 1998. — Sv. 37 , iss. 1-3 . — S. 95–138 . — ISSN 0743-1066 . - doi : 10.1016/S0743-1066(98)10005-5 . Archivováno z originálu 5. července 2022.
  3. ↑ Maude: specifikace a programování v přepisovací logice  //  Teoretická informatika. - 28. 8. 2002. — Sv. 285 , iss. 2 . — S. 187–243 . — ISSN 0304-3975 . - doi : 10.1016/S0304-3975(01)00359-0 . Archivováno z originálu 7. března 2022.