Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4662164 | Annals of Pure and Applied Logic | 2010 | 17 Pages |
Abstract
We tackle the problem of preservation of totality by composition in arena games. We first explain how this problem reduces to a finiteness theorem on what we call pointer structures, similar to the parity pointer functions of Harmer, Hyland & Melliès and the interaction sequences of Coquand. We discuss how this theorem relates to normalization of linear head reduction in simply-typed λ-calculus, leading us to a semantic realizability proof à la Kleene of our theorem. We then present another proof of a more combinatorial nature. Finally, we discuss the exact class of strategies to which our theorems apply.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic