Ordenación de rutas (reescritura de términos)

En la informática teórica , en particular en la reescritura de términos , un ordenamiento de caminos es un orden total estricto bien fundado (>) en el conjunto de todos los términos tales que

f (...) > g ( s ₁ ,..., s _n )  si f ^. > g y f (...) > s _i para i =1,..., n ,   

donde ( ^{. >) es un} orden de precedencia total dado por el usuario en el conjunto de todos los símbolos de función .

Intuitivamente, un término f (...) es mayor que cualquier término g (...) construido a partir de términos s _i menores que f (...) usando un símbolo raíz de menor precedencia g . En particular, por inducción estructural , un término f (...) es mayor que cualquier término que contenga solo símbolos menores que f .

Un ordenamiento de caminos se usa a menudo como ordenamiento de reducción en la reescritura de términos, en particular en el algoritmo de completación de Knuth-Bendix . Como ejemplo, un sistema de reescritura de términos para " multiplicar " expresiones matemáticas podría contener una regla x *( y + z ) → ( x * y )  +  ( x * z ). Para probar la terminación , se debe encontrar un ordenamiento de reducción (>) con respecto al cual el término x *( y + z ) sea mayor que el término ( x * y )+( x * z ). Esto no es trivial, ya que el primer término contiene menos símbolos de función y menos variables que el segundo. Sin embargo, estableciendo la precedencia (*) ^. > (+), se puede usar un ordenamiento de caminos, ya que tanto x *( y + z ) > x * y como x *( y + z ) > x * z es fácil de lograr.

También puede haber sistemas para ciertas funciones recursivas generales , por ejemplo, un sistema para la función de Ackermann puede contener la regla A( a ⁺ , b ⁺ ) → A( a , A( a ⁺ , b )), ^{[ 1 ]} donde b ⁺ denota el sucesor de b .

Dados dos términos s y t , con un símbolo raíz f y g , respectivamente, para decidir su relación se comparan primero sus símbolos raíz.

• Si f < ^. g , entonces s puede dominar a t solo si uno de los subtérminos de s lo hace.
• Si f ^. > g , entonces s domina a t si s domina a cada uno de los subtérminos de t .
• Si f = g , entonces los subtérminos inmediatos de s y t deben compararse recursivamente. Dependiendo del método particular, existen diferentes variaciones de ordenamientos de caminos. ^{[ 2 ] [ 3 ]}

Estas últimas variantes incluyen:

• el ordenamiento de caminos de multiconjuntos ( mpo ), originalmente llamado ordenamiento de caminos recursivos ( rpo ) ^{[ 4 ]}
• el ordenamiento de rutas lexicográficas ( lpo ) ^{[ 5 ]}
• una combinación de mpo y lpo, llamada ordenación de caminos recursiva por Dershowitz, Jouannaud (1990) ^{[ 6 ] [ 7 ] [ 8 ]}

Dershowitz y Okada (1988) enumeran más variantes y las relacionan con el sistema de notaciones ordinales de Ackermann . En particular, se da una cota superior para los tipos de orden de ordenaciones de caminos recursivos con n símbolos de función, que es φ( n , 0), utilizando la función de Veblen para ordinales numerables grandes. ^{[ 7 ]}

El ordenamiento de rutas de multiconjuntos (>) se puede definir de la siguiente manera: ^{[ 9 ]}

dónde

• (≥) denota el cierre reflexivo del mpo (>),
• { s ₁ ,..., s _m } denota el multiconjunto de subtérminos de s , de forma similar para t , y
• (>>) denota la extensión multiconjunto de (>), definida por { s ₁ ,..., s _m } >> { t ₁ ,..., t _n } si { t ₁ ,..., t _n } se puede obtener de { s ₁ ,..., s _m }
  • eliminando al menos un elemento, o
  • reemplazando un elemento por un multiconjunto de elementos estrictamente más pequeños (con respecto al mpo). ^{[ 10 ]}

De manera más general, un funcional de orden es una función O que asigna un orden a otro y satisface las siguientes propiedades: ^{[ 11 ]}

• Si (>) es transitivo , entonces O (>) también lo es.
• Si (>) es irreflexivo , entonces O (>) también lo es.
• Si s > t , entonces f (..., s ,...) O (>) f (..., t ,...).
• O es continua en las relaciones, es decir, si R ₀ , R ₁ , R ₂ , R ₃ , ... es una secuencia infinita de relaciones, entonces O (∪ ^∞ _{i =0} R _i ) = ∪ ^∞ _{i =0} O ( R _i ).

La extensión de multiconjuntos, que mapea (>) arriba a (>>) arriba, es un ejemplo de un funcional de orden: (>>)= O (>). Otro funcional de orden es la extensión lexicográfica , que conduce al ordenamiento de caminos lexicográficos .