Term_factorized, term_minimal, term_automaton, automaton_minimal

General
1

I’m looking through the documentation trying to understand the following predicates:

term_factorized/3 and term_factorized/4
term_minimal/2
term_automaton/2
automaton_minimal/2 and automaton_minimal/3

But I have to be honest I don’t understand what the documentation is trying to say. I can see what e.g. term_factorized/3 does (it replaces unifying sub-terms with a variable) but I don’t know why this predicate exists, for example, what is a typical use-case?

[EDIT: I initially thought term_factorize might have something to do with factors in unification, i.e. literals in a clause that can be replaced with a variable to speed up unification but it doesn’t look like that’s the use case here since term_factorized/[2,3] replaces terms, rather than literals].

[EDIT2 Oh hang on, yep, that’s what it does. Well, it would be nice if this was made clear in the documentation! Especially for users that don’t know what factorization is in unification.]

I don’t understand anything in the documentation of the other three predicates. For example, the documentation for term_automaton/2 says

True when Automaton is the term graph of Term written out as an explicit automaton, and Term is the term its start state denotes.

but I can’t understand what kind of “automaton” the documentation means and I’m not even sure what is a “term graph”.

It would be nice if these subjects were explained in a bit more high-level detail accessible to non-experts, and it would be even nicer if the examples of use clarified how these predicates would be useful to the average Prolog programmer.

Btw I remember there was a similarly confused comment on numbervars/3 saying that the predicate makes no sense to anyone who doesn’t already know how to use it, I think. Now, I know what numbervars/3 does: it Skolemizes variables. But I agree that some of the concepts behind certain predicates in the SWI library are a bit … esoteric maybe, and it would be helpful to give pointers to those concepts for anyone looking in the library to try and find capabilities they may need.

2

The “automaton” representation represents a set of compound nodes and primitive nodes that constitute a term as an array, where the nodes are identified by their array index. This representation of a compound term allows us to find cycles and duplicates efficiently. More in general, they allow for easier reasoning about a term viewed as a graph because we make the nodes and edges explicit.

Among these, this allows for defining a canonical version of a term. That is a term that is ==/2 to the original, but has the smallest number of nodes. As the minimizer orders the node by standard order, there is only one such representation. This, for example, allows creating a hash key that is equivalent for all variants of a term. Note that these two terms have different physical (in memory) graphs, but are equal under ==/2.

X = f(X)
X = f(f(X))

The original variant_hash/2 simply walked the term, walking shared nodes as many times as they appear (so A = g(a), X = f(A,A) is processed the same as X = f(g(a),g(a))). This way we cannot deal with cycles.

Well, maybe this is all still very vague :frowning: . Possibly @kuniaki.mukai can describe the goals more clearly.

3

I am not quite sure if this adds much to the discussion, but please allow me to share a small example regarding term graphs, though it might be slightly beside the point.

Consider the rational tree x defined by the following equation:

x = f(a, g(x))

For this equation, let us consider an automaton A:

  • States: \\{x, y, z, u\\} with accepting state u

  • Alphabet: \\{f_1, f_2, g_1, a\\}

  • Transitions:

    • x \xrightarrow{f_1} y

    • x \xrightarrow{f_2} z

    • y \xrightarrow{a} u

    • z \xrightarrow{g_1} x

Here, A is simply a mechanical rewriting of the definition of x. In other words, the term is treated as a transition system—which is precisely in the spirit of a term graph.

As an aside, if my memory serves me correctly, David H. D. Warren noted in the Edinburgh Prolog manual that terms are represented internally as directed graphs.

4

This can be very useful. I am always amazed at how much is included (but kind of hidden) in SWI-Prolog. Thanks to Jan and all those that collaborated through the years.

Here is an example that optimizes calculation of arithmetic expressions:

In this case 2x + 2x = 20 with x == 5, the prolog term that represents the expression is

add(mul(num(2),var(x)),mul(num(2),var(x)))

69 ?- demo.
  - Unoptimized canonical: automaton(add(2,5),mul(3,4),num(8),var(9),mul(6,7),num(8),var(9),2,x)
    (need 9 operations)
  - Minimal canonical: automaton(add(2,2),mul(3,4),num(5),var(6),2,x)
    (need 6 operations)
add(mul(num(2),var(x)),mul(num(2),var(x))) = 20
true.

