About the Paterson-Wegman linear unification algorithm

摘要

The Paterson-Wegman unification algorithm is investigated. An error is removed. The proper input format is clarified. A pre-processor is described that associates with each node a list of parent nodes, as required by the core algorithm. A post-processor is described that transforms an ordered substitution, produced by the core algorithm, into a regular substitution, making use of structure sharing when possible. The combination of pre-processor, core algorithm, and post-processor is still a linear algorithm (with respect to the sum of nodes and edges in the input graph).