LIPIcs.RTA.2013.239.pdf
- Filesize: 0.6 MB
- 16 pages
Document
Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings
Authors
-
Part of:
Volume:
24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2013-06-24
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)
https://doi.org/10.4230/LIPIcs.RTA.2013.239
https://doi.org/10.4230/LIPIcs.RTA.2013.239
Abstract
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.
Keywords
- lazy lambda calculus
- contextual semantics
- conservativity
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads