Article ID Journal Published Year Pages File Type
4662164 Annals of Pure and Applied Logic 2010 17 Pages PDF
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