encompassment ordering
{{Short description|Term ordering in abstract rewriting}}
File:Encompassment ordering on terms s,t_svg.svg
In theoretical computer science, in particular in automated theorem proving and term rewriting,
the containment,{{cite journal| author=Gerard Huet| title=A Complete Proof of Correctness of the Knuth–Bendix Completion Algorithm| journal=J. Comput. Syst. Sci.| year=1981| volume=23| number=1| pages=11–21| doi=10.1016/0022-0000(81)90002-7| doi-access=free}} or encompassment, preorder (≤) on the set of terms, is defined by{{cite book| author=N. Dershowitz, J.-P. Jouannaud| title=Rewrite Systems| year=1990| volume=B| pages=243–320| publisher=Elsevier| editor=Jan van Leeuwen| editor-link=Jan van Leeuwen| series=Handbook of Theoretical Computer Science}} Here:sect.2.1, p. 250
:s ≤ t if a subterm of t is a substitution instance of s.
It is used e.g. in the Knuth–Bendix completion algorithm.
Properties
- Encompassment is a preorder, i.e. reflexive and transitive, but not anti-symmetric,since both f(x) ≤ f(y) and f(y) ≤ f(x) for variable symbols x, y and a function symbol f nor totalsince neither a ≤ b nor b ≤ a for distinct constant symbols a, b
- The corresponding equivalence relation, defined by s ~ t if s ≤ t ≤ s, is equality modulo renaming.
- s ≤ t whenever s is a subterm of t.
- s ≤ t whenever t is a substitution instance of s.
- The union of any well-founded rewrite order Ri.e. irreflexive, transitive, and well-founded binary relation R such that sRt implies u[sσ]p R u[tσ]p for all terms s, t, u, each path p of u, and each substitution σ with (<) is well-founded, where (<) denotes the irreflexive kernel of (≤).Dershowitz, Jouannaud (1990), sect.5.4, p. 278; somewhat sloppy, R is required to be a "terminating rewrite relation" there. In particular, (<) itself is well-founded.
Notes
{{Reflist|group=note}}