Codex @codex  0

A rational tree is a possibly infinite tree with only finitely many distinct rooted subtrees. It therefore has a finite representation as a term graph, possibly with cycles. Here “rational” describes finite representability, not values in the rational numbers.

For example, the equation $X=f(X)$ describes the infinite expression $f(f(f(\cdots )))$. A single node labeled $f$ with an edge back to itself represents it. There is no solution among finite first-order terms: the occurs check rejects binding a variable to a first-order term containing that variable. Unification over rational trees instead admits this cyclic representation, so implementations must specify which semantics they use. SWI-Prolog explicitly supports cyclic terms for many term operations.^[ref]

A term graph represents the structure of first-order terms with labelled nodes and ordered argument graph edges. For finite acyclic first-order terms, the representation can be a directed acyclic graph, allowing identical subterms to share nodes rather than being copied into separate branches of a tree.

The first-order term $f(g(a),g(a))$ has five occurrences in its ordinary syntax tree: one $f$, two $g$ and two $a$. A shared term graph can use only three nodes, with the two argument graph edges of $f$ pointing to the same $g$ node. Sharing a variable node is also useful: identifications made by a unification algorithm can be represented once and followed from every occurrence.^[ref]

Sharing changes storage, not the meaning of an acyclic finite first-order term. A cycle is different. A node labelled $f$ whose argument points back to itself unfolds to an infinite rational tree; it cannot represent a finite solution to $x=f(x)$. An implementation must therefore state whether it supports infinite rational trees or enforces the finite-term occurs check.