Unification via Explicit Substitutions: The Case of Higher-Order Patterns

Gilles Dowek 1 Thérèse Hardin Claude Kirchner 2 Frank Pfenning
2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In [6] we have proposed a general higher-order unification method using a theory of explicit substitutions and we have proved its completeness. In this paper, we investigate the case of higher-order patterns as introduced by Miller. We show that our general algorithm specializes in a very convenient way to patterns. We also sketch an efficient implementation of the abstract algorithm and its generalization to constraint simplification, which has yielded good experimental results at the core of a higher-order constraint logic programming language.
Type de document :
Rapport
[Research Report] RR-3591, INRIA. 1998, pp.33
Liste complète des métadonnées

https://hal.inria.fr/inria-00077203
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 29 mai 2006 - 17:19:30
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : lundi 5 avril 2010 - 21:44:50

Fichiers

Identifiants

  • HAL Id : inria-00077203, version 1

Collections

Citation

Gilles Dowek, Thérèse Hardin, Claude Kirchner, Frank Pfenning. Unification via Explicit Substitutions: The Case of Higher-Order Patterns. [Research Report] RR-3591, INRIA. 1998, pp.33. 〈inria-00077203〉

Partager

Métriques

Consultations de la notice

219

Téléchargements de fichiers

142