SWI-Prolog / swipl-devel

SWI-Prolog Main development repository
http://www.swi-prolog.org
Other
984 stars 176 forks source link

system:compare/3 violates transitive ordering for rational trees (cyclic terms) #1159

Open ridgeworks opened 1 year ago

ridgeworks commented 1 year ago

For example:

?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)), compare(A,X,Y), compare(B,Y,Z), compare(C,X,Z).
X = f(X, a(X)),
Y = f(Y, b(Y)),
Z = f(Y, c(Y)),
A = B, B = (<),
C = (>).

Also:

?- A = s(A,A), B = s(C,1), C = s(C,s(1,C)), compare(O1,A,B), compare(O2,B,A).
A = s(A, A),
B = s(_S1, 1), % where
    _S1 = s(_S1, s(1, _S1)),
C = s(_S1, s(1, _S1)),
O1 = O2, O2 = (<).

This issue was first identified in

https://swi-prolog.discourse.group/t/how-to-compare-3-without-surprises-on-non-ground-terms/6386

with much additional discussion in https://swi-prolog.discourse.group/t/history-dependent-semi-lex-compare-3/6431, https://swi-prolog.discourse.group/t/fixing-the-compare-3-mirror-anomaly-in-swi-prolog/6438, and https://swi-prolog.discourse.group/t/cheap-compare-for-cyclic-terms-injective-collation-keys/6427.

A compare on cyclic terms based on lexical ordering is undecidable (see <https://groups.google.com/g/comp.lang.prolog/c/Om8bTZ_Mom4/m/uTPb727mMTUJ 1>) and Sicstus has documented the issue:

Please note : the standard order is only well-defined for finite (acyclic) terms. There are infinite (cyclic) terms for which no order relation holds. https://sicstus.sics.se/sicstus/docs/3.12.11/html/sicstus/Term-Compare.html 2

If the requirement for a sort based on lexical ordering is dropped, at least one approach, representative compare -https://swi-prolog.discourse.group/t/cheap-compare-for-cyclic-terms-injective-collation-keys/6427 has been identified which appears to preserve correct ordering of cyclic terms.

Ordering of terms is something fundamental to Prolog affecting basic sorting and libraries alike, e.g., library(rbtrees). Limitations of comparison of cyclic terms should be documented (like Sicstus), fixed (system:compare/3), or some combination thereof. Perhaps something like "representative compare" could be added to library(terms) for those rare applications which require cyclic term comparison.

JanWielemaker commented 1 year ago

This issue has been mentioned on SWI-Prolog. There might be relevant details there:

https://swi-prolog.discourse.group/t/history-dependent-semi-lex-compare-3/6431/56

JanWielemaker commented 1 year ago

This issue has been mentioned on SWI-Prolog. There might be relevant details there:

https://swi-prolog.discourse.group/t/fixing-the-compare-3-mirror-anomaly-in-swi-prolog/6438/4

JanWielemaker commented 1 year ago

This issue has been mentioned on SWI-Prolog. There might be relevant details there:

https://swi-prolog.discourse.group/t/cheap-compare-for-cyclic-terms-injective-collation-keys/6427/5

Jean-Luc-Picard-2021 commented 1 year ago

Its relatively straitght forward to implement naish/2 natively. Follow the following steps:

But depending on how your original copy_term/2 worked, it might not do the right thing. You can compare with the naish/2 reference implementation in Prolog only.

Difficulty is keeping injectivity versus (==)/2, a Brent algorithm without Brent adjustment might not do it correctly.