Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics

  • Alex Simpson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


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.


Operational Semantic Exponential Type Recursion Operator Typing Rule Reduction Sequence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abramsky, S., Haghverdi, E., Scott, P.: Geometry of interaction and linear combinatory algebras. Math. Struct. in Comp. Sci. 12, 625–665 (2002)zbMATHMathSciNetGoogle Scholar
  2. 2.
    Barber, A.: Linear Type Theories, Semantics and Action Calculi. PhD thesis, Department of Computer Science, University of Edinburgh (1997)Google Scholar
  3. 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
  4. 4.
    Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Inf. and Comp. 124, 103–112 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Launchbury, J.: A natural semantics for lazy evaluation. In: Proc. 20th POPL, pp. 144–154 (1993)Google Scholar
  6. 6.
    Mason, I.A., Talcott, C.L.: Equivalence in functional languages with effects. J. Functional Programming 1, 287–327 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    O’Hearn, P.W., Reynolds, J.C.: From Algol to polymorphic linear lambdacalculus. Journal of the ACM 47, 167–223 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Pitts, A.M.: Parametric polymorphism and operational equivalence. Math. Struct. in Comp. Sci. 10, 321–359 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theor. Comp. Sci. 1, 125–159 (1975)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Plotkin, G.D.: Type theory and recursion. Invited talk at 8th Symposium on Logic in Comp. Sci. (1993)Google Scholar
  11. 11.
    Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Information Processing 1983, pp. 513–523. North Holland, Amsterdam (1983)Google Scholar
  12. 12.
    Seaman, J., Iyer, S.P.: An operational semantics of sharing in lazy evaluation. Science of Computer Programming 27, 289–322 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Setstoft, P.: Deriving a lazy abstract machine. J. Functional Programming 7, 23–248 (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Alex Simpson
    • 1
  1. 1.LFCS, School of InformaticsUniversity of EdinburghUK

Personalised recommendations