A Linearization of the Lambda-Calculus and Consequences

摘要

We embed the standard λ-calculus, denoted A, into two larger λ-calculi, denoted A and & A. The standard notion of β-reduction for A corresponds to two new notions of reduction, βfor A and &βfor &A. A distinctive feature of our new calculus A (resp., & A) 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, β,β and &β. As a consequence, we provide an alternative framework to study the relationship between β-weak normalization and β-strong normalization, and give a new proof of the of-mentioned equivalence between β-strong normalization of standard λ-terms and typability I a system of 'intersection types'.