Different behaviout in trace mode and non-trace mode

Help!
1

This code comes from a programming mistake where the following code is expected to behave like if-then-else instead of a disjunction:

?- ((true -> X=a), true); X =b.
X = a ;
X = b.

This is a disjunction because the left hand side’s top level functor is , and not -> such that the unification with the if then else pattern fails:

?- (((true -> X=a),true); X =b) = ((C->G1);G2).
false.

When I turn on trace mode, the second solution is suddenly lost:

[trace]  ?- ((true -> X=a),true); X =b.
   Call: (9) true ? creep
   Exit: (9) true ? creep
   Call: (9) _5566=a ? creep
   Exit: (9) a=a ? creep
   Call: (9) true ? creep
   Exit: (9) true ? creep
X = a .

[trace]  ?-

Does someone know why this happens?

2

Welcome.

Is this related to this StackOverflow question?

Out of curiosity are you lambda.xy.x at StackOveflow? If so, thanks for asking here, I too would like to learn more about this.

3

Yes, sorry, I should have linked the SO question - I didn’t want to do some self-advertising but wanted to pick up on the suggestion to ask here.

4

Thanks. :clap:

I was the one who made the suggestion. I am GuyCoder at StackOverflow.

6

Thank you, typical problem between keyboard and computer!

8

The first query works for me as well:

?- (trace, (true -> X=a)); X=b.
   Call: (9) true ? creep
   Exit: (9) true ? creep
   Call: (9) _5288=a ? creep
   Exit: (9) a=a ? creep
X = a ;
   Call: (9) _5288=b ? creep
   Exit: (9) b=b ? creep
X = b.

I added the parenthesis for clarity but it works also with your exact query.

10

Ah sorry, yes certainly - that’s because the term does not have that form anymore:

?- ((trace, (true -> X=a)); X=b) = ((A -> B) ; C).
false.

If I understand it correctly, this is really a syntactic criterion.