Undecidable order (some cyclic terms)

Request For Comments
1

A reported bug on standard order for cyclic terms (#1529) made it free to detect cyclic terms that have no defined order. As a result, SWI-Prolog now has a flag incomparable that can be set to arbitrary (default, old behaviour, i.e., different representation leads to different results and transitivity is not guaranteed) and error, raising representation_error(standard_order(Sub1, Sub2)), where the culprits are the cycles that cause the problem. So, now we get

102 ?- set_prolog_flag(incomparable, error).
true.

103 ?- X=f(X,0),Y=f(Y,1), sort([X,Y], L).
ERROR: Cyclic terms have no standard order: @(S_1,[S_1=f(S_1,0)]) and @(S_1,[S_1=f(S_1,1)])
ERROR: In:
ERROR:   [16] sort([f(...,0),...],_280)
ERROR:   [14] toplevel_call(user:user: ...) at /home/jan/src/swipl-devel/build/home/boot/toplevel.pl:1678
ERROR: 
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.

In addition, the new partial_compare/3 gives (regardless of the flag):

109 ?- X=f(X,0),Y=f(Y,1), partial_compare(Diff, X, Y).
X = f(X, 0),
Y = f(Y, 1),
Diff = incomparable(f(X, 0), f(Y, 1)).
2

Hi Jan,
Although I almost forget details of discussions in this forum on ordering rationals terms,
I have to write this based on your new amazing version of ‘term-factorized’/3.

A total, transitive order extending standard order to rational terms is mathematically sound and decidable once we drop the subterm property (T_1<T_2)\Longrightarrow f(T_1)< f(T_2).
Viewing rational terms as minimal coalgebras (e.g., via Paige–Tarjan partition refinement) yields a unique canonical DFA form that can be ordered deterministically.
The “incomparability” here arises from the C-level comparison algorithm attempting to preserve the ISO recursive descent without a coinductive product-cycle history. Only the internal C engine has direct, high-performance access to pointer cycle-breaking primitives. If the C-level comparator tracked state pairs S_1 \times S_2 during DFS descent when cycles are encountered, a stable, transitive total order could be decided directly in the engine without raising representation_error.

3

I think what I was after is different. I’m happy to accept a total ordering is possible using this canonical serialization, but that is a little too costly for standard order comparison. What we need is an ordering that is consistent with ISO ordering (too much depends on it) and cheap for already comparable terms. I had some hope we could achieve that by detecting incomparable, run term_minimal/2 on the two terms and compare. That results in consistent ordering, i.e., if A @< B, any term that is == to A (EA) and == to B (EB) has EA @< EB. Claude found counter examples for the transitivity test though, which means you cannot use it for sort/2, ordered trees, etc.

4

Out of curiosity, can you give one of these counterexamples? (not urgent)

5

Not sure. Coming days I do not have access to the machine …

6

[Total order on rational terms using term_automaton/2 and automaton_minimal/3]

Using the recent term_automaton/2 and automaton_minimal/3, I wrote rt_compare/3 to compare rational terms.

It defines a total order extending the standard order of finite terms (dropping subterm compatibility, as expected). It uses a history stack to detect visited node pairs during traversal. While it may not be optimal in efficiency, sorting a list of 10,000 random terms took about 0.58 seconds.

Please note that I have not formally verified the correctness of rt_compare/3. It is a quick implementation based on my earlier compare_with_stack/3. The complete code is attached below; I would appreciate it if anyone interested could test it.

% ?- maplist(random_term, [X, Y, Z]), predsort(rt_compare, [X,Y,Z], R).
%@ X = _S1, % where
%@     _S1 = f(44, f(_S2, _S1, _S2), g(22.82, 28, "b")),
%@     _S2 = p(f(_S2, _S1, _S2), g(22.82, 28, "b"), g(22.82, 28, "b")),
%@ Y = -5.84,
%@ Z = f(_S4, _S3, _S4), % where
%@     _S3 = p(f(_S3, _, _)),
%@     _S4 = p(f(_S4, _S3, _S4)),
%@ R = [-5.84, f(44, f(_S2, _S1, _S2), g(22.82, 28, "b")), f(_S4, _S3, _S4)] .

% ?- N = 10000, length(_Ns, N),  maplist(random_term, _Ns), time(predsort(rt_compare, _Ns, _Sorted)).
%@ % 2,529,162 inferences, 0.564 CPU in 0.584 seconds (97% CPU, 4483519 Lips)
%@ N = 10000 .

% ?- term_min_coa(a(b,c(1)), V, I).
%@ V = automaton(a(3, 2), c(4), b, 1),
%@ I = map(1, 2, 3, 4).
% ?- X=f(Y, 0), Y=f(X, 1), rt_compare(C, X, Y).
% ?- X=f(Y, X), Y=f(X, X), rt_compare(C, X, Y).


% ?- non_terminal_compound(f(a), F, N).
% ?- non_terminal_compound(1, F, N).
non_terminal_compound(X, F, N):- nonvar(X),
		functor(X, F, N, compound),
		N > 0.
%
find_pair(I, J, [[I|_]|_],[[J|_]|_]):-!.
find_pair(I, J, [_|As], [_|Bs]):- find_pair(I, J, As, Bs).

% ?- rt_pop([], [], X, Y).
% ?- rt_pop([[]], [[]], X, Y).
% ?- rt_pop([[1,2]], [[3, 4]], X, Y).
% ?- rt_pop([[1],[2], [3, 7]], [[4], [5], [6, 8]], X, Y).
%@ X = [[7]],
%@ Y = [[8]].
rt_pop([], [], [], []):-!.
rt_pop([[]|As], [[]|Bs], As0, Bs0):-!, rt_pop(As, Bs, As0, Bs0).
rt_pop([[_]|As], [[_]|Bs], As0, Bs0):-!, rt_pop(As, Bs, As0, Bs0).
rt_pop([[_|Is]|As], [[_|Js]|Bs], [Is|As], [Js|Bs]).

%
term_min_coa(X, V, I):-
	term_automaton(X, Y),
	automaton_minimal(Y, V, I).
%
random_term(R):- random_term(R, []).


% main
rt_compare(C, X, Y):-
	term_min_coa(X, U, MapX),
	arg(I, MapX, I0),
	term_min_coa(Y, V, MapY),
	arg(J, MapY, J0),
	rt_compare(C, [[I0]], [[J0]], U-V).
%
rt_compare(=, [], [], _):-!.
rt_compare(C, [[]|As], [[]|Bs], Z):-!,
	rt_pop(As, Bs, As0, Bs0),
	rt_compare(C, As0, Bs0, Z).
rt_compare(C, [[I|Is]|As], [[J|Js]|Bs], X-Y):-!,
	arg(I, X, A),
	arg(J, Y, B),
	(	non_terminal_compound(A, F, K),
		non_terminal_compound(B, G, L) ->
		compare(D, K/F, L/G),
		(	D = (=) ->
			(	find_pair(I, J, As, Bs) ->
				rt_pop([Is|As], [Js|Bs], As0, Bs0),
				rt_compare(C, As0, Bs0, X-Y)
			;	A=..[_|Ps],
				B=..[_|Qs],
				rt_compare(C, [Ps, [I|Is]|As], [Qs, [J|Js]|Bs], X-Y)
			)
		;   C = D
		)
	;	compare(D, A, B),
		(	D = (=) ->
			rt_pop([Is|As], [Js|Bs], As0, Bs0),
			rt_compare(C, As0, Bs0, X-Y)
		;   C = D
		)
	).
7

As a follow-up, assuming correctness of rt_compare/3, I implemented the product-automaton traversal in C as a foreign predicate c_rt_compare/3 assisted by Gemini.

Using a Schwartzian transform (pre-minimizing the terms once with term_automaton/2 and automaton_minimal/3 so that the O(NlogN) comparisons do not repeatedly reconstruct automata):

key_rt(Term, Key-Term) :-
    term_automaton(Term, A),
    automaton_minimal(A, Key, _).

key_compare(C, K1-_, K2-_) :-
    c_rt_compare(C, K1, K2).

rt_sort(List, Sorted) :-
    maplist(key_rt, List, Keyed),
    predsort(key_compare, Keyed, SortedKeyed),
    pairs_values(SortedKeyed, Sorted).

Benchmark

  • N = 10,000

    • Naive C (re-minimizing on every compare): 0.481 CPU sec

    • Pre-minimized C (rt_sort/2): 0.088 CPU sec

  • N = 100,000

    • Naive C: 6.324 CPU sec

    • Pre-minimized C (rt_sort/2): 1.074 CPU sec

This gives roughly a 6× speedup overall, and pure traversal in C is well over 10× faster.

If Jan were to integrate this directly into the core engine with internal representation caching, I suspect it would run vastly faster still—perhaps completely eliminating the need for incomparable exceptions.

8

Regarding sorting, as shown below, the Schwartzian transform achieves nearly a 6× speedup. Since there was an error in the code from my previous post, I am posting the corrected version.

term_min_coa(X, V, I) :-
    term_automaton(X, Y),
    automaton_minimal(Y, V, Map),
    arg(1, Map, I).

key_rt(Term, rt(I, U)-Term) :-
    term_min_coa(Term, U, I).

key_compare(C, K1-_, K2-_) :-
    rt_compare(C, K1, K2).

rt_sort(List, Sorted) :-
    maplist(key_rt, List, Keyed),
    predsort(key_compare, Keyed, SortedKeyed),
    pairs_values(SortedKeyed, Sorted).

EDIT 2026/10/3

Sorting 100k Rational Terms: Algorithmic Optimization vs. C Foreign Interface

(Apologies for missing the ongoing thread on efficient rational term comparison—my focus here was specifically to evaluate practical applications of Jan’s recent term_automaton/2 and automaton_minimal/3 predicates.)

Previously, I reported an overall ~6.5x speedup by introducing a C implementation for cyclic term comparison. However, breaking down the benchmarks reveals where the real gain comes from:

  1. Naive (predsort/3 with on-the-fly minimization):

    7.26s (Minimizations: O(NlogN))

  2. Prolog + Schwartzian Transform:

    2.17s (~3.35x speedup)

  3. C foreign interface + Schwartzian Transform:

    1.12s (~1.94x faster than pure Prolog ST, ~6.5x vs. naive)

Key Takeaway:

The algorithmic improvement—eliminating redundant DFA minimization via the Schwartzian Transform (O(NlogN)→O(N)) using the minimized automata—accounts for over 80% of the total time reduction. The C foreign implementation provides an additional ~2x constant-factor speedup by optimizing the state-stack traversal. Algorithmic pruning dominates low-level optimization.