Beta-reduction as unification
Assaf J. Kfoury · Banach Center Publications · 1999
We define a new unification problem, which we call β-unification and which can be used to characterize the β-strong normalization of terms in the λ-calculus. We prove the undecidability of β-unification, its connection with the system of intersection type