Ordenamiento 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 .

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.

^ 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
^ ya que ni a ≤ b ni b ≤ a para símbolos constantes distintos a , b
^ 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 σ

^ 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 .
^ 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
^ Dershowitz, Jouannaud (1990), secc.5.4, p. 278; algo descuidado, allí se requiere que R sea una "relación de reescritura de terminación".