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 has five occurrences in its ordinary syntax tree: one , two and two . A shared term graph can use only three nodes, with the two argument graph edges of pointing to the same node. Sharing a variable node is also useful: identifications made by a unification algorithm can be represented once and followed from every occurrence.[ref]
An Efficient Unification Algorithm by Alberto Martelli and Ugo Montanari. Section2 and implementation discussion, sharing and the acyclicity test
Sharing changes storage, not the meaning of an acyclic finite first-order term. A cycle is different. A node labelled whose argument points back to itself unfolds to an infinite rational tree; it cannot represent a finite solution to . An implementation must therefore state whether it supports infinite rational trees or enforces the finite-term occurs check.
