Polish Notation with Sharing for Rational Trees

General
1

Strange this little Prolog code snippet, that creates a polish
notation with sharing out of a Prolog term, either acyclic or cyclic,
works for me to compare terms (that do not contain '$VAR'/1):

polish(X, L, T) :-
   sys_polish_term(X, [], H, T),
   sys_strip_number(H, 0, L).

Here the test cases from the top-level ticket:

?- p(X,Y), polish(p(X,Y),L,T).
L = [A=f(A), B=p(A, A)],
L = [A=f(B, D), B=a(A), C=g(B, D), D=b(C), E=p(B, D)],
L = [A=s(B, C), B=s(A, _A), C=s(C, B), D=p(B, C)],

The description “Polish” refers to the nationality of logician Jan
Łukasiewicz who invented Polish notation in 1924. You can imagine
the sharing happens by pressing the memory store and recall keys

of a HP-41C which had reverse polish. Defining a comparison as:

compare2(C,X,Y) :- polish(X,L,T), polish(Y,R,S),
   compare(C,L-T,R-S).

Has the following properties:

  • Open question whether it is conservative:
    I have mixed feelings whether it is conservative, i.e. mostlikely
    compare2/3 and compare/3 do not agree on acyclic terms.

  • It is a total order:
    Because compare2/3 falls back to compare/3, and polish
    is injective versus (==)/2, it has all desired properties.

Maybe @kuniaki.mukai can test it for me?