Term Utilities
**************

   This package defines operations on terms for subsumption checking,
"anti-unification", unification with occurs-check, testing acyclicity,
and getting the variables.

   To load the package, enter the query

     | ?- use_module(library(terms)).

`subsumes_chk(?GENERAL, ?SPECIFIC)'
     SPECIFIC is an instance of GENERAL, i.e. if there is a
     substitution that leaves SPECIFIC unchanged and makes GENERAL
     identical to SPECIFIC.  It doesn't bind any variables.
          subsumes_chk(f(X), f(a)).
          
          true
          
          | ?- subsumes_chk(f(a), f(X)).
          
          no
          
          | ?- subsumes_chk(A-A, B-C).
          
          no
          
          | ?- subsumes_chk(A-B, C-C).
          
          true

`subsumes_chk(?GENERAL, ?SPECIFIC)'
     SPECIFIC is an instance of GENERAL.  It will bind variables in
     GENERAL (but not those in SPECIFIC) so that GENERAL becomes
     identical to SPECIFIC.

`variant(?TERM, ?VARIANT)'
     TERM and VARIANT are identical modulo renaming of variables,
     provided TERM and VARIANT have no variables in common.

`term_subsumer(?TERM1, ?TERM2, ?GENERAL)'
     GENERAL is the most specific term that generalizes TERM1 and
     TERM2.  This process is sometimes called *anti-unification*, as it
     is the dual of unification.
          | ?- term_subsumer(f(g(1,h(_))), f(g(_,h(1))), T).
          
          T = f(g(_B,h(_A)))
          
          | ?- term_subsumer(f(1+2,2+1), f(3+4,4+3), T).
          
          T = f(_A+_B,_B+_A)

`term_hash(?TERM, +DEPTH, +RANGE, ?HASH)'
     If TERM is instantiated to the given DEPTH, an integer hash value
     in the range [0,RANGE) corresponding to TERM is unified with HASH.
     Otherwise, the goal just succeeds, leaving HASH uninstantiated.

     The *depth* of a term is defined as follows: the (principal functor
     of) the term itself has depth 1, and an argument of a term with
     depth I has depth I+1.

     DEPTH should be an integer >= -1.  If DEPTH = -1, TERM must be
     ground, and all subterms of TERM are relevant in computing HASH.
     Otherwise, only the subterms up to depth DEPTH of TERM are used in
     the computation.

     RANGE should be an integer >= 1.

          | ?- term_hash([a,b,_], 3, 4, H).
          
          H = 2
          
          | ?- term_hash([a,b,_], 4, 4, H).
          
          true
          
          | ?- term_hash(f(a,f(b,f(_,[]))), 2, 4, H).
          
          H = 0

     `term_hash/4' is provided primarily as a tool for the construction
     of sophisticated Prolog clause access schemes.  Its intended use
     is to generate hash values for terms that will be used with first
     argument clause indexing, yielding compact and efficient
     multi-argument or deep argument indexing.

`term_variables(?TERM, ?VARIABLES)'
     VARIABLES is the set of variables occurring in TERM.

`unify_with_occurs_check(?X, ?Y) "[ISO]"'
     True if X and Y unify to a finite (acyclic) term.  Runs in almost
     linear time.

`acyclic_term(?X)'
     True if X is finite (acyclic).  Runs in linear time.

`cyclic_term(?X)'
     True if X is infinite (cyclic).  Runs in linear time.