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

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

doi:10.4230/LIPIcs.RTA.2013.239

Document

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

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

Part of: Volume: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Rewriting Techniques and Applications (RTA)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2013-06-24

PDF

File

PDF

LIPIcs.RTA.2013.239.pdf

Filesize: 0.6 MB
16 pages

Document Identifiers

DOI: 10.4230/LIPIcs.RTA.2013.239
URN: urn:nbn:de:0030-drops-40651

Subject Classification

Keywords

lazy lambda calculus
contextual semantics
conservativity

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get 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

Author Details

Manfred Schmidt-Schauß

Elena Machkasova

David Sabel

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail