library(occurs)
The predicates in library(occurs)
test whether a given term
is a subterm of another or not. We define a subterm thus:
A proper subterm of a term T would be any subterm of T other than T itself. There are no library predicates concerned with the "proper subterm" relationship, only the "subterm" relationship.
There are two questions we might ask:
=
to) some subterm of T?
The predicates that ask this question have _term
in their names.
==
to) some subterm of T?
The predicates that ask this question have _var
in their names.
When the predicates are applied to ground terms, both questions have the same answers.
Seven predicates are defined by library(occurs)
:
contains_term(
+SubTerm,
+Term)
=
)
SubTerm.
contains_var(
+SubTerm,
+Term)
==
) SubTerm. The reason for the name is that this predicate is
normally used to check whether Term contains a particular
variable SubTerm. But contains_var/2
makes sense
even when SubTerm
is not a variable. In fact, if Term and SubTerm are both
ground, contains_term/2
and contains_var/2
are the same test.
free_of_term(
+SubTerm,
+Term)
=
) SubTerm.
free_of_var(
+SubTerm,
+Term)
==
) SubTerm. This is the "occur check",
which is needed for sound unification: a variable X should
unify with a non-variable term T only if free_of_var(
X,
T)
.
See library(unify)
(lib-tma-unify) for an example of the use of this predicate.
occurrences_of_term(
+SubTerm,
+Term,
?Tally)
=
) SubTerm.
occurrences_of_var(
+SubTerm,
+Term,
?Tally)
==
) SubTerm.
sub_term(
-SubTerm,
+Term)
| ?- sub_term(X, (a+b)*(c+d)), tab(8), write(X), nl, fail. (a+b)*(c+d) c+d d c a+b b a no
The order in which these terms are generated is subject to change, and should not be relied upon.