2026-07-22T21:03:18Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4065 2024-03-06T10:34:46Z ddc:004 open_access

Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings Schmidt-Schauß, Manfred Machkasova, Elena Sabel, David lazy lambda calculus contextual semantics conservativity 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manfred Schmidt-Schauß and Elena Machkasova and David Sabel 2013 Is Part Of LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2013.239 urn:nbn:de:0030-drops-40651 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.239 eng https://creativecommons.org/licenses/by/3.0/legalcode