Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings

Authors Manfred Schmidt-Schauß, Elena Machkasova, David Sabel

Thumbnail PDF


  • Filesize: 0.6 MB
  • 16 pages

Document Identifiers

Author Details

Manfred Schmidt-Schauß
Elena Machkasova
David Sabel

Cite AsGet BibTex

Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel. Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 239-254, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Our motivation is the question whether the lazy lambda calculus, a pure lambda calculus with the leftmost outermost rewriting strategy, considered under observational semantics, or extensions thereof, are an adequate model for semantic equivalences in real-world purely functional programming languages, in particular for a pure core language of Haskell. We explore several extensions of the lazy lambda calculus: addition of a seq-operator, addition of data constructors and case-expressions, and their combination, focusing on conservativity of these extensions. In addition to untyped calculi, we study their monomorphically and polymorphically typed versions. For most of the extensions we obtain non-conservativity which we prove by providing counterexamples. However, we prove conservativity of the extension by data constructors and case in the monomorphically typed scenario.
  • lazy lambda calculus
  • contextual semantics
  • conservativity


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads