# Reduction in a Linear Lambda-calculus with Applications to Operational Semantics

## Alex Simpson, University of Edinburgh

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 Lily, 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.