Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories
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...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Discrete Mathematics & Theoretical Computer Science
2000-01-01
|
| Series: | Discrete Mathematics & Theoretical Computer Science |
| Subjects: | |
| Online Access: | https://dmtcs.episciences.org/270/pdf |
| _version_ | 1797270211634659328 |
|---|---|
| author | Alexandre Boudet |
| author_facet | Alexandre Boudet |
| author_sort | Alexandre Boudet |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T02:00:40Z |
| format | Article |
| id | doaj.art-7c084ce213f34370a6d8b6b591d937d9 |
| institution | Directory Open Access Journal |
| issn | 1365-8050 |
| language | English |
| last_indexed | 2024-04-25T02:00:40Z |
| publishDate | 2000-01-01 |
| publisher | Discrete Mathematics & Theoretical Computer Science |
| record_format | Article |
| series | Discrete Mathematics & Theoretical Computer Science |
| spelling | doaj.art-7c084ce213f34370a6d8b6b591d937d92024-03-07T15:02:22ZengDiscrete Mathematics & Theoretical Computer ScienceDiscrete Mathematics & Theoretical Computer Science1365-80502000-01-01Vol. 4 no. 110.46298/dmtcs.270270Unification of Higher-order Patterns modulo Simple Syntactic Equational TheoriesAlexandre Boudet0Laboratoire de Recherche en InformatiqueWe 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.https://dmtcs.episciences.org/270/pdfunificationhigher-order unification[info.info-dm] computer science [cs]/discrete mathematics [cs.dm] |
| spellingShingle | Alexandre Boudet Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories Discrete Mathematics & Theoretical Computer Science unification higher-order unification [info.info-dm] computer science [cs]/discrete mathematics [cs.dm] |
| title | Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories |
| title_full | Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories |
| title_fullStr | Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories |
| title_full_unstemmed | Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories |
| title_short | Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories |
| title_sort | unification of higher order patterns modulo simple syntactic equational theories |
| topic | unification higher-order unification [info.info-dm] computer science [cs]/discrete mathematics [cs.dm] |
| url | https://dmtcs.episciences.org/270/pdf |
| work_keys_str_mv | AT alexandreboudet unificationofhigherorderpatternsmodulosimplesyntacticequationaltheories |