= Term graph
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 <subterm>[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 <abstract syntax tree>[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.<An Efficient Unification Algorithm by Alberto Martelli and Ugo Montanari>[Section2 and implementation discussion, sharing and the acyclicity test]{ref}
Sharing changes <computer memory>[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>.
Back to article page
