Checking Terms for Subterms -- library(occurs)

The predicates in library(occurs) test whether a given term is a subterm of another or not. We define a subterm thus:

• T is a subterm of T
• S is a subterm of T if A is an argument of T and S is a subterm of A

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:

• does S unify with (is it = to) some subterm of T? The predicates that ask this question have _term in their names.
• is S identical to (is it == 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)

is true when Term contains a subterm that unifies with (=) SubTerm.

contains_var(+SubTerm, +Term)

is true when Term contains a subterm that is identical to (==) 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)

is true when Term does not contain a subterm that unifies with (=) SubTerm.

free_of_var(+SubTerm, +Term)

is true when Term does not contain a subterm that is identical to (==) 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)

unifies Tally with the number of subterms of Term that unify with (=) SubTerm.

occurrences_of_var(+SubTerm, +Term, ?Tally)

unifies Tally with the number of subterms of Term that are identical to (==) SubTerm.

sub_term(-SubTerm, +Term)

enumerates the SubTerms of Term. The order in that the subterms are enumerated is not fully defined, though each subterm will be reported before any of its own subterms. Be careful: terms tend to have lots of subterms.

          | ?- 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.