Journal of Logic and Computation, Volume 10, Issue 3, pp. 411-436: Abstract.
A linearization of the Lambda-calculus and consequences
Department of Computer Science, Boston University, 111 Cummington Street, Boston, MA 02215, USA, E-mail: email@example.com
We embed the standard [lgr]-calculus, denoted [and], into two larger [lgr]-calculi, denoted [and][and] and &[and][and]. The standard notion of [bgr]-reduction for [and] corresponds to two new notions of reduction, [bgr][and] for [and][and] and &[bgr][and] for &[and][and]. A distinctive feature of our new calculus [and][and] (resp., &[and][and]) is that, in every function application, an argument is used at most once (resp. exactly once) in the body of the function). We establish various connections between the three notions of reduction, [bgr], [bgr][and] and &[bgr][and]. As a consequence, we provide an alternative framework to study the relationship between [bgr]-weak normalization and [bgr]-strong normalization, and give a new proof of the oft-mentioned equivalence between [bgr]-strong normalization of standard [lgr]-terms and typability in a system of 'intersection types'.
Keywords: weak normalization, strong normalization, intersection types, type inference, generalization of beta reduction