Encompassment ordering

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.
Triangle diagram of two terms s  t related by the encompassment preorder.

It is used e.g. in the Knuth–Bendix completion algorithm.

Properties

Notes

  1. since both f(x)  f(y) and f(y)  f(x) for variable symbols x, y and a function symbol f
  2. since neither a  b nor b  a for distinct constant symbols a, b
  3. 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 σ
gollark: Rainbow lineage, that's a cool idea.
gollark: Probably an entire salt shaker, considering.
gollark: Someone should really update the wiki.
gollark: Are xenowyrms actually that rare? I've seen many of them recently but no metallics or that blusang lindwyrm thing.
gollark: Also, don't these AP floods have to be planned about two days in advance?

References

  1. 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.
  2. N. Dershowitz, J.-P. Jouannaud (1990). Jan van Leeuwen (ed.). Rewrite Systems. Handbook of Theoretical Computer Science. B. Elsevier. pp. 243–320. Here:sect.2.1, p. 250
  3. Dershowitz, Jouannaud (1990), sect.5.4, p. 278; somewhat sloppy, R is required to be a "terminating rewrite relation" there.


This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.