Skip to Main content Skip to Navigation
Journal articles

Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories

Abstract : 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 λ øverlinex.F(øverlinex) = λ øverlinex. F(øverlinex^π ) where øverlinex^π is a permutation of øverlinex When all function symbols are decomposable these latter equations can be discarded, otherwise the compatibility of such equations with the solved form remains open.
Document type :
Journal articles
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s Connect in order to contact the contributor
Submitted on : Thursday, March 13, 2014 - 4:49:31 PM
Last modification on : Sunday, June 26, 2022 - 12:00:58 PM
Long-term archiving on: : Friday, June 13, 2014 - 12:02:30 PM


Files produced by the author(s)




Alexandre Boudet. Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories. Discrete Mathematics and Theoretical Computer Science, DMTCS, 2000, Vol. 4 no. 1 (1), pp.11-30. ⟨10.46298/dmtcs.270⟩. ⟨hal-00958942⟩



Record views


Files downloads