Instability of standard order

jan · September 21, 2026, 2:31pm

The discussion has been here before: standard order of terms is complete (except cyclic terms ), but unstable, i.e.,

X @< a, X = b

succeeds, but a @< b rather than a @> b. I wonder whether we should have a variant of compare/3 that fixes this. I see two sensible behaviours: a compare/3 variant that raises an instantiation exception and one that tells us which comparison decides. The implementation of compare/3 at some point stumbles on a variable. That means we cannot decide (unless the other side is the same variable, e.g., X==X). We can return a pair indicating the undecidable comparison, so we get

?- compare_ex(Diff, f(a), f(X)).
Diff = compare(a, X)

The sad thing is that instantiation_error has no culprit. Else, we could also consider

?- catch(compare_ex(Diff, f(a), f(X)), E, true).
E = error(instantiation_error(compare(a,X), _).

I know we can use the second argument. That is nice for a message, but not for something you want to act upon. Of course, the disadvantage is that normal computation may need to use catch/3, something I’ve never liked.

Opinions? Existing practice?

brebs · September 21, 2026, 4:00pm

I found compare/3 to be disappointingly illogical as a learner

Exceptions are a last resort, for when there are no other reasonable actions… how about, for a point-in-time comparison:

compare_sound(C, X, Y) :-
    (   X \= Y
    ->  compare(S, X, Y),
        % Will be < or > sign
        C = comp(S)
    ;   X == Y
    ->  C = comp(=)
        % Insufficiently instantiated for sound comparison
    ;   C = insuf
    ).

Results:

?- compare_sound(C, A, A).
C = comp(=).

?- compare_sound(C, b(_), a(_)).
C = comp(>).

?- compare_sound(C, A, B).
C = insuf.

I think these results would be the least surprising for a learner.

kwon-young · September 21, 2026, 6:38pm

hm, I heavily rely on being able to compare 2 variables and ground terms with variables in my egraph implementations.
In my case, the current status quo is okay I found…

jan · September 21, 2026, 6:39pm

I thought about this as well. It is not correct. consider compare(D, f(X, a), f(x, b)). These do not unify, but their comparison is unstable. The current working hypothesis is to introduce

 partial_compare(?Dif, @T1, @T2)

Which will unify Dif with one of >, =. < or undefined(X,Y), which expresses that we can not decide, but Dif is the same as compare(X,Y) when we can compare. Related, there is a proposal for

must_compare(Dif, T1, T2)

which raises an instantiation_error if the above returns undefined(,). Finally,

compare_when(Dif, T1, T2)

Which could act as a constraint, i.e., delays if we cannot decide now.

brebs · September 22, 2026, 7:13am

How about this idea - work in progress:

compare_sound(C, X, Y) :-
	compare(Comp, X, Y),
	(	Comp == (=)
        % Trustworthy equality
	->	C = Comp
	;	ground(X),
		ground(Y)
        % Trustworthy comparison
	->	C = Comp
	;	X \= Y,
		% Prevent attributed variables from interfering with later comparison
		copy_term(X, XC, _),
		copy_term(Y, YC, _),
		var_to_simple_list(XC, XL),
		var_to_simple_list(YC, YL),
		walk_vars_to_first_term_variable(XL, YL, FTV),
		(	first_term_variable_does_not_change_comparison(Comp, XC, YC, FTV)
		->	C = Comp
		;	C = insuf
		)
	;	C = insuf
    ).

walk_vars_to_first_term_variable(XL, YL, FTV) :-
	(	var(XL)
	->	FTV = XL
	;	var(YL)
	->	FTV = YL
	;	XL = [H|_],
		var(H)
	->	FTV = H
	;	YL = [H|_],
		var(H)
	->  FTV = H
	;	XL = [XH|_],
		YL = [YH|_],
		var_to_simple_list(XH, XSL),
		var_to_simple_list(YH, YSL),
		walk_vars_to_first_term_variable(XSL, YSL, FTVW)
	->	FTV = FTVW
	;	XL = [_|XT],
		YL = [_|YT],
		walk_vars_to_first_term_variable(XT, YT, FTV)
	).

var_to_simple_list(V, L) :-
    % To be able to walk through the variable's components
	(	atomic(V)
	->	L = V
	;	V =.. L
	).

first_term_variable_does_not_change_comparison(Comp, XC, YC, FTV) :-
    % TODO: Compare with instantiated extremities, to test that comparison result does not change

The method is basically:

if compare/3 gives =, or both variables are ground, then the result is trustworthy
Otherwise “walk” through both variables together until the first var
Run compare/3 with var temporarily instatiated to a lower then higher extremity, to check that the compare/3 result does not change - if it does not change, it is trustworthy

This should be easier than reimplementing the standard order’s subtleties. Hopefully

jan · September 22, 2026, 7:28am

It is lacking some high level description … The idea behind partial_compare/3 is that it is a good and fast to implement primitive that allows building higher level primitives. It simply does the normal compare/3, but when it encounters a comparison between a variable and anything but the same variable, it “returns” undecided(Var,Other). Now, this not always the end of the story. We could have

?- A in 1..6, partial_compare(D, A, a).

That results in undecided(A, a) and the constraint reasoner can decide this means <, as all integers are '@<'/2 to all atoms. In some cases a constraint reasoner could decide the undecided is always =. In that case the values are equal, so we can unify them and try again.

brebs · September 22, 2026, 7:52am

Is there a lowest (and highest) possible ground value, to use in compare/3, that works when compared to any datatype?

jan · September 22, 2026, 8:44am

partial_compare/3 is now in the git (can change if someone comes up with something better). Not really clear what should be provided on top, as this is mostly a building block, similarly like unifiable/3. Some candidates:

must_compare(?Diff, @Term1, @Term2)
As compare/3, but throws instantiation_error in case the comparison is unstable.
compare_when(?Diff, @Term1, @Term2)
As compare/3, but delays (is a constraint).
ord_stable(@List)
true if List is a stable ordered set.
stable_assoc(@Assoc)
rb_stable(@RbTree)
…

Or just leave it to the imagination of the users …

abaljeu · October 2, 2026, 5:18pm

Who depends on stable order with unbound variables that may become bound? I might to a (when(ground(X), X @< a → ; ), but if I’m doing X @< A and X is not ground it’s because I am committed to never grounding X, or I know the variable is not the key in differentiating order.

kuniaki.mukai · October 3, 2026, 5:13am

Subject (or Reply): Observation: Non-transitivity in cyclic term sorting vs. robustness of DFA minimization

Hi all,

While I haven’t been able to follow every detail of this extensive thread, I ran into an interesting empirical finding while testing Jan’s term_automaton/2 and automaton_minimal/3 that might be of interest to the discussion.

When sorting random ground cyclic terms (N=1000), I noticed occasional discrepancies between the built-in sort/2and a sort based on minimal automata (rt_sort):

Prolog

?- rt_sort(GroundNs, S1), sort(GroundNs, S2), S1 \== S2.

Investigating the difference revealed that this is not caused by deduplication differences, but by a violation of transitivity in the built-in standard order comparison for cyclic terms. Specifically, we can isolate concrete pairs where:

Direct comparison yields A<B in both compare/3 and rt_compare/3:

Prolog

?- compare(C1, A, B), rt_compare(C2, A, B).
%@ C1 = C2, C2 = (<).

Yet in sort/2 (S2), B is placed before A:

Plaintext
```
Pos(B) in S2 = 522
Pos(A) in S2 = 524
```

Because cyclic term comparison via cycle-detection traversal can depend on traversal paths and pointer identities, transitivity (X<Y∧Y<Z⟹X<Z) occasionally breaks down during sorting, causing sorting anomalies depending on which pairs the sort algorithm compares first.

By contrast, normalizing the terms upfront via Paige-Tarjan minimization (automaton_minimal/3) establishes a canonical, path-independent state representation. Although it is computationally a more round-about route, it strictly preserves a mathematically sound total order and avoids these ordering paradoxes altogether.

Just sharing this observation in case it provides useful context for the ongoing discussion on rational term comparison semantics and robustness.

jan · October 3, 2026, 7:49am

I think that is true. It is just too costly as a default compare/3 implementation I was hoping that we can use this only for the complicated cases, which we already identify. Unfortunately that does not seem to work. I should still look at the proof (a counter example found by Claude).

kuniaki.mukai · October 3, 2026, 12:23pm

I agree with the current approach.

BTW. Comparing rational trees directly using the output of term_automatonwithout minimization should work correctly.

Also I have an idea to detect cycles directly in O(1) without scanning the stack, so I will test this in C as a small hobby project. I will let you know if I obtain any noteworthy benchmark results.

jan · October 3, 2026, 12:28pm

You have to minimize the automaton, no? Than you should indeed get a total ordering, but again different from ISO compare/3 The problem is that we need a total ordering that is depth-first-left-right as that is what a lot of existing code expects.

jan · October 3, 2026, 12:50pm

The issue got concrete when faced with the requirement to define (@<)/2, etc. as a constraint. If the order is already stable, you are fine. Else you want to find the variable that is first compared to something and delay on that. when(ground(...) is too strong.

Then, there have been various suggestions that e.g., library(assoc) should require its key to be ground. That is too tight. They just need a stable order or, indeed, the user must be aware that the order may change. The new incomparable flag allows you to spot possible bugs caused by violating these assumptions. Few applications will want this flag, but it can be a good safely net and debugging tool.

kuniaki.mukai · October 3, 2026, 2:22pm

Jan,

I see your point about the compatibility expectations for the standard order.

My primary goal right now is simply to investigate the total ordering mathematically and explore the cycle-detection performance in C without getting stuck in specification details.

I will experiment on my side first. Thanks for the clarification!

kuniaki.mukai · October 5, 2026, 2:36am

Subject: Experimental result on rational tree comparison / Request regarding term_automaton

I would like to share a brief experimental result regarding the comparison of rational trees, without getting into deep theoretical discussions.

Using a fast C-based state-pair stack traversal (fast_rt_compare), I tested whether the comparison order on raw automata directly generated from terms matches the order obtained after Paige-Tarjan minimization (fast_rt_min_compare).

In an experiment comparing 1,000,000 randomly generated cyclic term pairs:

All 1,000,000 pairs yielded completely identical comparison results (<, =, >).
The order on raw automata appears to be consistent with the minimized canonical order in practice.

Also, for our experiments, having built-in support for term_automaton/2 (or automaton/3) in SWI-Prolog would be very helpful.

kuniaki.mukai · October 5, 2026, 3:49am

Title: Benchmark: C-based pair-stack vs. Automaton-based comparison for rational trees

Hi all,

I would like to share a brief benchmark comparison between different rational tree comparison implementations on SWI-Prolog.

Benchmark Setup

Repeated 1,000,000 iterations for a fixed pair of random cyclic terms (X,Y).
Comparison targets:
1. fast_rt_compare/3: C-based pair-stack traversal directly on raw terms.
2. fast_rt_min_compare/3: C-based pair-stack traversal with minimization.
3. rt_compare/5 (raw): Comparison over raw term_automaton/2 representation (pre-converted outside the loop).
4. rt_compare/5 (min): Comparison over Paige-Tarjan minimized automaton (pre-converted outside the loop).

% ===================================================================
% Benchmark: fast_rt_compare vs fast_rt_min_compare vs rt_compare
% ===================================================================

% ?- benchmark_compare(1000000).
%@ Generating test terms...
%@ @(S_1,[S_1=h(h(h(h(S_1,S_1,S_1),h(S_1,S_1,S_1),g(S_1,S_1,S_1),h(S_1,S_1,S_1,S_1))),h(h(f(S_1,S_1,S_1),h(S_1)),f(g(S_1,S_1,S_1,S_1,S_1)),h(g(S_1,S_1),g(S_1,S_1,S_1,S_1,S_1))),h(h(h(S_1),h(S_1,S_1,S_1),f(S_1,S_1,S_1),h(S_1,S_1,S_1,S_1,S_1),h(S_1,S_1,S_1,S_1)),f(h(S_1,S_1),g(S_1),h(S_1,S_1,S_1))),h(h(g(S_1,S_1,S_1),g(S_1,S_1,S_1,S_1,S_1)),f(f(S_1,S_1,S_1),h(S_1),h(S_1,S_1,S_1,S_1,S_1)),h(f(S_1,S_1,S_1))),g(g(h(S_1,S_1,S_1,S_1,S_1),h(S_1,S_1,S_1,S_1,S_1),g(S_1,S_1,S_1,S_1),f(S_1),f(S_1,S_1)),h(f(S_1),h(S_1,S_1,S_1,S_1,S_1),f(S_1,S_1,S_1),f(S_1,S_1)),h(h(S_1,S_1,S_1,S_1,S_1),h(S_1,S_1,S_1,S_1,S_1),g(S_1,S_1),h(S_1,S_1,S_1),f(S_1)),h(f(S_1,S_1),f(S_1),g(S_1,S_1,S_1),g(S_1,S_1,S_1)),h(g(S_1),h(S_1,S_1,S_1,S_1),f(S_1,S_1))))])
%@ @(S_1,[S_1=f(h(f(g(S_1,S_1,S_1)),h(g(S_1,S_1,S_1),f(S_1,S_1))),f(f(f(S_1,S_1,S_1),g(S_1,S_1,S_1)),g(f(S_1,S_1,S_1,S_1)),h(h(S_1,S_1,S_1),g(S_1,S_1,S_1,S_1),f(S_1,S_1,S_1),f(S_1)),h(g(S_1,S_1),f(S_1,S_1),f(S_1,S_1,S_1,S_1),f(S_1,S_1)),f(g(S_1,S_1,S_1),f(S_1,S_1,S_1,S_1))),f(f(g(S_1,S_1,S_1,S_1)),f(h(S_1),g(S_1,S_1),f(S_1,S_1,S_1),g(S_1,S_1,S_1,S_1)),h(g(S_1,S_1,S_1,S_1,S_1),f(S_1,S_1),g(S_1,S_1)),g(f(S_1,S_1,S_1),f(S_1,S_1),h(S_1,S_1,S_1,S_1),f(S_1,S_1,S_1))),h(h(h(S_1,S_1),g(S_1,S_1)),f(g(S_1,S_1,S_1,S_1,S_1),h(S_1),f(S_1,S_1)),g(h(S_1,S_1),h(S_1,S_1,S_1,S_1),f(S_1,S_1),h(S_1,S_1),h(S_1)),f(g(S_1,S_1,S_1,S_1,S_1))))])
%@ 
%@ --- 1. fast_rt_compare (C stack, raw terms) [1000000 iterations] ---
%@ % 11,999,999 inferences, 5.831 CPU in 5.853 seconds (100% CPU, 2057990 Lips)
%@ 
%@ --- 2. fast_rt_min_compare (C stack, with minimization) [1000000 iterations] ---
%@ % 17,999,999 inferences, 16.863 CPU in 16.918 seconds (100% CPU, 1067431 Lips)
%@ 
%@ --- 3. rt_compare (raw automaton) [1000000 iterations] ---
%@ % 2,999,999 inferences, 0.296 CPU in 0.297 seconds (99% CPU, 10142019 Lips)
%@ 
%@ --- 4. rt_compare (minimized automaton) [1000000 iterations] ---
%@ % 2,999,999 inferences, 0.294 CPU in 0.296 seconds (100% CPU, 10189349 Lips)
%@ true.
```

### Notes

* Once converted into automaton tables outside the loop, `rt_compare/5` runs very fast (\~0.34s / 1M calls), with essentially no speed difference between raw and minimized tables.

* For direct term comparison, `fast_rt_compare/3` (without prior minimization) runs about 2x faster than `fast_rt_min_compare/3`.

* In a separate consistency test over 1,000,000 random cyclic term pairs, `fast_rt_compare/3` and `fast_rt_min_compare/3` produced identical ordering results in all cases.

Just sharing the benchmark data for reference.

Best regards,

Kuniaki Mukai

EDIT 2026/10

I would like to report the results of this experiment on the rational tree ordering:
Minimization via Jan's automaton_minimal/3 turned out to be strictly essential.
I have not yet analyzed why term_automaton/2 alone unexpectedly fails transitivity.
This update is a C implementation of my earlier Prolog prototypes that satisfied transitivity.
The algorithm uses cycle length information, though it remains unclear to me why incorporating cycle length is so effective.

Topic		Replies	Views
How to compare/3 without surprises on non-ground terms? Help!	81	2698	March 31, 2023
Undecidable order (some cyclic terms) Request For Comments	7	150	October 2, 2026
Cyclic terms unification `X=f(f(X), X), Y=f(Y, f(Y)), X = Y. ` General	70	1455	August 29, 2025
Fast Term Factorization via Paige-Tarjan: Bypassing ==/2 and compare/2 General	16	280	July 15, 2026
On sorting non-ground terms and the standard order of terms General	26	2081	January 2, 2020

Instability of standard order

Benchmark Setup

Related topics