Ordenamiento de abarcamiento

Ordenación de términos en la reescritura de resúmenes

Diagrama triangular de dos términos s  ≤  t relacionados por el preorden de abarcamiento.

En informática teórica , en particular en la demostración automatizada de teoremas y la reescritura de términos , la contención , ^[1] o abarcamiento , preorden (≤) en el conjunto de términos , se define por ^[2]

s  ≤  t si un subtérmino de t es una instancia de sustitución de s .

Se utiliza, por ejemplo, en el algoritmo de compleción de Knuth-Bendix .

Propiedades

• La abarcación es un preorden , es decir, reflexivo y transitivo , pero no antisimétrico , ^{[nota 1]} ni total ^{[nota 2]}
• La relación de equivalencia correspondiente , definida por s  ~  t si s  ≤  t  ≤  s , es igualdad módulo cambio de nombre .
• s  ≤  t siempre que s sea un subtérmino de t .
• s  ≤  t siempre que t sea una instancia de sustitución de s .
• La unión de cualquier orden de reescritura bien fundado R ^{[nota 3]} con (<) está bien fundada , donde (<) denota el núcleo irreflexivo de (≤). ^[3] En particular, (<) en sí mismo está bien fundado.

Notas

1. ya que tanto f ( x ) ≤  f ( y ) como f ( y ) ≤  f ( x ) para los símbolos de variable x , y y un símbolo de función f
2. ya que ni a  ≤  b ni b  ≤  a para símbolos constantes distintos a , b
3. es una relación binaria irreflexiva, transitiva y bien fundada R tal que sRt implica u [ s σ ] _p R u [ t σ] _p para todos los términos s , t , u , cada camino p de u y cada sustitución  σ

Referencias

1. Gerard Huet (1981). "Una prueba completa de la corrección del algoritmo de compleción de Knuth-Bendix". J. Comput. Syst. Sci . 23 (1): 11–21. doi : 10.1016/0022-0000(81)90002-7 .
2. N. Dershowitz, J.-P. Jouannaud (1990). Jan van Leeuwen (ed.). Rewrite Systems . Manual de informática teórica. Vol. B. Elsevier. págs. 243–320.Aquí: sección 2.1, pág. 250
3. Dershowitz, Jouannaud (1990), secc.5.4, p. 278; algo descuidado, allí se requiere que R sea una "relación de reescritura de terminación".