Game Semantics and the Geometry of Backtracking: a New Complexity Analysis of Interaction

TL;DR

This paper introduces a new complexity analysis for game semantics, providing bounds on interaction lengths and exponential towers, which improves previous estimates significantly.

Contribution

It develops a novel method to bound interaction lengths in game semantics, leading to tighter complexity bounds for various dialogical processes.

Findings

New bounds on the length of interactions between strategies

Precise measurement of exponential towers in complexity

Improved estimates over previous models

Abstract

We present abstract complexity results about Coquand and Hyland-Ong game semantics, that will lead to new bounds on the length of first-order cut-elimination, normalization, interaction between expansion trees and any other dialogical process game semantics can model and apply to. In particular, we provide a novel method to bound the length of interactions between visible strategies and to measure precisely the tower of exponentials defining the worst-case complexity. Our study improves the old estimates on average by several exponentials.