Paper abstract bibtex

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.

@article{ a_tcs93, author = {Daniel J.\ Dougherty}, title = {Higher-order unification via combinators}, journal = {Theoretical Computer Science}, volume = {114}, number = {2}, pages = {273--298}, day = {21}, year = {1993}, 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. }, url = {tcs93.pdf} }

Downloads: 0