// Workers AI · dad joke modeWhat did Encompassment Ordering say to its date? You're always contained within my heart.
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
[edit]- 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
[edit]- ↑ 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 σ
References
[edit]- ↑ Gerard Huet (1981). "A Complete Proof of Correctness of the Knuth–Bendix Completion Algorithm". 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. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. Here:sect.2.1, p. 250
- ↑ Dershowitz, Jouannaud (1990), sect.5.4, p. 278; somewhat sloppy, R is required to be a "terminating rewrite relation" there.
 | This computer science article is a stub. You can help Wikipedia by adding missing information. |