Ordenamiento de rutas (reescritura de términos)

Orden total en informática

En informática teórica , en particular en la reescritura de términos , un ordenamiento de rutas 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 (...) utilizando 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 ruta se utiliza a menudo como ordenamiento de reducción en la reescritura de términos, en particular en el algoritmo de compleció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 utilizar un ordenamiento de ruta, ya que tanto x *( y + z ) > x * y como x *( y + z ) > x * z son fáciles 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 sólo si uno de los subtérminos de s lo hace.
• Si f ^. > g , entonces s domina a t si s domina 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 ordenamiento de trayectorias. ^{[2] [3]}

Las últimas variaciones incluyen:

• El ordenamiento de rutas multiconjunto ( mpo ), originalmente llamado ordenamiento de rutas recursivo ( rpo ) ^[4]
• El ordenamiento de rutas lexicográficas ( lpo ) ^[5]
• una combinación de mpo y lpo, llamada ordenación de ruta 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, un límite superior dado para los tipos de orden de ordenamientos de rutas recursivas con n símbolos de función es φ( n ,0), utilizando la función de Veblen para ordinales contables grandes. ^[7]

Definiciones formales

El ordenamiento de rutas de conjuntos múltiples (>) se puede definir de la siguiente manera: ^[9]

dónde

• (≥) denota el cierre reflexivo del mpo (>),
• { s ₁ ,..., s _m } denota el multiconjunto de los subtérminos de s , similares para t , y
• (>>) denota la extensión multiconjunto de (>), definida por { s ₁ ,..., s _m } >> { t ₁ ,..., t _n } si { t ₁ ,..., t _n } puede obtenerse 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 ordenamiento 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 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 multiconjunto, que asigna (>) arriba a (>>) arriba, es un ejemplo de una función de orden: (>>)= O (>). Otra función de orden es la extensión lexicográfica , que conduce al ordenamiento de rutas lexicográficas .

Referencias

1. N. Dershowitz, "Terminación" (1995). pág. 207
2. Nachum Dershowitz , Jean-Pierre Jouannaud (1990). Jan van Leeuwen (ed.). Reescribir sistemas . Manual de informática teórica. vol. B. Elsevier. págs. 243–320.Aquí: secc.5.3, p.275
3. Gerard Huet (mayo de 1986). Estructuras formales para computación y deducción. Escuela de verano internacional sobre lógica de programación y cálculos de diseño discreto. Archivado desde el original el 14 de julio de 2014.Aquí: capítulo 4, p.55-64
4. N. Dershowitz (1982). "Ordenamientos para sistemas de reescritura de términos" (PDF) . Theoret. Comput. Sci . 17 (3): 279–301. doi :10.1016/0304-3975(82)90026-3. S2CID  6070052.
5. S. Kamin, J.-J. Levy (1980). Dos generalizaciones del ordenamiento recursivo de rutas (informe técnico). Univ. de Illinois, Urbana/IL.
6. Kamin, Levy (1980)
7. N. Dershowitz, M. Okada (1988). "Técnicas de teoría de pruebas para la teoría de reescritura de términos". Actas del 3.er Simposio IEEE sobre lógica en informática (PDF) . págs. 104-111.
8. Mitsuhiro Okada, Adam Steele (1988). "Ordenamiento de estructuras y el algoritmo de compleción de Knuth-Bendix". Actas de la Conferencia Allerton sobre comunicación, control y computación .
9. Huet (1986), sección 4.3, definición 1, p.57
10. Huet (1986), sección 4.1.3, p.56
11. Huet (1986), sección 4.3, pág. 58