[Flash Report] Fast sorting & canonical deduplication for rational trees via C foreign predicate (tcoa_sort/2)

General
1

I would like to share an experimental C-based foreign predicate, tcoa_sort/2, designed to sort and deduplicate lists of terms (including rational trees/cyclic terms) up to bisimilarity on a 1,000,000-term scale.

  1. Approach Overview
    Based on term_automaton/2: Each term is converted to an automaton representation.
    No automaton_minimal/3: Explicit automaton minimization (e.g., Hopcroft-style partition refinement) is omitted.
    Bisimilarity-driven serialization:
    During serialization into binary canonical keys, the serializer frequently queries a bisimilarity checker (check_bisimilar_states/3) against ancestor nodes to detect cycles and encode back-references.
    Open question: There appears to be a clear design trade-off between “minimizing upfront then trivially serializing” versus “interleaving local bisimilarity queries on the fly during serialization.” Further discussion on this architectural choice is welcome.
  2. Benchmark (1,000,000 Random Terms)
    Comparison with SWI-Prolog’s built-in syntactic sort/2:

(iMac Intele 2020 macOS 26)

?- N = 1000000, length(_Ns, N), maplist(random_term, _Ns),
   time(tcoa_sort(_Ns, _Sorted)),
   time(sort(_Ns, _Sorted0)),
   time(tcoa_sort(_Sorted, _Sorted1)),
   length(_Sorted, L1), length(_Sorted0, L2), length(_Sorted1, C),
   writeln(L1:L2:C).
% 999,999 inferences, 5.650 CPU in 6.244 seconds (1st tcoa_sort)
% -1 inferences,      1.694 CPU in 1.701 seconds (built-in sort)
% 342,675 inferences, 3.661 CPU in 3.788 seconds (2nd tcoa_sort)
342676 : 545461 : 342676

Throughput: Runs at roughly 1/3 the speed of the built-in syntactic sort/2 (~3.3× CPU time), despite performing automaton generation and bisimilarity equivalence checking.
Deduplication power:
Built-in sort/2 (syntactic identity): 545,461 items
tcoa_sort/2 (bisimilarity equivalence): 342,676 items
Cyclic terms with identical unwinding behaviors but differing syntactic unrollings are consolidated into single equivalence classes.
Idempotence:
Running tcoa_sort/2 on the already sorted output yields L1
=C=342,676, verifying idempotence (f(f(X))=f(X)).
Current profiling aims to optimize the implementation further to reach around 1/2 the runtime of built-in sort/2.
3. Open Question: Potential Applications
This project originated as a personal exploratory experiment investigating the limits of C-Prolog interfacing and rational tree representations, without a predetermined target application.
If anyone sees concrete use cases for fast sorting and canonical deduplication of rational trees / automata (e.g., in type systems, model checking, coalgebraic logic programming, or term rewriting), or has perspectives on the on-the-fly bisimilarity-serialization trade-off, comments and insights are welcome.