A linearization of the Lambda-calculus and consequences
Assaf J. Kfoury · Journal of Logic and Computation · 2000
We embed the standard λ-calculus, denoted ∧, into two larger λ-calculi, denoted ∧∧ and &∧∧. The standard notion of β-reduction for ∧ corresponds to two new notions of reduction, β∧ for ∧∧ and &β∧ for &∧∧. A distinctive feature of our new calculus ∧∧ (resp., &∧∧) 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 oft-mentioned equivalence between β-strong normalization of standard λ-terms and typability in a system of 'intersection types'.