RT Book, Section
T1 Relating function spaces to resourced function spaces.
A1 Sánchez Gil, Lidia
A1 Hidalgo Herrero, Mercedes
A1 Ortega Mallén, Yolanda
AB 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 standardlifted 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 initialsolution of D = [D → D]⊥. Then we define a “similarity”relation between values in the constructed domain and valuesin the standard lifted function space. This relation isinspired by Abramsky’s applicative bisimulation.Finally we prove the desired equivalence between the standard denotational semantics and the resourced semantics for the lazy λ-calculus.
PB ACM
SN 978-1-4503-0113-8
YR 2001
FD 2001
LK https://hdl.handle.net/20.500.14352/60584
UL https://hdl.handle.net/20.500.14352/60584
LA eng
NO Comunidad de Madrid
NO Ministerio de Ciencia e Innovación (MICINN)
NO Ministerio de Educación
DS Docta Complutense
RD 9 abr 2025