We study beta-reduction in a linear lambda-calculus derived from Abramsky’s linear combinatory algebras. Reductions are classified depending on whether the redex is in the computationally active part of a term (“surface” reductions) or whether it is suspended within the body of a thunk (“internal” reductions). If surface reduction is considered on its own then any normalizing term is strongly normalizing. More generally, if a term can be reduced to surface normal form by a combined sequence of surface and internal reductions then every combined reduction sequence from the term contains only finitely many surface reductions. We apply these results to the operational semantics of
, a second-order linear lambda-calculus with recursion, introduced by Bierman, Pitts and Russo, for which we give simple proofs that call-by-value, call-by-name and call-by-need contextual equivalences coincide.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten