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 ?
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. So, the following might be true.
But I am not sure at this moment.
compareU(=, X,Y), compareU(=,Y,Z)) -> compareU(=,X,Z)
Yes persistent, almost trivial, but in case of “undecidable”, I don’t want one answer one time and a different answer the next.
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.
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)].
I respect C programmars as well as mathematicians.
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?
Thanks for correction.
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.
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.
Thank you for help.
With @@<<, x, y being the same as:
(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.
It seems the struggle is real! Struggle for some formulas,
but never consider an inconsistency?
It directly leads to an inconsistency. Since a strict comparison
should satisfy asymmetry, besides transitivity:
Asymmetric relation
if aRb then bRa must not hold.
https://en.wikipedia.org/wiki/Asymmetric_relation
Edit 31.03.2023
I also used asymmetry in my proof when I stated Lab, ¬Lba.
An alternative proof would be, only now the proof is a litte longer:
/* Asymmetric Relation */
∀x∀y(Lxy→ Lyx),
/* Lexical Ordering */
∀x∀y∀z∀t(Ls(x,y)s(z,t) ↔ (Lxz ∨ (x=z ∧ Lyt))),
/* Example A,B satisfies A @< B */
Lab,
/* Example A,B is A=s(B,c) and B=s(A,d), proof works for any c,d */
a=s(b,c), b=s(a,d)
/* We can derive a Contradiction */
entails p∧¬p.
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.
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.
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.