Nominal unification with atom-variables. (January 2019)

• Record Type: Journal Article
• Authors: Schmidt-Schauß, Manfred; Sabel, David; Kutz, Yunus D.K.
• Is Part Of: Journal of symbolic computation. Volume 90(2018)
• Page Start: 42
• Page End: 64
• Publication Date: 2019-01
• Subjects: Program transformations -- Nominal unification -- Functional languages -- Atom-variables -- Correctness; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2018.04.003
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: The problem of nominal unification where variables are allowed for atoms, and computing a complete set of unifiers is considered. The complexity is shown to be NP-complete, while for special cases there are polynomial time algorithms. The main result is a novel algorithm to compute a complete set of unifiers which performs lazy guessing of equality or disequality of atom-variables, runs in NP time, and the collecting variant has more chances to keep the complete set of unifiers small. Applications of this algorithm are in reasoning about program transformations in higher order functional languages. We also present a variant of the unification algorithm that delays guessing and checking solvability, and produces a single most general unifier.