% Expression:         add(mul(num(2),var(x)),mul(num(2),var(x)))
% Original automaton: automaton(add(2,5),mul(3,4),num(8),var(9),mul(6,7),num(8),var(9),2,x)
% Minimal automaton:  automaton(add(2,2),mul(3,4),num(5),var(6),2,x)
% Minimal term:       add(mul(num(2),var(x)),mul(num(2),var(x)))
%                     ^^ looks the same but smaller in memory
% States: original 9, optimized 6 -> 3 repeated subtrees

% Example to optimize calculation of arithmetic expression
% 2x + 2x = 20
sample1( add(mul(num(2),var(x)),mul(num(2),var(x))) ).
var_value(x,5).

demo :-
   sample1(S), calculate(S,R),
   format('~w = ~w',[S,R]).

calculate(Expr, Result) :-
   % automaton is canonical expr
   term_automaton(Expr,CExpr),
   canonical_calculate("Unoptimized canonical:",CExpr,_),
   automaton_minimal(CExpr, MinCExpr),
   canonical_calculate("Optimized canonical:",MinCExpr,Result).

canonical_calculate(Msg, CExpr, R) :-
   format('  - ~w ~w~n',[Msg,CExpr]),
   functor(CExpr,automaton,Cnt),
   format('    (need ~w operations)~n',[Cnt]),
   % begin with first operation (i.e. first state)
   arg(1,CExpr,E1),
   canonical_calculate1(E1,CExpr,R).

canonical_calculate1(add(P1,P2), CExpr, R) :-
   arg(P1,CExpr,E1), arg(P2,CExpr,E2),
   canonical_calculate1(E1,CExpr,R1),
   canonical_calculate1(E2,CExpr,R2),
   R is R1 + R2.

canonical_calculate1(mul(P1,P2), CExpr, R) :-
   arg(P1,CExpr,E1), arg(P2,CExpr,E2),
   canonical_calculate1(E1,CExpr,R1),
   canonical_calculate1(E2,CExpr,R2),
   R is R1 * R2.

canonical_calculate1(num(P1), CExpr, R) :-
   arg(P1,CExpr,R).

canonical_calculate1(var(P1), CExpr, R) :-
   arg(P1,CExpr,V1),
   var_value(V1,R).
5

This is one of those things I have to try in the listener otherwise my brain can’t handle it:

80 ?- X = f(X), X = f(f(X)), X == X.
X = f(X).

That makes sense [EDIT: although it’s the kind of thing that makes functional programmers think “two way pattern matching” a.k.a. unification is dangerous madness]. So the new predicates are… a fast way to deal with cycles in terms without going into an infinite recursion? Is that right?

Thanks for that. However I squint and squint at your example and I’m still not confident I fully get it. I think the alphabet represents the arguments of the term (𝑓1,𝑓2, for the two arguments of term f/2, 𝑔_1 for the single term of g/1, and 𝑎 for the zero’th argument of constant a) and I guess the states 𝑦,𝑧,𝑢 are added automatically to complete the automaton? How is that calculated?

Based on that, I can kind of follow the transitions to walk over the term although I’m still not sure how the transitions are created. And: it’s a regular automaton? That’s a bit surprising.

I should explain that I have never tried to implement a WAM so I don’t understand the internal representation of Prolog terms. Is there a source I can read to understand this representation of terms as automata?

Thanks again!

EDIT: I wonder if term_automaton/2 could be used to implement a version of “flattening” an old ILP technique to replace first-order terms with arity one or more with literals. The motivation is to reduce Prolog to a language without functions other than constants and ensure termination.

6

Thanks for the thoughtful reply.

Regarding term graphs as automata, I must admit my explanation was informal. I have taken the correspondence between (cyclic) term graphs and deterministic automata as a kind of folklore. My own background view comes from coalgebras, though I do not have a concise, self-contained reference at hand—I hope good introductory materials can be found online.

On the other hand, I completely agree with your observation on flattening terms. The “solved forms” in Alain Colmerauer’s foundational work on rational trees, together with the coalgebraic perspective in Peter Aczel’s book Non-Well-Founded Sets, were indeed the main motivation behind my post.

7

Hi Jan

[A suggestion on term_factorized/3 for cyclic terms]

When applying term_factorized/3 to a cyclic term, the current behavior returns a bare variable as the skeleton if the root itself is part of a cycle:

?- X = f(X), term_factorized(X, Skel, Eqs).
X = f(X),
Eqs = [Skel=f(Skel)]

Here, Skel is an unbound variable, so one cannot see the top functor or the outermost shape without inspecting Eqs.

