Sequential algorithms and strongly stable functions

AbstractIntuitionistic proofs and PCF programs may be interpreted as functions between domains, or as strategies on games. The two kinds of interpretation are inherently different: static vs. dynamic, extensional vs. intentional. It is thus extremely instructive to compare and to connect them. In this article, we investigate the extensional content of the sequential algorithm hierarchy [-]SDS introduced by Berry and Curien. We equip every sequential game [T]SDS of the hierarchy with a realizability relation between plays and extensions. In this way, the sequential game [T]SDS becomes a directed acyclic graph, instead of a tree. This enables to define a hypergraph [T]HC on the extensions (or terminal leaves) of the game [T]SDS. We establish that the resulting hierarchy [-]HC coincides with the strongly stable hierarchy introduced by Bucciarelli and Ehrhard. We deduce from this a game-theoretic proof of Ehrhard's collapse theorem, which states that the strongly stable hierarchy coincides with the extensional collapse of the sequential algorithm hierarchy