Copy term with variables without variables being bound

Question

With SWI-Prolog.

How can a term with variables be copied without the variables being bound?

What I have tried

I tried copy_term/2 and duplicate_term/2

For example:

foo(c).

foo(E) :-
    E = bar(a,b,X),
    copy_term(E,Ec),
    duplicate_term(E,Ed),
    write("E:  "),write(E),nl,
    write("Ec: "),write(Ec),nl,
    write("Ed: "),write(Ed),nl.

results in

?- foo(bar(a,b,bar(a,b,bar(a,b,c)))).
E:  bar(a,b,bar(a,b,bar(a,b,c)))
Ec: bar(a,b,bar(a,b,bar(a,b,c)))    <-- Copy
Ed: bar(a,b,bar(a,b,bar(a,b,c)))    <-- Duplicate
true.

?- foo(bar(a,b,bar(a,b,c))).
E:  bar(a,b,bar(a,b,c))
Ec: bar(a,b,bar(a,b,c))    <-- Copy
Ed: bar(a,b,bar(a,b,c))    <-- Duplicate
true.

?- foo(bar(a,b,c)).
E:  bar(a,b,c)
Ec: bar(a,b,c)    <-- Copy
Ed: bar(a,b,c)    <-- Duplicate
true.

and checked the section Analyzing and Constructing Terms

What I need

Here En is the result of predicate returning what I need

?- foo(bar(a,b,bar(a,b,bar(a,b,c)))).
E:  bar(a,b,bar(a,b,bar(a,b,c)))
En: bar(a,b,X),                      <-- Need this
true.

?- foo(bar(a,b,bar(a,b,c))).
E:  bar(a,b,bar(a,b,c))
En: bar(a,b,X),                      <-- Need this
true.

?- foo(bar(a,b,c)).
E:  bar(a,b,c)
En: bar(a,b,X),                      <-- Need this
true.

I was hoping for a built-in predicate.

TL;DR

The need for this is in solving binary expressions. The original is used to select the predicate and to solve the expression. A copy I refer to as local is used to show the rewrite for the subexpression and a copy I refer to as global is used to show the rewrite applied to the entire expression. If there is only one term, e.g. no copies, once the variable is bound for one use, it causes the other uses to fail.

The current solution is to type in the multiple terms with different variables for each use into the predicate. Multiply this by hundreds to possibly thousands of predicates with possible typing or copy/paste mistakes and you can see the need.

Other considerations

I have also considered having a master copy of the term in the predicate and then using that to make the three copies. The problem with that is one of the copies is used in selecting the predicate, so before a predicate can be selected the copy would have to take place. So even if a predicate is not selected for evaluation a copy has to take place in the predicate.

foo(c).

foo(Ec) :-
    M = bar(a,b,X),
    copy_term(M,Ec),
    duplicate_term(M,Ed),
    write("M:  "),write(M),nl,
    write("Ec: "),write(Ec),nl,
    write("Ed: "),write(Ed),nl.

?- foo(bar(a,b,bar(a,b,bar(a,b,c)))).
M:  bar(a,b,_9364)
Ec: bar(a,b,bar(a,b,bar(a,b,c)))
Ed: bar(a,b,_9384)
true.

?- foo(bar(a,b,bar(a,b,c))).
M:  bar(a,b,_9240)
Ec: bar(a,b,bar(a,b,c))
Ed: bar(a,b,_9260)
true.

?- foo(bar(a,b,c)).
M:  bar(a,b,_9116)
Ec: bar(a,b,c)
Ed: bar(a,b,_9136)
true.

So
copy_term/2 gives me the copy with the variables bound which is needed for the predicate selection and evaluation part duplicate_term/2 gives me the term with the free variables for use with other predicates.

Example output from actual application

                    Global                           Local
                    ------------------               -----------------------------
Input               (1 + ((0 + 0) + 0)) 
0 + X -> X                                           (0 + 0)                -> 0
=                   (1 + (0 + 0))       
X + 0 -> X                                           (0 + 0)                -> 0
=                   (1 + 0)             
X + 0 -> X                                           (1 + 0)                -> 1
=                   1

I do not get why in the third example you replace `c` with `X`. You always want to replace the third with a variable? — Willem Van Onsem, Feb 21 '17 at 14:57
@false No I need it to be available as an unbound variable. Currently I used `term_variables/2` to extract the new variable out of the copied term. — Guy Coder, Feb 21 '17 at 15:00
@false Thanks didn't know about `subsumes_term/2` will take a look. — Guy Coder, Feb 21 '17 at 15:04
@WillemVanOnsem Maybe I misread your comment. Were you referring to the `What I have tried` or the `What I need` version? — Guy Coder, Feb 21 '17 at 15:15
@GuyCoder: the **What I need** part: you say the expected result for `bar(a,b,c)` is `bar(a,b,X)`. Why? — Willem Van Onsem, Feb 21 '17 at 15:17
@WillemVanOnsem Thanks. In hunting down one of my bugs those cases, e.g. leaves, were working correctly and that's when I found the other cases, e.g. branches, that were causing the invalid output. I would like to avoid making the distinction between leaves and branches in my code if possible. So by using `X` instead of `c` for the last one the code is more generic. I know it means doing more processing for the leaf case, but I hope to make it so an end user can make the rules without understanding the workings of Prolog. Obviously will need to parse user made rules. Make sense? — Guy Coder, Feb 21 '17 at 15:27
@GuyCoder: "Make sense?" mnmnm, You have here a lot of declarative reasoning ("more generic" should probably be "more general") somehow mixed with rather operational notions. What means "hunting down one of my bugs" exactly to you? I mean, you don't know them by name, don't you? — false, Feb 21 '17 at 15:49
@false `What means "hunting down one of my bugs" exactly to you?` In this case using `gtrace` and stepping until I see where the expected values and different values occur. In this case the result of `term_copy` was not what I expected with the variable being bound on return. — Guy Coder, Feb 21 '17 at 16:05
@false What does `that situation` mean? If you are referring to the names `local` and `global` I don't like them either, but I haven't found anything better. — Guy Coder, Feb 21 '17 at 16:12
@false That is the question, `copy_term(E,Ec)` returned `bar(a,b,bar(a,b,bar(a,b,c)))` when I expected `bar(a,b,X)` — Guy Coder, Feb 21 '17 at 16:21
@false Thanks. I at least understand that last comment. I will see if I can make a better example. — Guy Coder, Feb 21 '17 at 16:41
@false LOL. I could probably write a chapter or two or three on that question. I just can't figure out how to do `disjunction` recursively, or if using disjunction is even the correct path to take. I have also tried swapping `a` with `b` but then the variables are bound when I need them to be free. I have also tried `rotate`, but I can't remember why that failed. I tried variations on `cross-product` but that simplifies down to swap. Used DCG, difference list, etc. etc. — Guy Coder, Feb 21 '17 at 17:10
@false Thanks for bearing with me on this question. I learn a lot from your comments and past questions. I don't think I can do better than what I have. — Guy Coder, Feb 21 '17 at 17:12
@false You are endowing me with more knowledge of Prolog than I have. Specifically I don't uses functors that much. I am at least glad to see no one else has posted an answer. I suspect someone else has the answer and they are just waiting to see if others find it. — Guy Coder, Feb 21 '17 at 17:16
@false I am no bounty expert but I think this applies `If you do not award your bounty within 7 days (plus the grace period), the highest voted answer created after the bounty started with a minimum score of 2 will be awarded half the bounty amount (or the full amount, if the answer is also accepted). If two or more eligible answers have the same score (their scores are tied), the oldest answer is chosen. If there's no answer meeting those criteria, no bounty is awarded to anyone. ` [bounty](http://stackoverflow.com/help/bounty) — Guy Coder, Feb 21 '17 at 17:19
@false My current plan of attack for the points is to let it sit on the back burner and hope the answers comes to me before the time limit. I know I just used a functor in this, but that was a simple one. I started with functors with the expressions for this question and had to change to list before I could get all of the code to work as I needed. Since I am still in the proof of concept phase I am not endeared to using list. — Guy Coder, Feb 21 '17 at 17:25
@false. If you post `But already the goal before it, E = bar(a,b,X), unified X with c. So poor copy_term/2 has no chance to undo that! That's why I suspected you need subsumes_term/2.` or something like it I will accept it as the answer since it explained where my conception of `copy_term/2` was wrong. — Guy Coder, Feb 21 '17 at 17:55
What's the point of adding highlighting here? Copy is now highlighted as a variable. But it is not a variable etc. — false, Apr 01 '17 at 05:58
For those who have read this far. I found a much better solution to the problem related to this question. To solve the problem I realized I should not traverse the tree as normal, e.g. traverse the tree from start to end in one pass, but instead traverse the expression until a simplification or evaluation of a term can be applied then back out and write the updated expression. Then start the traverse the tree anew looking for the next simplification or evaluation, etc., etc.. — Guy Coder, Apr 04 '17 at 11:16

score 4 · Accepted Answer · edited May 23 '17 at 12:02

(A very tiny remark in the beginning: Rather use single quotes, not double quotes for simple atoms.)

In the first case, the relevant part is:

foo(E) :-
    E = bar(a,b,X),
    copy_term(E,Ec),
    write('X' = X).

?- foo(bar(a,b,bar(a,b,bar(a,b,c)))).

Here, E = bar(a,b,X) already unifies X, which cannot be undone later on. With the $-debugger (see below) I get:

call:copy_term(bar(a,b,bar(a,b,bar(a,b,c))),A).
exit:copy_term(bar(a,b,bar(a,b,bar(a,b,c))),bar(a,b,bar(a,b,bar(a,b,c))))

So the ground term is simply copied.

In the second case, the relevant part is:

foo(Ec) :-
    M = bar(a,b,X),
    copy_term(M,Ec),
    write('Ec: '),write(Ec),nl.

?- foo(bar(a,b,bar(a,b,bar(a,b,c)))).

First note the variables! Ec is in the beginning a ground term. And that will not change! No matter what you do.

What you actually do is to copy a non-ground term onto a ground term. Now, literally that means, you are copying the term, and the copy gets unified with the ground terms. Unification cannot undo the groundness.

In this fragment you are unhappy that the copied term is ground. In fact, prior to copy_term(M, Ec), the term Ec is already ground. If you have used a d-bugger and have not found the error, consider a simpler version and simply add a $ in front of copy_term/2. That is:

foo(Ec) :-
        M = bar(a,b,X),
        $copy_term(M,Ec),
        write('Ec: '),write(Ec),nl.

which produces:

call:copy_term(bar(a,b,A),bar(a,b,bar(a,b,bar(a,b,c)))).
exit:copy_term(bar(a,b,A),bar(a,b,bar(a,b,bar(a,b,c)))).
Ec: bar(a,b,bar(a,b,bar(a,b,c)))

So, the copy_term/2 is entirely redundant in this case.

Some minor remarks: In SWI, the difference betweencopy_term/2 and duplicate_term/2 is only of relevance when you do destructive update on terms (don't!). Particularly problematic is that both copy constraints somehow:

?- X #> Y, copy_term(X,C).
Y#=<X+ -1,
_3398#=<C+ -1,
_3398#=<C+ -1.

?- X #> Y, duplicate_term(X,C).
Y#=<X+ -1,
_3780#=<C+ -1.

?- X #> Y, copy_term_nat(X,C). % syntactic version
Y#=<X+ -1.

In general, maintaining copies of constraints is quite complex, better avoid it or treat it more generally. SICStus offers only a purely syntactic copy_term/2. If you want more, you need to use copy_term/3.