Encompassment ordering
Term ordering in abstract rewriting
From Wikipedia, the free encyclopedia
In theoretical computer science, in particular in automated theorem proving and term rewriting, the containment,[1] or encompassment, preorder (≤) on the set of terms, is defined by[2]
- 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,[note 1] nor total[note 2]
- 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 R[note 3] with (<) is well-founded, where (<) denotes the irreflexive kernel of (≤).[3] In particular, (<) itself is well-founded.
Notes
- since both f(x) ≤ f(y) and f(y) ≤ f(x) for variable symbols x, y and a function symbol f
- since neither a ≤ b nor b ≤ a for distinct constant symbols a, b
- i.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 σ
