Observational Equivalence and a New Operational Semantics for Lazy Evaluation with Selective Strictness

Haeri, Seyed Hossein
(2010) International Conference on Theoretical and Mathematical Foundations of Computer Science (TMFCS-10) — Location: Orlando, Florida, USA (12.July.2010)

Files

tmfcs2010.pdf
  • Open Access
  • Adobe PDF
  • 267.15 KB
Download

Details

Authors
  • Haeri, Seyed HosseinUCLouvain
    Author
Abstract
For the purpose of adding to the time or space efficiency, selective enforcement of strictness is commonly practiced in today's lazy programming. Although it plays a key role in equational reasoning about programs, many few studies have considered observational equivalence between lazy programs in presence of selective strictness (OELPPSS). Gabbay et al. were first to consider OELPPSS and Haeri later completed their work. Both Gabbay et al. and Haeri build on a variation of the operational semantics of van Eekelen and de Mol which, in return, extends Launchbury's semantics for lazy evaluation to selective strictness. Gabbay et al. and Haeri choose to manipulate the operational semantics of van Eekelen and de Mol to prevent increase in heap expressiveness upon expression evaluation. This improvement helped them to prove their desired observational equivalences using a novel proof technique called: induction on the number of manipulated bindings (INMB). They used INMB to prove a handful of interesting results including a couple of observational equivalences. However, their operational semantics suffers from restrictions in expressiveness. In this paper, we present yet another variation of van Eekelen and de Mol. Our operational semantics is as expressive as that of van Eekelen and de Mol. We prove that INMB is valid for our operational semantics too. Therefore, all the interesting results of Gabbay et al. and Haeri including their observational equivalences remain valid for our system as well. This is whilst, like that of Gabbay et al. and Haeri, our operational semantics avoids increase in heap expressiveness upon expression evaluation.
Affiliations
  • MuSemantikLtd

Citations

  • APA
  • Chicago
  • FWB

Haeri, S. H. (2010). Observational Equivalence and a New Operational Semantics for Lazy Evaluation with Selective Strictness. Proceedings of International Conference on Theoretical and Mathematical Foundations of Computer Science 2010 (TMFCS-10). Published. International Conference on Theoretical and Mathematical Foundations of Computer Science (TMFCS-10), Orlando, Florida, USA. https://hdl.handle.net/2078.5/220884