Discrete Mathematics & Theoretical Computer Science (Dec 2000)

Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories

  • Alexandre Boudet

Journal volume & issue
Vol. 4, no. 1

Abstract

Read online

We present an algorithm for unification of higher-order patterns modulo simple syntactic equational theories as defined by Kirchner [14]. The algorithm by Miller [17] for pattern unification, refined by Nipkow [18] is first modified in order to behave as a first-order unification algorithm. Then the mutation rule for syntactic theories of Kirchner [13,14] is adapted to pattern E-unification. If the syntactic algorithm for a theory E terminates in the first-order case, then our algorithm will also terminate for pattern E-unification. The result is a DAG-solved form plus some equations of the form λ x.F(x) = λ x. F(x π) where x π is a permutation of x When all function symbols are decomposable these latter equations can be discarded, otherwise the compatibility of such equations with the solved form remains open.