= Rational tree
A <rational tree> is a possibly infinite <tree (graph theory)> 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.<Rational trees in the SWI-Prolog manual>[§2.16, cyclic-term support and example A = f(A)]{ref}
Back to article page
