Functional unification of higher-order patterns
- 1 January 1993
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The complete development of a unification algorithm for so-called higher-order patterns, a subclass of lambda -terms, is presented. The starting point is a formulation of unification by transformation, and the result a directly executable functional program. In a final development step, the result is adapted to lambda -terms in de Bruijn's (1972) notation. The algorithms work for both simply typed and untyped terms.<>Keywords
This publication has 9 references indexed in Scilit:
- Orthogonal higher-order rewrite systems are confluentPublished by Springer Nature ,2005
- A logic programming language with lambda-abstraction, function variables, and simple unificationPublished by Springer Nature ,2005
- Higher-order critical pairsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Unification and anti-unification in the calculus of constructionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Linear unification of higher-order patternsPublished by Springer Nature ,1993
- The TPS theorem proving systemPublished by Springer Nature ,1990
- Linear unificationJournal of Computer and System Sciences, 1978
- A unification algorithm for typed
- Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theoremIndagationes Mathematicae, 1972