# Quick unification question

**URL:** <https://swi-prolog.discourse.group/t/quick-unification-question/9558>\
**Category:** General\
**Created:** [March 30, 2026, 12:16am UTC](https://swi-prolog.discourse.group/t/quick-unification-question/9558 "2026-03-30T00:16:27Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![emummel20](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/emummel20/32/4952_2.png) [@emummel20](https://swi-prolog.discourse.group/u/emummel20)\
**Post date:** [March 30, 2026, 12:16am UTC](https://swi-prolog.discourse.group/t/quick-unification-question/9558/1 "2026-03-30T00:16:27Z")

</div>

Hi, quick question:

```prolog
?- 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](https://www.swi-prolog.org/pldoc/man?section=compare#:~:text=Compound%20terms%20are%20first%20checked%20on%20their%20arity%2C%20then%20on%20their%20functor%20name%20(alphabetically)%20and%20finally%20recursively%20on%20their%20arguments%2C%20leftmost%20argument%20first.):

> 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.

---

<div class="post-metadata">

**Author:** ![Boris](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/boris/32/7486_2.png) [@Boris](https://swi-prolog.discourse.group/u/Boris)\
**Post date:** [March 30, 2026, 4:34am UTC](https://swi-prolog.discourse.group/t/quick-unification-question/9558/2 "2026-03-30T04:34:51Z")

</div>

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

> [@emummel20](#):
>
> `1+2+3` is de-sugared as `+(1,+(2,3))`, correct?

It seems that it is _not_ parsed as `+(1,+(2,3))`. This depends on the [operator](https://www.swi-prolog.org/pldoc/man?section=operators) definition for `+`. You check the docs for op/3 (see the table at the bottom) and also query it using current\_op/3:

```prolog
?- 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:

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

```

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

```prolog
?- 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](https://swi-prolog.discourse.group/t/seeming-inconsistency-between-ground-1-and-nonvar-2-predicates/8634/9). 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:

```plaintext
?- 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.

```

---

<div class="post-metadata">

**Author:** ![brebs](https://avatars.discourse-cdn.com/v4/letter/b/e9c0ed/32.png) [@brebs](https://swi-prolog.discourse.group/u/brebs)\
**Post date:** [March 30, 2026, 10:10am UTC](https://swi-prolog.discourse.group/t/quick-unification-question/9558/3 "2026-03-30T10:10:47Z")

</div>

> [@emummel20](#):
>
> ?- 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?

Both are rather misleading, looking like arithmetic 😉

Can use clp, e.g.:

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

```

What are you _really_ trying to do?

---

<div class="post-metadata">

**Author:** ![emummel20](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/emummel20/32/4952_2.png) [@emummel20](https://swi-prolog.discourse.group/u/emummel20)\
**Post date:** [March 31, 2026, 7:13pm UTC](https://swi-prolog.discourse.group/t/quick-unification-question/9558/5 "2026-03-31T19:13:40Z")

</div>

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

Yes,

```prolog
?- 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](https://youtu.be/KJ8uZiWpomg?si=KKXC-SQBo7sDWi2z&t=566) 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!
