Manfred Schmidt-Schauß ; David Sabel ; Elena Machkasova - Simulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq

lmcs:930 - Logical Methods in Computer Science, March 16, 2015, Volume 11, Issue 1 - https://doi.org/10.2168/LMCS-11(1:7)2015
Simulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and SeqArticle

Authors: Manfred Schmidt-Schauß ; David Sabel ORCID; Elena Machkasova

    This paper shows equivalence of several versions of applicative similarity and contextual approximation, and hence also of applicative bisimilarity and contextual equivalence, in LR, the deterministic call-by-need lambda calculus with letrec extended by data constructors, case-expressions and Haskell's seq-operator. LR models an untyped version of the core language of Haskell. The use of bisimilarities simplifies equivalence proofs in calculi and opens a way for more convenient correctness proofs for program transformations. The proof is by a fully abstract and surjective transfer into a call-by-name calculus, which is an extension of Abramsky's lazy lambda calculus. In the latter calculus equivalence of our similarities and contextual approximation can be shown by Howe's method. Similarity is transferred back to LR on the basis of an inductively defined similarity. The translation from the call-by-need letrec calculus into the extended call-by-name lambda calculus is the composition of two translations. The first translation replaces the call-by-need strategy by a call-by-name strategy and its correctness is shown by exploiting infinite trees which emerge by unfolding the letrec expressions. The second translation encodes letrec-expressions by using multi-fixpoint combinators and its correctness is shown syntactically by comparing reductions of both calculi. A further result of this paper is an isomorphism between the mentioned calculi, which is also an identity on letrec-free expressions.


    Volume: Volume 11, Issue 1
    Published on: March 16, 2015
    Imported on: October 26, 2011
    Keywords: Computer Science - Logic in Computer Science

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1005 times.
    This article's PDF has been downloaded 386 times.