A variant of the problem is the "occurs check", used in theorem proving: https://en.wikipedia.org/wiki/Occurs_check Removing the occurs check reduces the cost of unifying two terms (t1, t2) from *O(size(t1) + size(t2))* to *O(min(size(t1), size(t2)))*, which is why Prolog implementations don't do the occurs check by default (but provide unify_with_occurs_check and acyclic_term predicates for when the check is needed). One use for cyclic terms is in representing grammars. Of course, the loops can be avoided by changing the representation from a graph to a BNF-style set of clauses - that is, by naming the nodes.