Discrete Mathematics & Theoretical Computer Science
Volume 4 n° 1 (2000), pp. 11-30
| author: | Alexandre Boudet |
|---|---|
| title: | Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories |
| keywords: | Unification, Higher-order unification |
| 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 Eunification. If the syntactic algorithm for a theory E terminates in the first-order case, then our algorithm will also terminate for pattern Eunification. The result is a DAG-solved form plus some equations of the form lambda x.F(x) = lambda x. F(x^{pi}) where x^{\pi} 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. |
| reference: | Alexandre Boudet (2000), Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories , Discrete Mathematics and Theoretical Computer Science 4, pp. 11-30 |
| ps.gz-source: | dm040102.ps.gz (52 K) |
| ps-source: | dm040102.ps (149 K) |
| pdf-source: | dm040102.pdf (184 K) |
The first source gives you the `gzipped' PostScript, the second the plain PostScript and the third the format for the Adobe accrobat reader. Depending on the installation of your web browser, at least one of these should (after some amount of time) pop up a window for you that shows the full article. If this is not the case, you should contact your system administrator to install your browser correctly.
Automatically produced on Tue Apr 25 17:26:58 CEST 2000 by novelli