term_instance_si/2

[bakaq]

ISO Prolog (with Cor.2) has the predicate subsumes_term/2. You can read the definition in the link, but it basically encodes the concept of a term being "more general" than another. It is clearly not monotonic, but it also isn't transitive:

?- subsumes_term(f(a), f(X)).
   false.
?- X = a, subsumes_term(f(a), f(X)).
   % Adding a constraint increases the number of solutions! Non-monotonic!
   X = a.

?- subsumes_term(a(A,B), a(C,D)).
   true.
?- subsumes_term(a(C,D), a(B,A)).
   true.
?- subsumes_term(a(A,B), a(B,A)).
   % Not transitive!
   false.

term_instance/2 resolves the transitivity problem by copying one of the terms before calling subsumes_term/2:

?- term_instance(a(A,B), a(C,D)).
   true.
?- term_instance(a(C,D), a(B,A)).
   true.
?- term_instance(a(A,B), a(B,A)).
   % Transitive!
   true.

This effectively makes it decouple the variables from one argument from the variables of the other, and therefore only looks at the "shape of the holes" left by the variables to see if they fit into each other. By being reflexive (every term is an instance of itself) and transitive, it induces a preorder in the set of Prolog terms. Up to isomorphism this gives us a partial order. I've been thinking deeply about the nature of monotonicity of entailment and how to properly formalize the concept of monotonicity in the context of Prolog, and I'm quite confident that the preorder that term_instance/2 induces is essential for that. It also seems useful for implementing "pattern matching" (the normal language kind, not general unification), which is what made me think about this again recently (see bakaq/bakage#22 (comment)).

Unfortunately, it is still not monotonic:

?- term_instance(f(1), f(X)).
   false.
?- X = 1, term_instance(f(1), f(X)).
   X = 1.

The problem I want to solve then is the following: is it possible to make an _si version of term_instance/2 that is sufficiently useful? That is, a predicate that throws instantiation errors when it can't properly guarantee monotonicity. Equivalently, what is the set of conditions that the arguments need to satisfy so that no answers are lost by the raw term_instance/2?

My intuition is that this is not possible to do for the same reasons that a var_si/1 predicate is quite absurd, but I really want to be wrong because this would be an incredibly useful building block for many things. If a good behavior for term_instance_si/2 can be found, we can then do _t (for use with if_/3) and maybe even _c (constraints) based on it.

A first observation is that if this is indeed possible to do, the examples I used above for non-monotonicity should give:

?- term_instance_si(f(1), f(X)).
   error(instantiation_error,_).
?- X = 1, term_instance_si(f(1), f(X)).
   X = 1.

[hurufu]

I don't think that it makes sense to make such predicate, for exactly same reason as you've mentioned yourself – the only thing I see is to use when/2 to delay it...

[UWN]

It would help to look at the applications you have in mind. subsumes_term/2 (and not term_instance/2) is used for loop-checking. There, the same variables may appear on both sides. But it cannot have a declarative meaning. It only serves to implement things that do have a declarative meaning. if_/3 relies very much on having a declarative meaning.

The easiest way to check if a predicate may have a declarative meaning is to see if its entire meaning can be derived from just considering ground literals.

[bakaq]

In the case of only ground terms term_instance/2 seems to be just the identity relation. Hm, this is tricky...