Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics
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.
KeywordsOperational Semantic Exponential Type Recursion Operator Typing Rule Reduction Sequence
Unable to display preview. Download preview PDF.
- 2.Barber, A.: Linear Type Theories, Semantics and Action Calculi. PhD thesis, Department of Computer Science, University of Edinburgh (1997)Google Scholar
- 3.Bierman, G.M., Pitts, A.M., Russo, C.V.: Operational properties of Lily, a polymorphic linear lambda calculus with recursion. Elect. Notes in Theor. Comp. Sci. 41 (2000)Google Scholar
- 5.Launchbury, J.: A natural semantics for lazy evaluation. In: Proc. 20th POPL, pp. 144–154 (1993)Google Scholar
- 10.Plotkin, G.D.: Type theory and recursion. Invited talk at 8th Symposium on Logic in Comp. Sci. (1993)Google Scholar
- 11.Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Information Processing 1983, pp. 513–523. North Holland, Amsterdam (1983)Google Scholar
- 13.Setstoft, P.: Deriving a lazy abstract machine. J. Functional Programming 7, 23–248 (1999)Google Scholar