Game Semantics and the Geometry of Backtracking: a New Complexity Analysis of Interaction
Logic
2016-08-12 v3 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.1511.06260,
title = {Game Semantics and the Geometry of Backtracking: a New Complexity Analysis of Interaction},
author = {Federico Aschieri},
journal= {arXiv preprint arXiv:1511.06260},
year = {2016}
}
Comments
Final version