Block structure vs. scope extrusion: Between innocence and omniscience

Abstract

We study the semantic meaning of block structure using game semantics and introduce the notion of block-innocent strategies, which turns out to characterise call-by-value computation with block-allocated storage through soundness, finitary definability and universality results. This puts us in a good position to conduct a comparative study of purely functional computation, computation with block storage and dynamic memory allocation respectively. For example, we show that dynamic variable allocation can be replaced with block-allocated variables exactly when the term involved (open or closed) is of base type and that block-allocated storage can be replaced with purely functional computation when types of order two are involved. To illustrate the restrictive nature of block structure further, we prove a decidability result for a finitary fragment of call-by-value Idealized Algol for which it is known that allowing for dynamic memory allocation leads to undecidability. © 2010 Springer-Verlag.