We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
A linearization of the Lambda-calculus and consequences.
- Authors
Kfoury, Assaf J.
- Abstract
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'.
- Subjects
CALCULUS; MATHEMATICAL functions; MATHEMATICS; MATHEMATICAL analysis; EMBEDDINGS (Mathematics)
- Publication
Journal of Logic & Computation, 2000, Vol 10, Issue 3, p411
- ISSN
0955-792X
- Publication type
Article
- DOI
10.1093/logcom/10.3.411