Rational tree

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]