![Encompassment ordering on terms s,t_svg](https://upload.wikimedia.org/wikipedia/commons/4/44/Encompassment_ordering_on_terms_s%2Ct_svg.svg)
In
theoretical computer science
Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory.
It is difficult to circumsc ...
, in particular in
automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...
and
term rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or reduc ...
,
the containment, or encompassment,
preorder
In mathematics, especially in order theory, a preorder or quasiorder is a binary relation that is reflexive and transitive. Preorders are more general than equivalence relations and (non-strict) partial orders, both of which are special c ...
(≤) on the set of
term
Term may refer to:
* Terminology, or term, a noun or compound word used in a specific context, in particular:
**Technical term, part of the specialized vocabulary of a particular field, specifically:
***Scientific terminology, terms used by scient ...
s, is defined by
:''s'' ≤ ''t'' if a
subterm
In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a wh ...
of ''t'' is a
substitution instance Substitution is a fundamental concept in logic.
A substitution is a syntactic transformation on formal expressions.
To apply a substitution to an expression means to consistently replace its variable, or placeholder, symbols by other expressions.
T ...
of ''s''.
It is used e.g. in the
Knuth–Bendix completion algorithm The Knuth–Bendix completion algorithm (named after Donald Knuth and Peter Bendix) is a semi-decision algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it effectively ...
.
Properties
* Encompassment is a
preorder
In mathematics, especially in order theory, a preorder or quasiorder is a binary relation that is reflexive and transitive. Preorders are more general than equivalence relations and (non-strict) partial orders, both of which are special c ...
, 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
In formal logic and related branches of mathematics, a functional predicate, or function symbol, is a logical symbol that may be applied to an object term to produce another object term.
Functional predicates are also sometimes called mappings, but ...
''f'' nor
total
Total may refer to:
Mathematics
* Total, the summation of a set of numbers
* Total order, a partial order without incomparable pairs
* Total relation, which may also mean
** connected relation (a binary relation in which any two elements are comp ...
[since 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
In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a wh ...
of ''t''.
* ''s'' ≤ ''t'' whenever ''t'' is a
substitution instance Substitution is a fundamental concept in logic.
A substitution is a syntactic transformation on formal expressions.
To apply a substitution to an expression means to consistently replace its variable, or placeholder, symbols by other expressions.
T ...
of ''s''.
* The union of any well-founded
rewrite order
In theoretical computer science, in particular in automated reasoning about formal equations, reduction orderings are used to prevent endless loops. Rewrite orders, and, in turn, rewrite relations, are generalizations of this concept that have tur ...
''R''
[i.e. irreflexive, transitive, and well-founded binary relation ''R'' such that ''sRt'' implies ''u'' ''s''Substitution (logic)#First-order logic">σ">Substitution_(logic)#First-order_logic.html" ;"title="/a>''s''Substitution (logic)#First-order logic">σsub>''p'' R ''u''[''t''σ]''p'' for all terms ''s'', ''t'', ''u'', each path ''p'' of ''u'', and each Substitution (logic)#First-order logic, substitution ''σ''] with (<) is well-founded, where (<) denotes the
irreflexive kernel
In mathematics, a binary relation ''R'' on a set ''X'' is reflexive if it relates every element of ''X'' to itself.
An example of a reflexive relation is the relation " is equal to" on the set of real numbers, since every real number is equal to ...
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
References
Rewriting systems
Order theory
{{comp-sci-stub