Hi,
I have no clue when guys are talking about
“Note that your X and Y are incomparable”
“but it does not restore the transitivity claim”.
My test case here had always 3 terms, X, Y and Z:
?- [user].
test(X,Y,Z) :-
X=f(X,0),Y=f(Y,1),Z=f(X,Y).
Transitivity was a problem of the many attempts of
Kuniaki Mukai. It is a totally different problem
than the Matt Carlsson counter example, which
consistes of only two terms X and Y. You cannot
show something about transitivity with only two
terms X and Y. Since transitivity is a law about 3 terms:
/* Transitivity */
X < Y & Y < Z => X < Z
If you would use Claude and random terms correctly
you would on the other hand find example that violate this.
But the coin flip is entirely on the side of random terms,
/* Lexicality */
s(X,Y) < s(X2,Y2) <=> (X < X2) & (X == X2 & Y < Y2)
The coin flip has nothing to do with the compare/3
implementation or standard order or incomparable
terms. The coin flipping is used to sample a large
sample space , by randomly generating samples. So as to
find counter examples either to Transitivity, which needs 3
sample terms or to Lexicality which needs 2 sample term.
It is enough to make a Law crumble by a single sample of n
terms if the Law speaks about n terms. Laws are typically
tested against concrete or prototypical compare/3 implementations.
Bye
BTW: Matts Carlsson’s example uses only two terms, since
for the Lexical Law, he used s(A,0) = B and s(B, 1) = A. But my
tripple is not an example of the sort that would reduce the number
of required witnesses for the Law of Lexicality of the s/2 Functor.