I propose an alternative design where the outermost constructor of the root node is always unfolded, and only the re-entering edges (cycles) are abstracted as variables:

?- X = f(X), my_term_factorized(X, Skel, Eqs).
Skel = f(A),
Eqs = [A = f(A)].

?- X = f(a, g(X)), my_term_factorized(X, Skel, Eqs).
Skel = f(a, g(A)),
Eqs = [A = f(a, g(A))].

?- my_term_factorized((a+b)-(a+b), Skel, Eqs).
Skel = A - A,
Eqs = [A = a+b].

Advantages:

  1. Skel immediately reveals the principal functor and arity of the term.
  2. It clearly indicates which argument position loops back to the root.

What do you think about this behavior?

Kuniaki

8

Being Inspired by your question, I asked Gemini from my own curiosity. Here is the answer.
it might be helpful also for you.

Q: What is the cycle-breaking algorithm used in pt_term_factorized/3, and what is its complexity?

A: It is a cycle-breaking O(N) traversal based on Robert Tarjan’s classical DFS framework (1972).

  1. Foundations (Tarjan’s DFS pattern): In Tarjan’s DFS, edges are classified into tree edges, back-edges, cross edges, and forward edges. By keeping a visited table (or reference counts), back-edges that create cycles can be detected in O(1) time. This guarantees that every node and edge is inspected exactly once, achieving strict O(V+E) (linear time) complexity without falling into infinite recursion.

  2. Application to Term Graphs and Rational Trees: Applying this traversal to break cyclic edges and reconstruct terms into systems of equations (solved forms) traces back to Alain Colmerauer’s work on rational trees (1982) and the term graph rewriting literature (e.g., Barendregt, Sleep).

In pt_term_factorized/3, this traversal breaks the re-entering back-edges in one pass, replaces them with sharing variables, while keeping the outermost constructor of the root node unfolded.

9

The fact that you can see the outer functor is nice, but instantiating creates X = f(f(X)) rather than X = f(X), the minimal cycle. That seems a step in the wrong direction.

10

You make a very good point. Re-instantiating Skel = f(A) with A = f(A) indeed yields f(f(A)), doubling the period and breaking the minimal cycle.

I have updated the behavior accordingly. If the root itself is part of a cycle, Root is represented directly as the sharing variable in Eqs, preserving the minimal representation:

?- X = f(X), my_term_factorized(X, Root, Eqs).
X = f(X),
Eqs = [Root = f(Root)].

?- X = f(A, X), my_term_factorized(X, Root, Eqs).
X = f(A, X),
Eqs = [Root = f(A, Root)].

For acyclic terms (including terms with free variables), it behaves as expected:

?- X = f(A, B), my_term_factorized(X, Root, Eqs).
Root = f(A, B),
Eqs = [].

?- my_term_factorized((a+b)-(a+b), Root, Eqs).
Root = A - A,
Eqs = [A = a+b].

This keeps the equations minimal while consistently handling both cyclic and acyclic terms. Thank you for the correction!

11

But this is exactly the current version, no?

103 ?- X = f(X), term_factorized(X, Root, Eqs).
X = f(X),
Eqs = [Root=f(Root)].

104 ?- X = f(A, X), term_factorized(X, Root, Eqs).
X = f(A, X),
Eqs = [Root=f(A, Root)].

105 ?- X = f(A, B), term_factorized(X, Root, Eqs).
X = Root, Root = f(A, B),
Eqs = [].

106 ?- term_factorized((a+b)-(a+b), Root, Eqs).
Root = _A-_A,
Eqs = [_A=a+b].
12

Indeed—my point was simply that I have updated my implementation to fully conform to SWI-Prolog’s canonical term_factorized/3 behavior.

Looking at edit(term_factorized), however, the current implementation does not yet seem to build on the wonderful recent library(automaton). I look forward to seeing how that might evolve!

13

?? I get this from 10.1.15:

image
image1090×666 63.3 KB

That works on the automation, but not materialized as a Prolog term. It collects the automation as a term_t array, does the minimization on that data and generates the result. That avoids some intermediate Prolog data structures to save time and memory. These low level mechanisms are used by the high level API term_automaton/2, etc.

14

Ah, I see—my apologies! I was looking at the older implementation in library(terms) and missed that term_factorized/3 is backed directly by the C-level minimization in pl-bisim.c without materializing intermediate Prolog terms.

Thank you for the clarification!

15

Thank you, those seem like the references to consult. Particularly Colmerauer’s work on rational trees that I had no idea about.