Totality in arena games |
| |
Authors: | Pierre Clairambault |
| |
Affiliation: | PPS, CNRS & Université Paris Diderot-Paris 7, Case 7014, 75205 Paris Cedex 13, France |
| |
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. |
| |
Keywords: | 03B70 68Q55 03B40 |
本文献已被 ScienceDirect 等数据库收录! |
|