Lidia Sánchez-Gil
ABSTRACT
In order to prove the computational adequacy of the (operational) natural semantics for lazy evaluation with respect to a standard denotational semantics, Launchbury defines a resourced denotational semantics. This should be equivalent to the standard one when given infinite resources, but this fact cannot be so directly established, because each semantics produces values in a different domain. The values obtained by the standard semantics belong to the usual lifted function space D = [D → D]⊥, while those produced by the resourced semantics belong to [C → E] where E satisfies the equation E = [[C → E] → [C → E]]⊥ and C (the domain of resources) is a countable chain domain defined as the least solution of the domain equation C = C⊥.
We propose a way to relate functional values in the standard lifted function space to functional values in the corresponding resourced function space. We first construct the initial solution for the domain equation E = [[C → E]] → [C → E]]⊥ following Abramsky's construction of the initial solution of D = [D → D]⊥. Then we define a "similarity" relation between values in the constructed domain and values in the standard lifted function space. This relation is inspired by Abramsky's applicative bisimulation.
Finally we prove the desired equivalence between the standard denotational semantics and the resourced semantics for the lazy λ-calculus.
- S. Abramsky. Research Topics in Functional Programming, chapter The Lazy Lambda Calculus, pages 65--116. Addison-Wesley, 1990. Google Scholar
Digital Library
- S. Abramsky and C.-H. L. Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105(2): 159--267, 1993. Google ScholarDigital Library
- C. Baker-Finch, D. King, and P. W. Trinder. An operational semantics for parallel lazy evaluation. In ACM International Conference on Functional Programming (ICFP'00), pages 162--173, 2000. Google ScholarDigital Library
- H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984.Google Scholar
- G. Boudol, P. Curien, and C. Lavatelli. A semantics for lambda calculi with resources. Mathematical Structures in Computer Science, 9(4): 437--482, 1999. Google ScholarDigital Library
- C. Gunter and D. S. Scott. Semantic domains. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 633--674. Elsevier Science, 1990. Google ScholarDigital Library
- J. Launchbury. A natural semantics for lazy evaluation. In ACM Symposium on Principles of Programming Languages (POPL'93), pages 144--154. ACM Press, 1993. Google ScholarDigital Library
- A. Melton, D. A. Schmidt, and G. E. Strecker. Galois connections and computer science applications. In Category Theory and Computer Programming, pages 299--312. LNCS 240, Springer, 1986. Google ScholarDigital Library
- K. Nakata and M. Hasegawa. Small-step and big-step semantics for call-by-need. Journal of Functional Programming, 19(6): 699--722, 2009. Google ScholarDigital Library
- G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Journal of Theoretical Computer Science, 1(2): 125--159, 1975.Google ScholarCross Ref
- L. Sánchez-Gil, M. Hidalgo-Herrero, and Y. Ortega-Mallén. Trends in Functional Programming, volume 10, chapter An Operational Semantics for Distributed Lazy Evaluation, pages 65--80. Intellect, 2010.Google Scholar
- M. Schmidt-Schauǧ. Equivalence of call-by-name and call-by-need for lambda-calculi with letrec. Technical report, Institut für Informatik. J. W. Goethe Universität Frankfurt am Main, Germany, 2006.Google Scholar
- D. S. Scott. Continuous lattices. In Toposes, Algebraic Geometry and Logic, pages 97--136. LNCS 274, Springer, 1972.Google Scholar
- P. Sestoft. Deriving a lazy abstract machine. Journal of Functional Programming, 7(3): 231--264, 1997. Google ScholarDigital Library
- M. van Eekelen and M. de Mol. Reflections on Type Theory, λ-calculus, and the Mind. Essays dedicated to Henk Barendregt on the Occasion of his 60th Birthday, chapter Proving Lazy Folklore with Mixed Lazy/Strict Semantics, pages 87--101. Radboud University Nijmegen, The Netherlands, 2007.Google Scholar
Index Terms
- Relating function spaces to resourced function spaces
Recommendations
Observationally-induced Effect Monads: Upper and Lower Powerspace Constructions
Alex Simpson has suggested to use an observationally-induced approach towards modelling computational effects in denotational semantics. The principal idea is that a single observation algebra is used for defining the computational type structure. He ...
A category of compositional domain-models for separable stone spaces
In this paper we introduce SFPM, a category of SFP domains which provides very satisfactory domain-models, i.e. "partializations", of separable Stone spaces (2-Stone spaces). More specifically, SFPM is a subcategory of SFPep, closed under direct limits ...
Equilogical spaces
Mathematical foundations of programming semanticsIt is well known that one can build models of full higher-order dependent-type theory (also called the calculus of constructions) using partial equivalence relations (PERs) and assemblies over a partial combinatory algebra. But the idea of categories of ...
Comments