Loading...
Please wait, while we are loading the content...
Higher-Order Unification via Combinators (1993)
| Content Provider | CiteSeerX |
|---|---|
| Author | Dougherty, Daniel J. |
| Abstract | We present an algorithm for unification in the simply typed lambda calculus which enumerates complete sets of unifiers using a finitely branching search space. In fact, the types of terms may contain type-variables, so that a solution may involve typesubstitution as well as term-substitution. the problem is first translated into the problem of unification with respect to extensional equality in combinatory logic, and the algorithm is defined in terms of transformations on systems of combinatory terms. These transformations are based on a new method (itself based on systems) for deciding extensional equality between typed combinatory logic terms. 1 Introduction This paper develops a new algorithm for higher-order unification. A higher-order unification problem is specified by two terms F and G of the explicitly simply typed lambda calculus LC; a solution is a substitution oe such that oeF = fij oeG. We will always assume the extensionality axiom j in this paper. In fact we tre... |
| File Format | |
| Volume Number | 114 |
| Journal | Theoretical Computer Science |
| Language | English |
| Publisher Date | 1993-01-01 |
| Access Restriction | Open |
| Subject Keyword | Higher-order Unification Extensional Equality Branching Search Space Typed Combinatory Logic Term New Method Combinatory Term Combinatory Logic New Algorithm Fij Oeg Typed Lambda Calculus Lc Typed Lambda Calculus Higher-order Unification Problem Complete Set Substitution Oe |
| Content Type | Text |
| Resource Type | Article |
