Sequential algorithms and innocent strategies share the same execution mechanism
We want to emphasise some striking similarities between sequential algorithms and innocent strategies, say, for the simple type hierarchy as in PCF. The first one is that both formalims allow a fat and a meager version. In the world of sequential algorithms, the meager version is provided by the configurations of function spaces (or their description as forests), while the fat version is provided by the notion of abstract algorithm. Composition of "meager'' sequential algorithms is given in terms of an abstract machine, while composition of abstract algorithms is synthetic and "mathematical'' (essentially, the composition of the underlying functions and the composition in the reverse order of the computation strategies). In the world of Hyland and Ong’s innovent strategies, the meager version is provided by sets of views (in which PCF Böhm trees inject via a suitable transcription sharing the same underlying tree), while the fat version is given by the set of plays (which record all possible sequences of interactions of the strategy with its environment). Composition of "meager'' strategies is given in terms of an abstract machine, while composition of abstract algorithms is synthetic, via the slogan “parallel composition plus hiding”. What is even more striking an analogy is that the composition in the meager versions is actually performed by the same device, which I called geometric abstract machine in joint work with Herbelin on a general notion of abstract Böhm tree. This machine embodies two simple mechanisms, which I call tree interaction and pointer interaction, respectively. The first (forgetting for a moment the role of pointers) is a simple superposition of the trees of a strategy and a counterstrategy, determining a unique eecution path (choices made by one resolve choices offered by the other). The second kind of interaction makes use of pointers, The execution alternates between the composed strategies, and pointers guide towards where the next move has to be played in the other strategy. There are no pointers in sequential algorithms, but a sequential algorithm represented as a forest does induce a natural (and unique) pointer structure, making it look really like an innocent strategy. We believe that this analogy should be further studied.
Sat 6 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 18:00 | |||
16:00 30mTalk | Sequential algorithms and innocent strategies share the same execution mechanism GaLoP Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt | ||
16:30 40mTalk | A Dialectica-Like Interpretation of a Linear MSO on Infinite Words GaLoP |