Title: Beta-Reduction as Unification
Author: A.J. Kfoury, Computer Science, Boston University
Date: July 8, 1996
Abstract:
We define a unification problem ^UP with the property that,
given a pure lambda-term M, we can derive an instance Gamma(M)
of ^UP from M such that Gamma(M) has a solution if and only if
M is beta-strongly normalizable. There is a type discipline for
pure lambda-terms that characterizes beta-strong normalization;
this is the system of intersection types (without a ``top'' type
that can be assigned to every lambda-term). In this report, we
use a lean version LAMBDA of the usual system of intersection types.
Hence, ^UP is also an appropriate unification problem to characterize
typability of lambda-terms in LAMBDA. It also follows that ^UP is
an undecidable problem, which can in turn be related to semi-unification
and second-order unification (both known to be undecidable).