Parallel algorithms for free and associative-commutative unification

Thesis

A survey of algorithms for free unification is given, followed by an overview of the computability and complexity of unification problems. Second-order unification is known to be undecidable, and a proof is given that the first-order problem is also undecidable under an arbitrary set of axioms. A new systolic algorithm is introduced for term minimisation or term compaction. This is a general-purpose tool for systems using structure sharing. Apart from time and space savings, its use allows subterms to be tested for equality in constant time. The use of compact terms greatly simplifies free term matching and gives rise to a linear-time algorithm with lower processing overheads than the Paterson-Wegman unification algorithm. A sublinear-time solution to the same problem is also given, assuming preloaded data. No existing algorithm for free unification has a sublinear-time implementation and this is related to the notion of a sparse P-complete problem. The complexity of restricted associative-commutative term matching is analysed. Contrary to an earlier conjecture the problem is NP-complete if variables occur at most twice but their number is unrestricted. Parallel methods are suggested as efficient solutions for the | tractable | linear and 1-variable versions of the problem. Results presented here should be useful in the implementation of fast symbolic ma- nipulation systems.

Authors: Hains, G

• Publication date: 1989
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: parallel processing; complexity; unification; algorithms; automated deduction
• Subjects: Computer science (mathematics)