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.
Type de document :
Article dans une revue
Discrete Mathematics and Theoretical Computer Science, DMTCS, 2000, 4 (1), pp.11-30
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00958942
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : jeudi 13 mars 2014 - 16:49:31
Dernière modification le : mardi 24 avril 2018 - 13:55:39
Document(s) archivé(s) le : vendredi 13 juin 2014 - 12:02:30

Fichier

dm040102.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00958942, version 1

Collections

Citation

Alexandre Boudet. Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories. Discrete Mathematics and Theoretical Computer Science, DMTCS, 2000, 4 (1), pp.11-30. 〈hal-00958942〉

Partager

Métriques

Consultations de la notice

118

Téléchargements de fichiers

169