Careful with compare/3 and Brent algorithm

[ridgeworks]

@kuniaki.mukai

It follows from Persistency that compareU(Op, X, Y) is always true (for any Op, X, Y)
This is almost contradiction. Is this what you intend ?

Yes persistent, almost trivial, but in case of “undecidable”, I don’t want one answer one time and a different answer the next.

@kuniaki.mukai

As for Transitivity, I am not sure for now. For compare_with_stack = includes case in which X and Y are incomparable like Carlson’s pair.

As I, perhaps wrongly, interpreted the match stack algorithm: if you encounter a compound term pair that are already being compared, assume they’re equal and continue, thus avoiding an infinite loop. If there’s a subsequent argument that forces it one way or the other, then that will ripple back upon unwinding the recursive compare. I think this is what @j4n_bur53’s shallow lexical order was getting at: if undecidable, look further, not deeper.

I think you need to extend Carllson’s example to test transitivity, for example (using my logical compare):

?- A=s(B,0),B=s(C,1),C=s(A,2), comparable(OAC,A,C), comparable(OCB,C,B), comparable(OAB,A,B).
A = s(s(s(A, 2), 1), 0),
B = s(s(A, 2), 1),
C = s(A, 2),
OAC = OCB, OCB = OAB, OAB = (>).

If transitivity of compare_with_stack can’t be “proven”, are there any counter examples that fail the transitivity test?

The level of my mathematical skills is about the same as my C programming skills, so this may all be rubbish.

[kuniaki.mukai]

@ridgeworks

Yes persistent, almost trivial, but in case of “undecidable”, I don’t want one answer one time and a different answer the next.

The Persistency implies, for instance, comparable(=, a, b), comparable(<, a, b), and comparable(>, b, a) hold at the same time. It seems almost contradiction. I am afraid that your Persistency formulation is missing some additional condition.

Although I gave up transitivity of comapare_with_stack, but instead, it is used to sort lists
in a cosistent way locally (not globally) .

% ?- A=s(B,0),B=s(C,1),C=s(A,2), compare_with_stack(OAC,A,C), 
%	compare_with_stack(OCB,C,B), compare_with_stack(OAB,A,B).
%@ A = s(s(s(A, 2), 1), 0),
%@ B = s(s(A, 2), 1),
%@ C = s(A, 2),
%@ OAC = OCB, OCB = OAB, OAB = (>).

% ?- A=s(B,0),B=s(C,1),C=s(A,2), semi_lex_sort([A,B,C,C,A], S).
%@ A = s(s(s(A, 2), 1), 0),
%@ B = s(s(A, 2), 1),
%@ C = s(A, 2),
%@ S = [s(s(A, 2), 1), s(A, 2), s(s(s(A, 2), 1), 0)].

@ridgeworks

The level of my mathematical skills is about the same as my C programming skills, so this may all be rubbish.

I respect C programmars as well as mathematicians.

[ridgeworks]

@kuniaki.mukai

The Persistency implies, for instance, comparable(=, a, b), comparable(<, a, b), and comparable(>, b, a) hold at the same time.

Did not know that, so that’s not the definition I was using. My definition was “once true, always true”, so number(T) is “persistent”, var(T) is not. Is there a term for that?

[kuniaki.mukai]

Thanks for correction.

[kuniaki.mukai]

@ridgeworks

• Persistence: (compareU(Op,X,Y), compareU(Op,X,Y)) is always true.

I read this as

for all OP, X, and Y, it is true that ( compareU(Op,X,Y) and compareU(Op,X,Y) ).

Is this wrong reading ?

[ridgeworks]

@kuniaki.mukai

I read this as

for all OP, X, and Y, it is true that ( compareU(Op,X,Y) and compareU(Op,X,Y) ).

Is this wrong reading ?

It’s meant to be read as Prolog so yes but Op, X and Y have the same values for both calls to compareU since they’re the same logic variables. Also replace ‘and’ with ‘,’ which in Prolog means “and-then”. Is there a better way to express this?

It’s a trivial point but I thought something had to be stated due to the undecidability of Carllson’s example.

[kuniaki.mukai]

There exists a relation say @@<< on rational trees which extends the standard lexical order @< on Herband terms. @@<< is coinductively defined from @<.

