History dependent semi_lex_compare/3

General
11

I got lost in the math but monkey testing caught my attention again. Because my version of logical compare defers on variables, I made a small mod to random_cyclic/1:

% random_cyclic(-Term)
random_cyclic(T) :-
   random_cyclic([T], T),
   numbervars(T,0,_).  % ground version

I believe comparable/3 basically uses the same strategy as compare_with_stack so I ran the follwing query several times:

between(1,1000000,_), random_cyclic(T1), random_cyclic(T2), random_cyclic(T3),
comparable(Ct,T1,T2), comparable(Ct,T2,T3), comparable(C,T1,T3), C \= Ct.

I actually had a couple of runs with no failures but most had 1 and occasionally 2; never saw more than 2.

Here’s the output from 1 run of 4,000,000 with 5 fails:

T1 = s(s(T1, A), T1),
T2 = s(_S1, 1), % where
    _S1 = s(s(_S1, 1), _S1),
T3 = s(s(_S2, A), B), % where
    _S2 = s(s(_S2, A), _S2),
Ct = (<),
C = (>) ;
T1 = s(_S1, 0), % where
    _S1 = s(_S1, 1),
T2 = _S2, % where
    _S2 = s(s(_S2, s(_S3, 1)), 0),
    _S3 = s(_S3, s(_S3, 1)),
T3 = s(T3, s(0, s(0, A))),
Ct = (>),
C = (<) ;
T1 = s(s(_S1, 0), A), % where
    _S1 = s(s(_S1, 0), _S1),
T2 = s(T2, 1),
T3 = s(s(T3, 0), T3),
Ct = (>),
C = (<) ;
T1 = _S2, % where
    _S1 = s(_S1, s(0, _S2)),
    _S2 = s(_S1, _S2),
T2 = s(_S3, A), % where
    _S3 = s(s(_S3, A), _S3),
T3 = _S4, % where
    _S4 = s(_S5, s(_S4, _S6)),
    _S5 = s(s(_S4, 0), s(_S5, 1)),
    _S6 = s(0, _S6),
Ct = (>),
C = (<) ;
T1 = s(_S1, 0), % where
    _S1 = s(s(_S1, 0), _S1),
T2 = s(_S2, B), % where
    _S2 = s(_S2, _S3),
    _S3 = s(s(s(_S2, B), A), _S3),
T3 = s(T3, s(T3, 1)),
Ct = (<),
C = (>) ;
false.

Failures are quite rare but haven’t been able to figure out what triggers them.