Matching with Free Function Symbols -- A Simple Extension of Matching?

Christophe Ringeissen 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Matching is a solving process which is crucial in declarative (rule-based) programming languages. In order to apply rules, one has to match the left-hand side of a rule with the term to be rewritten. In several declarative programming languages, programs involve operators that may also satisfy some structural axioms. Therefore, their evaluation mechanism must implement powerful matching algorithms working modulo equational theories. In this paper, we show the existence of an equational theory where matching is decidable (resp. finitary) but matching in presence of additional (free) operators is undecidable (resp. infinitary). The interest of this result is to easily prove the existence of a frontier between matching and matching with free operators.
Type de document :
Communication dans un congrès
Aart Middeldorp. International Conference on Rewriting Techniques and Applications - RTA'2001, 2001, Utrecht, The Netherlands, Springer-Verlag, 2051, pp.276--290, 2001, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00108076
Contributeur : Publications Loria <>
Soumis le : jeudi 19 octobre 2006 - 15:40:46
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00108076, version 1

Collections

Citation

Christophe Ringeissen. Matching with Free Function Symbols -- A Simple Extension of Matching?. Aart Middeldorp. International Conference on Rewriting Techniques and Applications - RTA'2001, 2001, Utrecht, The Netherlands, Springer-Verlag, 2051, pp.276--290, 2001, Lecture Notes in Computer Science. 〈inria-00108076〉

Partager

Métriques

Consultations de la notice

75