Positional Injectivity for Innocent Strategies

TL;DR

This paper explores the concept of positionality in innocent strategies within pointer games, demonstrating that while innocence does not imply positionality, finite strategies are uniquely determined by their positions, with some limitations.

Contribution

It extends the understanding of positionality from asynchronous games to pointer games, showing finite innocent strategies are positionally injective, but this does not hold universally.

Findings

Finite innocent strategies are positionally injective.

Counterexample shows non-injective behavior when finiteness and totality are lifted.

Strategies with the same positions share the same P-views of maximal length.

Abstract

In asynchronous games, Melli{\`e}s proved that innocent strategies are positional: their behaviour only depends on the position, not the temporal order used to reach it. This insightful result shaped our understanding of the link between dynamic (i.e. game) and static (i.e. relational) semantics. In this paper, we investigate the positionality of innocent strategies in the traditional setting of Hyland-Ong-Nickau-Coquand pointer games. We show that though innocent strategies are not positional, total finite innocent strategies still enjoy a key consequence of positionality, namely positional injectivity: they are entirely determined by their positions. Unfortunately, this does not hold in general: we show a counterexample if finiteness and totality are lifted. For finite partial strategies we leave the problem open; we show however the partial result that two strategies with the same positions must have the same P-views of maximal length.