Scryer-prolog: Suboptimal variable names sometimes appear in answers

[triska]

For instance:

?- A*B + C #= D.
   clpz:(A*B#=_4171), clpz:(_4171+C#=D)
;  false.

vs. for example:

?- length(Ls, 4).
   Ls = [_A,_B,_C,_D].

_A, _B etc. are nice readable names, whereas for example _4171 is not.

[mthom]

This might be resolved now. There may still be edge cases.

[triska]

With the example I showed, I now get:

?- A*B + C #= D.
   clpz:(_A+C#=D)
;  false.
?- 

This is actually worse than before, because the fact that _A is arithmetically equal to A*B is now missing, and this makes the answer no longer semantically equivalent to the query.

[triska]

Related issue: #446, where apparently critical information is missing in the goal projection.

This could be a mistake in library(clpz), or in the toplevel projection code. To more easily reason about such issues, it would be nice to move the implementation of copy_term/3 to Prolog (please see #422).

[triska]

It turns out that copy_term/3 works correctly in this case:

?- A*B + C #= D, Vs = [A,B,C,D], copy_term(Vs, Vs, Gs).
   Vs = [A,B,C,D], Gs = [clpz:(A*B#=_A),clpz:(_A+C#=D), ...|...]

When displaying answers, the toplevel should collect all variables that have attributes attached, and invoke copy_term/3 to obtain their residual goals. These are the goals that must be shown as answer.

In the case above, A*B#=_A is correctly projected by copy_term/3, but the toplevel answer does not include this goal.

[mthom]

So in this case, the top-level should print all the attributes copy_term copies to Gs, even the clpz:put_atts entries? And those entries will likely contain anonymous variables named under the _A convention, which means that it will also print equations between attribute variables. That results in some very detailed feedback. I don't have a problem with it, but this is what it looks like:

?- use_module(library(clpz)).
   true.
?- A*B+C#=D.
   _A = _H, _B = _T, _C = _V, _D = _X, _E = _Z, _F = _B1, _G = _D1, _H = _A, _I = _F1, _J = _H1, _K = _J1, _L = _L1, _M = _N1, _N = _P1, _O = _R1, _P = _T1, _Q = _V1, _R = _A, clpz:(A*B#=_A), clpz:(_A+C#=D), clpz:put_atts(_B,queue([],_U)), clpz:put_atts(_C,queue([],_W)), clpz:put_atts(_D,queue([],_Y)), clpz:put_atts(_E,queue([],_A1)), clpz:put_atts(_F,queue([],_C1)), clpz:put_atts(_G,queue([],_E1)), clpz:put_atts(_I,queue([],_G1)), clpz:put_atts(_J,queue([],_I1)), clpz:put_atts(_K,queue([],_K1)), clpz:put_atts(_L,queue([],_M1)), clpz:put_atts(_M,queue([],_O1)), clpz:put_atts(_N,queue([],_Q1)), clpz:put_atts(_O,queue([],_S1)), clpz:put_atts(_P,queue([],_U1)), clpz:put_atts(_Q,queue([],_W1))
;  false.

[triska]

Yes, absolutely: copy_term/3 ought to be the central interface to project attributes to residual goals, and the toplevel should stay true to the list of goals it obtains in this way. copy_term/3 is a pure interface: It prints nothing on the terminal, everything it does is available for reasoning within Prolog, and so everything it does can be easily tested.

It's definitely not the toplevel's job to censor any goals, or to modify them in any way, because that would mean that we do not see what is actually going on. (Yes, the toplevel shortens lists etc., but there must always be a way to see the actual terms, in this case by pressing w for writing them.) This is because the toplevel emits the goals on the terminal, and therefore is very hard to test. For this reason, the toplevel should be kept as simple as possible.

Could you please briefly explain the current logic by which only a subset of goals are emitted? I think the best approach is to emit all goals that copy_term/3 yields. To shorten the list of goals by emitting those that can be omitted, the right place to do this is Module:attribute_goals//1. In this concrete case, I will modify clpz:attribute_goals//1 to remove attributes that need not be projected to goals, so that copy_term/3 no longer sees them as pending. However, I can only do this if the toplevel is absolutely honest about which attributes are there.

[triska]

If possible, please let's discuss the issue of goal projection in a call, I think it would be easier to talk about it: I currently also do not know whey there are so many queue/2 residuals, and how I can best avoid them: Deleting them in attribute_goals//1 does not seem to make them go away.

Meanwhile, I think #445 is an actual mistake in the engine, and I would appreciate if you could look into it.

[mthom]

Could you please briefly explain the current logic by which only a subset of goals are emitted?

It's messy and I'll be glad to be rid of it. In brief: the term_variables of QueryVarList are taken. QueryVarList comes from the variable_names option of read_term, essentially. Goals is computed by applying copy_term to QueryVarList appended to the list of attached attributed variables and anonymous variables. Goals is filtered according to whether its member goals share a variable with QueryVarList, and those that do are printed by the top-level.

[triska]

OK, I think this is generally a very sound approach: First, it is ideal to use the variable_names/1 option of read_term/3, with the prospect to make a portable toplevel that uses, as far as possible, only standard predicates.

The use of copy_term/3 is also very good, because this is the central pure interface to project attributes to variables.

From what I can tell at least at first glance, only the filtering is wrong, because there may be constraints that do not share any variables directly with the query, but are indirectly entangled with the query variables.

So, as a first approximation, I suggest to simply remove the filtering (i.e., the last step in your description), and emit all goals that copy_term/3 yields. We can then think about how to minimize the residual constraints, but first we must be able to see what is even there. Also, the filtering cannot happen in the toplevel, but must happen in the specific libraries and their attribute_goals//1 definitions, because the toplevel cannot make a judgement about which residuals are important.

[triska]

Also, I think copy_term/3 somehow fetches too many residual goals, but I am not sure from where (I mean whether attribute_goals//1 in library(clpz) projects too much, or copy_term/3 looks too far beyond its scope).

For example, please consider the following query:

?-  A*B+C#=D, Vs = [A,B,C,D], copy_term(Vs, Vs, Gs), writeq(Gs), false.
[clpz:(_3977*_4050#=_5995),clpz:(_5995+_4123#=_3453),clpz:put_atts(_6018,queue([],_6027)),clpz:put_atts(_6029,queue([],_6038)),clpz:put_atts(_6040,queue([],_6049)),clpz:put_atts(_6051,queue([],_6060)),clpz:put_atts(_6062,queue([],_6071)),clpz:put_atts(_6073,queue([],_6082)),clpz:put_atts(_6084,queue([],_6093)),clpz:put_atts(_6095,queue([],_6104)),clpz:put_atts(_6106,queue([],_6115)),clpz:put_atts(_6117,queue([],_6126)),clpz:put_atts(_6128,queue([],_6137)),clpz:put_atts(_6139,queue([],_6148)),clpz:put_atts(_6150,queue([],_6159)),clpz:put_atts(_6161,queue([],_6168)),clpz:put_atts(_6170,queue([],_6174))]false.

I am using false/0 at the end of the query so that we only see the goals of copy_term/3, and the toplevel does not add its own output or performs any projection.

The issue is: Where do variables such as _6018 and _6027 even come from? They do not seem to be involved with any other variables.

In any case, a good step is to let the toplevel show what's actually there. If it's too much, let's think about how to improve it starting with the complete information.

[triska]

With #450, we now have:

?- A*B + C #= D.
   _A = _H, _H = _A, _R = _A, clpz:(A*B#=_A), clpz:(_A+C#=D)
;  false.

It looks much better, doesn't it? In this example, _H and _R seem quite redundant though!

[notoria]

It may be out of subject and known but:

?- A = H, H = A, R = A.
   A = H, H = A.

In the current master.

[triska]

This is definitely a mistake, since the binding of R is missing! Very good catch!

[mthom]

It may be out of subject and known but:

?- A = H, H = A, R = A.
   A = H, H = A.

In the current master.

This should now be fixed.

[triska]

All issues raised in this thread are now brilliantly resolved, thank you a lot! #326 is one important remaining issues regarding the toplevel interaction.

We now have:

?- A*B + C #= D.
   clpz:(A*B#=_A), clpz:(_A+C#=D)
;  false.

That's close to perfect!