Ground, Numbervars, Subsumption, Variant

ground(+X)

basics
Succeeds if X is currently instantiated to a term that is completely bound (has no uninstantiated variables in it); otherwise it fails. Predicate ground/1 has no associated error conditions.

numbervars(+Term, +FirstN, ?LastN)

num_vars
This predicate provides a mechanism for grounding a (HiLog) term so that it may be analyzed. Each variable in the (HiLog) term Term is instantiated to a term of the form '$VAR'(N), where N is an integer starting from FirstN. FirstN is used as the value of N for the first variable in Term (starting from the left). The second distinct variable in Term is given a value of N satisfying "N is FirstN + 1" and so on. The last variable in Term has the value LastN-1.

numbervars(+Term)

num_vars
This predicate is defined as:

numbervars(Term, 0, _).

It is included solely for convenience.

unnumbervars(+Term, +FirstN, ?Copy)

num_vars
This predicate is a partial inverse of predicate numbervars/3. It creates a copy of Term in which all subterms of the form '$VAR'(<int>) where <int> is not less than FirstN are uniformly replaced by variables. '$VAR'' subterms with the same integer are replaced by the same variable. Also a version unnumbervars/2 is provided which calls unnumbervars/3 with the second parameter set to 0.

subsumes(?Term1, +Term2)

subsumes
Term subsumption is a sort of one-way unification. Term Term1 and Term2 unify if they have a common instance, and unification in Prolog instantiates both terms to that (most general) common instance. Term1 subsumes Term2 if Term2 is already an instance of Term1. For our purposes, Term2 is an instance of Term1 if there is a substitution that leaves Term2 unchanged and makes Term1 identical to Term2. Predicate subsumes/2 does not work as described if Term1 and Term2 share common variables.

subsumes_chk(+Term1, +Term2)

subsumes
The subsumes_chk/2 predicate is true when Term1 subsumes Term2; that is, when Term2 is already an instance of Term1. This predicate simply checks for subsumption and does not bind any variables either in Term1 or in Term2. Term1 and Term2 should not share any variables.

Examples:

            | ?- subsumes_chk(a(X,f,Y,X),a(U,V,b,S)).

            no
            | ?- subsumes_chk(a(X,Y,X),a(b,b,b)).

            X = _595884
            Y = _595624

variant(?Term1, ?Term2)

subsumes
This predicate is true when Term1 and Term2 are alphabetic variants. That is, you could imagine that variant/2 as being defined like:

        variant(Term1, Term2) :-
             subsumes_chk(Term1, Term2),
             subsumes_chk(Term2, Term1).

but the actual implementation of variant/2 is considerably more efficient. However, in general, it does not work for terms that share variables; an assumption that holds for most (reasonable) uses of variant/2.