This module offers performs decoding, which is the task of traversing the data structure maintained by the unifier and transforming it into a data representation selected by the user (typically, some form of tree). It is parameterized by the term structure S, by the unifier U, and by the data representation O. Read-only access to the unifier's data structure suffices. Two decoding algorithms are proposed: the acyclic decoder does not tolerate cycles, and produces ordinary trees; whereas the cyclic decoder can deal with cycles, and produces trees that contain μ binders.