Block structure vs scope extrusion: between innocence and omniscience

TL;DR

This paper uses game semantics to analyze block-structured computation, introducing block-innocent strategies and comparing it with dynamic memory allocation, revealing conditions under which they can be substituted and exploring their computational limits.

Contribution

It introduces block-innocent strategies in game semantics and characterizes call-by-value computation with block storage, enabling a comparative analysis with dynamic memory allocation.

Findings

Dynamic variable allocation can be replaced with block-allocated variables for base types.

Block-allocated storage can be replaced with purely functional computation at order two types.

Decidability is established for a fragment of call-by-value Idealized Algol with restricted memory allocation.

Abstract

We study the semantic meaning of block structure using game semantics. To that end, we introduce the notion of block-innocent strategies and characterise call-by-value computation with block-allocated storage through soundness, finite definability and universality results. This puts us in a good position to conduct a comparative study of purely functional computation, computation with block storage as well as that with dynamic memory allocation. For example, we can 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.