Sökvägsordning (termomskrivning)
Inom teoretisk datavetenskap , särskilt i termomskrivning , är en vägordning en välgrundad strikt totalordning (>) på uppsättningen av alla termer så att
- f (...) > g ( s 1 ,..., s n ) om f . > g och f (...) > si för i = 1,..., n ,
där ( . >) är en användargiven total prioritetsordning på uppsättningen av alla funktionssymboler .
Intuitivt är en term f (...) större än någon term g (...) byggd av termer s i mindre än f (...) med en rotsymbol g med lägre prioritet . I synnerhet genom strukturell induktion är en term f (...) större än någon term som bara innehåller symboler som är mindre än f .
En sökvägsordning används ofta som reduktionsordning i termomskrivning, särskilt i Knuth–Bendix-kompletteringsalgoritmen . Som ett exempel kan ett termomskrivningssystem för att " multiplicera ut " matematiska uttryck innehålla en regel x *( y + z ) → ( x * y ) + ( x * z ). För att bevisa uppsägning måste en reduktionsordning (>) hittas med avseende på vilken termen x *( y + z ) är större än termen ( x * y )+( x * z ). Detta är inte trivialt, eftersom den förra termen innehåller både färre funktionssymboler och färre variabler än den senare. Ange dock prioritet (*) . > (+), kan en sökvägsordning användas, eftersom både x *( y + z ) > x * y och x *( y + z ) > x * z är lätta att uppnå.
Det kan också finnas system för vissa generella rekursiva funktioner , till exempel kan ett system för Ackermann-funktionen innehålla regeln A( a + , b + ) → A( a , A( a + , b )), där b + betecknar efterträdare till b .
Givet två termer s och t , med en rotsymbol f respektive g , för att bestämma deras relation jämförs deras rotsymboler först.
- Om f < . g , då kan s dominera t endast om en av s: s undertermer gör det.
- Om f . > g , då dominerar s t om s dominerar var och en av ts deltermer.
- Om f = g måste de omedelbara deltermerna för s och t jämföras rekursivt. Beroende på den speciella metoden finns olika variationer av banordningar.
De senare varianterna inkluderar:
- multiset vägordning ( mpo ), ursprungligen kallad rekursiv vägordning ( rpo )
- den lexikografiska vägordningen ( lpo )
- en kombination av mpo och lpo, kallad rekursiv vägordning av Dershowitz, Jouannaud (1990)
Dershowitz, Okada (1988) listar fler varianter och relaterar dem till Ackermanns system av ordningsnotationer . Speciellt är en övre gräns som ges för ordningstyperna för rekursiva banordningar med n funktionssymboler φ( n ,0), med hjälp av Veblens funktion för stora räknebara ordinaler.
Formella definitioner
Fleruppsättningsvägordningen (>) kan definieras enligt följande :
| s = f ( s 1 ,..., s m ) > t = g ( t 1 ,..., t n ) | om | ||||||||
| f | . > | g | och | s | > | t j | för varje | j ∈{1,..., n }, | eller |
| är jag | ≥ | t | för vissa | i ∈{1,..., m }, | eller | ||||
| f | = | g | och | { s 1 ,..., s m } >> { t 1 ,..., t n } | |||||
var
- (≥) anger den reflexmässiga stängningen av mpo (>),
- { s 1 ,..., s m } betecknar multiuppsättningen av s s undertermer, liknande för t , och
- (>>) betecknar multiset-förlängningen av (>), definierad av { s 1 ,..., s m } >> { t 1 ,..., t n } if { t 1 ,..., t n } kan erhållas från { s 1 ,..., s m }
- genom att ta bort minst ett element, eller
- genom att ersätta ett element med en multiset av strikt mindre (wrt mpo) element.
Mer generellt är en beställningsfunktion till en funktion O som mappar en beställning en annan och uppfyller följande egenskaper:
- Om (>) är transitiv , så är O (>) det också.
- Om (>) är irreflexiv , så är O (>) det också.
- Om s > t , då f (..., s ,...) O (>) f (..., t ,...).
-
0 O är kontinuerlig på relationer, dvs om R , R 1 , R 2 , R 3 , ... är en oändlig sekvens av relationer, då O (∪
∞ i =0 R i ) = ∪
∞ i =0 O ( R i ).
Multiset-tillägget, avbildning (>) ovan till (>>) ovan är ett exempel på en ordningsfunktion: (>>)= O (>). En annan funktionell ordning är den lexikografiska förlängningen, vilket leder till den lexikografiska vägordningen .