Normální forma (abstraktní přepisování) - Normal form (abstract rewriting)

Při abstraktním přepisování je předmět v normální podobě, pokud jej nelze dále přepisovat, tj. Je neredukovatelný. V závislosti na systému přepisování se může objekt přepsat do několika normálních formulářů nebo vůbec. Mnoho vlastností přepisovacích systémů se týká normálních forem.

Definice

Formálně řečeno, pokud ( A , →) je abstraktní přepisovací systém , x ∈ A je v normální formě, pokud neexistuje žádné y ∈ A takové, že x → y , tj. X je neredukovatelný termín.

Objekt a se slabě normalizuje, pokud existuje alespoň jedna konkrétní sekvence přepisů počínaje a, která nakonec poskytne normální formu. Přepisovací systém má vlastnost slabé normalizace nebo se (slabě) normalizuje (WN), pokud se každý objekt slabě normalizuje. Objekt je silně normalizací jestliže každé sekvence přepsání počínaje nakonec končí s normální formě. Abstraktní přepisovací systém silně normalizuje , končí , je noetherový nebo má (silnou) normalizační vlastnost (SN), pokud se každý z jeho objektů silně normalizuje.

Přepisování systém má normální tvar vlastnost (NF), jestliže pro všechny objekty A a normální formy B , b může být dosaženo z sérií přepsání a inverzních přepsání pouze v případě, snižuje až b . Přepisování systém má jedinečnou vlastnost normální forma (OSN), jestliže pro všechny obvyklé formy několika , b ∈ S , může být dosaženo z b sérií přepsání a inverzních přepsání pouze v případě, se rovná b . Přepisování systém má jedinečnou vlastnost normální tvar s ohledem na snížení (UN ^→ ), pokud pro každý termín snížení do normálních forem a , b , se rovná b .

Výsledek

Tato část představuje některé dobře známé výsledky. Za prvé, SN znamená WN.

Confluence (zkráceně CR) znamená NF implikuje OSN implikuje OSN ^→ . Opačné implikace obecně neplatí. {a → b, a → c, c → c, d → c, d → e} je UN ^→, ale ne OSN, protože b = e a b, e jsou normální tvary. {a → b, a → c, b → b} je UN, ale ne NF, protože b = c, c je normální forma a b se nesnižuje na c. {a → b, a → c, b → b, c → c} je NF, protože neexistují žádné normální formy, ale ne CR jako a redukuje na b a c, a b, c nemají žádnou společnou redukci.

WN a OSN ^→ znamenají soutok. CR, NF, OSN a OSN ^{→ se tedy} shodují, pokud WN platí.

Příklady

Například pomocí systému přepisování výrazu s jediným pravidlem g ( x , y ) → x lze výraz g ( g (4,2), g (3,1)) přepsat následujícím způsobem, přičemž se pravidlo použije na nejvzdálenější výskyt g :

g ( g (4,2), g (3,1)) → g (4,2) → 4.

Protože na poslední výraz 4 neplatí žádné pravidlo, nelze jej dále přepisovat, a je tedy normální formou výrazu g ( g (4,2), g (3,1)) s ohledem na tento systém přepisování termínů . Systém pravidel se silně normalizuje, protože každá aplikace pravidel správně zmenšuje velikost výrazu, a proto nemůže existovat nekonečná posloupnost přepisů začínající od jakéhokoli výrazu. Naproti tomu systém dvou pravidel { g ( x , y ) → x , g ( x , x ) → g (3, x )} se slabě, ale ne silně normalizuje, přestože každý výraz neobsahuje g (3,3 ) se silně normalizuje. Termín g (4,4) má v tomto systému dvě normální formy, tj. g (4,4) → 4 a g (4,4) → g (3,4) → 3, systém proto není splývavý .

Další příklad: Systém s jedním pravidlem { r ( x , y ) → r ( y , x )} nemá žádné normalizační vlastnosti (ani slabě ani silně), protože z libovolného výrazu, např. R (4,2), jedna přepisovací sekvence začíná, tzn. r (4,2) → r (2,4) → r (4,2) → r (2,4) → ..., což je nekonečně dlouhé.

Netypický lambda kalkul

Čistá bez typu lambda kalkulu nesplňuje silným normalizace majetek, a dokonce ani slabé normalizace vlastnost. Zvažte termín . Má následující pravidlo přepisu: Pro jakýkoli výraz , ${\ Displaystyle \ lambda x.xxx}$ ${\ displaystyle t}$

{\ Displaystyle (\ mathbf {\ lambda} x.xxx) t \ rightarrow ttt}

Ale zvažte, co se stane, když aplikujeme na sebe: ${\ Displaystyle \ lambda x.xxx}$

{\ Displaystyle {\ begin {aligned} (\ mathbf {\ lambda} x.xxx) (\ lambda x.xxx) & \ rightarrow (\ mathbf {\ lambda} x.xxx) (\ lambda x.xxx) (\ lambda x.xxx) \\ & \ rightarrow (\ mathbf {\ lambda} x.xxx) (\ lambda x.xxx) (\ lambda x.xxx) (\ lambda x.xxx) \\ & \ rightarrow (\ mathbf {\ lambda} x.xxx) (\ lambda x.xxx) (\ lambda x.xxx) (\ lambda x.xxx) (\ lambda x.xxx) \\ & \ rightarrow \ \ cdots \, \ end {zarovnáno }}}

Tento termín proto není ani silně, ani slabě normalizující. ${\ Displaystyle (\ lambda x.xxx) (\ lambda x.xxx)}$

Psaný lambda kalkul

Různé systémy zadaný lambda kalkulu včetně prostě napsané lambda kalkulu , Jean-Yves Girard ‚s System F a Thierry Coquand ‘ s kalkul staveb jsou silně normalizace.

Systém lambda kalkulu s vlastností normalizace lze považovat za programovací jazyk s vlastností, kterou každý program ukončí . Ačkoli je to velmi užitečná vlastnost, má jednu nevýhodu: programovací jazyk s vlastností normalizace nemůže být Turing dokončen , jinak by bylo možné problém se zastavením vyřešit tím, že se podíváme, jestli program kontroluje typ. To znamená, že existují vyčíslitelné funkce, které nelze definovat v jednoduše napsaném lambda kalkulu (a podobně existují vyčíslitelné funkce, které nelze vypočítat v počtu konstrukcí nebo systému F ), například autointerpret .

Viz také

Poznámky

Reference

Baader, Franz ; Nipkow, Tobias (1998). Přepisování termínů a vše ostatní . Cambridge University Press. ISBN 9780521779203.

Languages

In other projects