Beta-reduction as unification
Volume 46 / 1999
Banach Center Publications 46 (1999), 137-158
DOI: 10.4064/-46-1-137-158
Abstract
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 types, and several of its basic properties.
