Game semantics approach to higher-order complexity

Hugo Férée

Standard complexity theory provides a well-known notion of complexity for first-order functions (i.e. functions over integers or binary words). A lesser known but well understood notion of complexity for second-order functions (i.e. functions over first-order functions) also exists, as well as a class of feasible functions analogue to the standard class of polynomial time computable (first-order) functions. However, no satisfactory notion of complexity at higher types has been given yet.

We propose here a definition of complexity for higher order functions (more precisely, PCF functionals) based on game semantics, i.e. where functions are represented by strategies and the application operation of corresponds to the confrontation of such strategies in a game. In particular, we define a complexity class which coincides with the usual notions of polynomial time complexity at first and second order, and satisfies several properties that we can expect from a higher order class of feasible functions.