Detecting whether proving a predicate unified something

1
votes

I have a predicate that may unify its arguments, for example:

foo(X) :- X = 42.

How can I tell if, while proving foo(X), unification changed X? For example, I would like to know if writeln(X), foo(X), writeln(X) would print the same value for X twice, without actually doing the printing.

My actual implementation of foo/1 is actually much more complex, so please don't suggest specific to the simplified version above. In my program, foo(X) simplifies X using unification, but foo(X) may need to be proven several times until all simplifications have been performed. I would like to be able to write a foohelper(X) predicate that invokes foo(X) until X stops being unified.

2
prologunification
When do you want to tell if X has been instantiated? (We do not change X, we instantiate it) - false
I want to know if X was instantiated while proving foo(X), at the location of the second writeln(X) in my example. - Ed McMan

2 Answers

3
votes

Assuming we have only syntactic unification - that is, no constraints:

:- meta_predicate(call_instantiated(0,?)).

call_instantiated(Goal_0, Instantiated) :-
    copy_term(Goal_0, Copy_0),
    Goal_0,
    (  subsumes_term(Goal_0, Copy_0) ->  % succeeds iff equal u.t.r.
       Instantiated = false
    ;  Instantiated = true
    ).

Note that Goal_0 will or will not be further instantiated. The above subsumes_term/2 tests whether or not Goal_0 is now "more general" than Copy_0. Of course, it cannot be more general, so effectively that test tests whether or not the terms are identical up to renaming of variables.

Compared to using term_variables/2, as @PauloMoura has indicated, this may more may not be more efficient. It primarily depends on the efficiency of subsumes_term/2.

2
votes

Maybe you can use the standard term_variables/2 predicate? You can call it with your goal before and after calling the goal and check if the returned lists of variables are different. Something like:

...,
term_variables(foo(X), Vars0),
foo(X),
term_variables(foo(X), Vars),
(  Vars0 == Vars ->
   write(simplified)
;  write(not_simplified)
),
...