Let rational trees x y be Matt Carllson’s pair x=f(y,0), y=f(x,1).
I noticed that I have not a proof of either x @@<< y or y@@ << x.
If both of x @@<< y and y@@ << x are false then both of

x @@<< y => y@@ << x,
y @@<< x => x@@ << y

are vacuously true.

( then also x @@<<y, y@@x => x=y)

Perhaps I am wrong at somewhere. But, to be honest, I can’t eliminate this logical possibility.
Help me if you have answer to this.

[kuniaki.mukai]

Thank you for help.

With @@<<, x, y being the same as:

@kuniaki.mukai

There exists a relation say @@<< on rational trees which extends the standard lexical order @< on Herband terms. @@<< is coinductively defined from @<.

Let rational trees x y be Matt Carllson’s pair x=f(y,0), y=f(x,1).

(Conjecture) Both of the following hold.

• x @@<< y

• y @@<< x

This is tentative conjecture. In fact, I wrote compare_with_stack assuming both of them implicitly without proof.

As it depends on the definition of @@<< built from @< by coinduction, I have to review the
construction itself. Thus, depending on the conjecture, there is room for that @@<< is trasitive,
though it seems unlikely in my intuition. Anyway this is just a speculation for the time being.

[kuniaki.mukai]

@j4n_bur53

but never consider an inconsistency?

@kuniaki.mukai

(Conjecture) Both of the following hold.

• x @@<< y
• y @@<< x

Now I am 100 % sure on this conjecture.
The existence of @@<< as the largest fixipoint of the operation F (which was posed) is clear. Then add the above two to the fixpoint. Clearly the extended one, say R satisfies R\subset F(R). As @@<< is such a largest one, it follows that R= (@@<<). (This is a typical argument on coinductive construction)

If this is right, despite of simplicity, the monotone operator F may not be appropriate to define lexical ordering on rational trees.

In fact, I am thinking about not so complicated alternatives which gives a lexical ordering directly on rational trees.

[kuniaki.mukai]

Persistency on ordering is important. In fact,
my compare_with_stack and semi_lex_sort take care maximally for that . However global pesistency is difficult for them. I have no idea for global persistency, but I would like to encourage those who try to find a way to that.

[kuniaki.mukai]

@j4n_bur53

There is no such requirement as “persistence”, as mentioned by @ridgeworks .
This might have some motivation, but it doesn’t belong to what is usually
listed for a strict comparison, that is not necessary a lexical order.

As for me, I mean by persistency a way of giving a total order < to a set A
which is given a binary relation R. For example,
linearise R= {(a, b), (a, c), (b, d), (c, d)} to a < b < c < d
as far as conservatively.

[kuniaki.mukai]

I have extended the history stack for union-find usage so that it is no mre necessay
to build bisimulation for compareing cyclic terms. It seems work well with using only same_term/2. It was strange for me that despite of my naming I never saw occasions for popup operations but only pushing pairs of terms indexes. I observe that with the stack I used only limited features of union-find. I guess the use of ==/2 on compare_with_stack/3 for scanning the stack may explains why it works. ==/2 plays hidden role of union-find in invisible way, which is my guess.

[j4n_bur53]

@kuniaki.mukai

I have extended the history stack for union-find usage

Any equivalence based approach that uses compare_index/3
will bang its head at Mats Carlson’s example. Not the exact
same example in the arguments but a related one

when compare_index/3 is doing its work recursively.
Just a triple X, Y, Z that hits Mats Carlsons example from
different angles. The offending definition is this clause:

compare_term_args(I, C, X, Y, A, H):-
		arg(I, X, K),
		arg(I, Y, L),
		!,
		compare_index(D, K, L, A, H),
		(	D = (=) ->
			I0 is I + 1,
			compare_term_args(I0, C, X, Y, A, H)
		;	C = D
		).
compare_term_args(_ ,= , _, _, _, _).

It will always violate Matt Carlsons counter example,
when confronted with a certain tripples. Instead of
s(A,X) you can also use A-X, its the same term

left recursion, like I am doing here in this thread
when I use rational number derived sequences.

comparing infinite terms - 16.07.1996
Mats Carlsson
https://groups.google.com/g/comp.lang.prolog/c/Om8bTZ_Mom4/m/uTPb727mMTUJ