Game Semantics and the Geometry of Backtracking: a New Complexity Analysis of Interaction
JOURNAL OF SYMBOLIC LOGIC(2017)
摘要
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.
更多查看译文
关键词
Hyland-Ong Coquand game semantics,first-order logic,bounds,strategy interactions,cut-elimination,normalization
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络