mthom / scryer-prolog

A modern Prolog implementation written mostly in Rust.
BSD 3-Clause "New" or "Revised" License
2.01k stars 118 forks source link

dif/2 residuals could sometimes be more compact #2540

Open triska opened 2 weeks ago

triska commented 2 weeks ago

Example:

?- dif(a(X), a(1)).
   dif:dif(a(X),a(1)). % correct
   dif:dif(X,1).       % ideal
|  dif:dif(1,X).       % also correct
infradig commented 2 weeks ago

Cute, but then you can end up with stuff like this...

$ swipl -q ?- dif(a(X), a(1)). dif(X, 1).

?- dif(a(X,Y,Z), a(1,2,3)). dif(f(X, Y, Z), f(1, 2, 3)).

triska commented 2 weeks ago

To clarify: I do not mean to change only the projection of residual goals, but that the internal storage of the constraint can be simplified to this. The projection should not apply extra steps to simulate a simplification that is not actually present in the internal propagation mechanism, because if it does then we may not even know that there is such an opportunity for improvement! For this reason, the projection should be kept simple and should report what is actually present.

A simplified residual goal in this case will be a natural consequences of such internal improvements.

bakaq commented 2 weeks ago

My intuition is that this simplification will be kind of hard to implement. I remember trying to do it when I improved the dif/2 implementation (because it seems kinda obvious), and it not working for some reason (I don't remember exactly why). May have something to do with cyclic terms.

hurufu commented 2 weeks ago

To my untrained eye it looks like that to make it work one needs to compute least general unifier (like in anti-unification) and if it isn't a variable then use it.

Sidenote: Cyclic terms are strange beasts, they complicate everything, but have some cool use-cases.

UWN commented 2 weeks ago

SWI tried this. And so far failed. This is extremely complex for minor gains. Definitely a work sink. And, it is already non-trivial for terms, even worse for rational trees (with cycles).

UWN commented 2 weeks ago

@infradig: An even more unreadable case in SWI is #2029