Quick unification question

General
1

Hi, quick question:

?- X+Y = 1+2+3.
X = 1+2,
Y = 3.

Is it expected we don’t get a choice point for X = 1, Y = 2+3.? Would that not satisfy the unification as well?

I did find this:

Compound terms are first checked on their arity, then on their functor name (alphabetically) and finally recursively on their arguments, leftmost argument first.

Is this unification rule the cause here? Can you clarify? 1+2+3 is de-sugared as +(1,+(2,3)), correct? Doesn’t that make the left most argument 1? Is there any way to force the alternative unification here? Thanks.

2

This has more to do with operators than unification. What matters here is how the expression 1+2+3 is parsed.

It seems that it is not parsed as +(1,+(2,3)). This depends on the operator definition for +. You check the docs for op/3 (see the table at the bottom) and also query it using current_op/3:

?- current_op(Precedence, Type, +).
Precedence = 200,
Type = fy ;
Precedence = 500,
Type = yfx.

In the expression 1+2+3 you have the yfx “+” twice, so it parses unambiguously to +(+(1,2),3). I checked this using display/1:

?- display(1+2+3).
+(+(1,2),3)
true.

It seems that operators cannot have multiple definitions: you can redefine + (don’t do it :smiley: ) but then you will only get the other parsing:

?- op(500, xfy, +).
true.

?- display(1+2+3).
+(1,+(2,3))
true.

It really depends on what you are doing. Maybe you could:

  • redefine + only for a module to be xfy instead of yfx;
  • parenthesize your expression as 1+(2+3);
  • parse the expression yourself.

The last one is trivial if you have already tokenized it. But it is more important what exactly it is that you are after.

PS: Hmmm, it seems we have been here before. Back then you asked, “what is the use case for (X,Y) besides simply holding values” and my answer would have been “you can use parentheses to parenthesize correctly”. For example, you cannot stuff X, Y inside the parentheses of a compound term since it will parse as two arguments. With display/1 again:

?- display(x, y).
ERROR: stream `x' does not exist
ERROR: In:
ERROR:   [13] write_term(x,y,[quoted(true),...|...])
ERROR:   [11] toplevel_call(user:user: ...) at lib/swipl/boot/toplevel.pl:1529
ERROR: 
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.

?- display((x, y)).
','(x,y)
true.
3

Both are rather misleading, looking like arithmetic :wink:

Can use clp, e.g.:

?- use_module(library(clpq)).
?- { X + Y = 1 + 2 + 3 }.
{Y=6-X}.

What are you really trying to do?

4

Not when you call (=)/2, since it is a deterministic predicate.
It doesn’t leave any choice points only bindings. Well there
is an exception, if the terms have attributed variables,

it might also leave choice points. But to view a term under
associativity (A + B) + C = A + (B + C), and have some non-
deterministic answers, you would need to program your

own equality. In FOL+ it would come automatically by adding
associativity. But in Prolog you cannot change (=)/2 itself.
So you could try for example your own equality equals/2:

equals(X, Y) :- 
    add_to_list(X, H, []), 
    add_to_list(Y, H, []).

:- table add_to_list/3.
add_to_list(X+Y) -->  
    add_to_list(X), 
    add_to_list(Y).
add_to_list(X) -->
    [X], {integer(X)}.

I am using the table/1 directive (sic!) because add_to_list/3
is left recursive. It seems to work, we didn’t say anything about
commutativity, you will see the Catalan Number C_3 = 5:

?- equals(1+2+3+4,(1+2)+(3+4)).
true.
?- equals(1+2+3+4,(1+2)+(4+3)).
false.
?- equals(1+2+3+4,X).
X = 1+2+3+4 ;
X = 1+(2+3)+4 ;
X = 1+2+(3+4) ;
X = 1+(2+3+4) ;
X = 1+(2+(3+4)).

What is C_5 = ?, i.e. the number of ways to write 1+2+3+4+5+6 ?

5

Thanks all, appreciate the insight. Might take some time to fully digest all of it, I haven’t played around with tabling yet.

Yes,

?- X+Y = 1+2+3.
X = 1+2,
Y = 3.

?- X+Y = 1+(2+3).
X = 1,
Y = 2+3.

Is what I was looking for with “forcing” one unification or the other. Didn’t think to try that.

As far as what I’m really doing, honestly nothing specific. I was watching a power of prolog video where Markus talks about something like this and I was trying to follow along and saw an unexpected result, so I wanted to ask about it.

Thanks all!