The notion of list structure is discussed, and a new construct is introduced into LISP which permits the computation of list structures containing cycles without recourse to operations which alter existing structures. It is shown that list structures can be used to represent both finite and “rational” infinite terms. Substitutions (generalized for a term algebra which includes infinite terms) are discussed, “tables” are introduced as an abstract data type, and two methods of representing substitutions by tables, together with their interrelation, are considered. Concise programs are given for a succession of forms of Robinson’s unification algorithm, including one which operates in almost linear time, and for the application of substitutions to terms.
Morris, F. Lockwood, "ON LIST STRUCTURES AND THEIR USE IN THE PROGRAMMING OF UNIFICATION" (1978). Electrical Engineering and Computer Science Technical Reports. Paper 40.