Alexandre Boudet - Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories

dmtcs:270 - Discrete Mathematics & Theoretical Computer Science, January 1, 2000, Vol. 4 no. 1 - https://doi.org/10.46298/dmtcs.270
Unification of Higher-order Patterns modulo Simple Syntactic Equational TheoriesArticle

Authors: Alexandre Boudet 1

  • 1 Laboratoire de Recherche en Informatique

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.


Volume: Vol. 4 no. 1
Published on: January 1, 2000
Imported on: March 26, 2015
Keywords: Unification,Higher-order unification,[INFO.INFO-DM] Computer Science [cs]/Discrete Mathematics [cs.DM]

Consultation statistics

This page has been seen 315 times.
This article's PDF has been downloaded 226 times.