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.
@InProceedings{schmidtschau_et_al:LIPIcs.RTA.2013.239, author = {Schmidt-Schau{\ss}, Manfred and Machkasova, Elena and Sabel, David}, title = {{Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {239--254}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.239}, URN = {urn:nbn:de:0030-drops-40651}, doi = {10.4230/LIPIcs.RTA.2013.239}, annote = {Keywords: lazy lambda calculus, contextual semantics, conservativity} }
Feedback for Dagstuhl Publishing