Higher-order critical pairs
- 10 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 342-349
- https://doi.org/10.1109/lics.1991.151658
Abstract
A subclass of lambda -terms, called patterns, which have unification properties resembling those of first-order terms, is introduced. Higher-order rewrite systems are defined to be rewrite systems over lambda -terms whose left-hand sides are patterns: this guarantees that the rewrite relation is easily computable. The notion of critical pair is generalized to higher-order rewrite systems, and the analog of the critical pair lemma is proved. The restricted nature of patterns is instrumental in obtaining these results. The critical pair lemma is applied to a number of lambda -calculi and some first-order logic formalized by higher-order rewrite systems.Keywords
This publication has 8 references indexed in Scilit:
- A logic programming language with lambda-abstraction, function variables, and simple unificationPublished by Springer Nature ,2005
- Combining algebra and higher-order typesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Rewrite SystemsPublished by Elsevier ,1990
- Higher-order unification revisited: Complete sets of transformationsJournal of Symbolic Computation, 1989
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- A unification algorithm for typed
- Simple Word Problems in Universal Algebras††The work reported in this paper was supported in part by the U.S. Office of Naval Research.Published by Elsevier ,1970
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940