Paper Info
Title
Sequential algorithms and strongly stable functions
Abstract
Intuitionistic 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 gametheoretic proof of Ehrhard's collapse theorem, which states that the strongly stable hierarchy coincides with the extensional collapse of the sequential algorithm hierarchy.
Year
DOI
Venue
2005
10.1016/j.tcs.2005.05.015
Theor. Comput. Sci.
Keywords
DocType
Volume
Strongly stable functions,Intuitionistic proof,stable hierarchy,sequential game,Sequential algorithms,Linear logic,sequential algorithm hierarchy,PCF program,extensional collapse,Game semantics,acyclic graph,resulting hierarchy,extensional content,collapse theorem,stable function,Extensional collapse
Journal
343
Issue
ISSN
Citations 
1-2
Theoretical Computer Science
12
PageRank 
References 
Authors
0.77
19
1
Name
Order
Citations
PageRank
Paul-andré Melliès139230.70