Simulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq

This paper shows equivalence of several versions of applicative similarityand contextual approximation, and hence also of applicative bisimilarity andcontextual equivalence, in LR, the deterministic call-by-need lambda calculuswith letrec extended by data constructors, case-expressions and Haskell'sseq-operator. LR models an untyped version of the core language of Haskell. Theuse of bisimilarities simplifies equivalence proofs in calculi and opens a wayfor more convenient correctness proofs for program transformations. The proofis 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 lattercalculus equivalence of our similarities and contextual approximation can beshown by Howe's method. Similarity is transferred back to LR on the basis of aninductively defined similarity. The translation from the call-by-need letreccalculus into the extended call-by-name lambda calculus is the composition oftwo translations. The first translation replaces the call-by-need strategy by acall-by-name strategy and its correctness is shown by exploiting infinite treeswhich emerge by unfolding the letrec expressions. The second translationencodes letrec-expressions by using multi-fixpoint combinators and itscorrectness is shown syntactically by comparing reductions of both calculi. Afurther result of this paper is an isomorphism between the mentioned calculi,which is also an identity on letrec-free expressions.Comment: 50 pages, 11 figure