Beta-Reduction As Unification
MetadataShow full item record
CitationKfoury, A.J.. "Beta-Reduction as Unification", Technical Report BUCS-1996-019, Computer Science Department, Boston University, July 8, 1996. [Available from: http://hdl.handle.net/2144/1595]
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).