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

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail