Estimation of the length of interactions in arena game semantics
Pierre Clairambault

TL;DR
This paper estimates the maximum length of interactions in arena game semantics, providing bounds that also apply to lambda-calculus reduction and program execution, including effects like non-determinism.
Contribution
It introduces a combinatorial rewriting rule on trees that bounds interaction lengths, bridging game semantics with operational and computational models.
Findings
Bounds on interaction lengths in game semantics
Applicability to lambda-calculus reduction
Rewriting rule on trees for analysis
Abstract
We estimate the maximal length of interactions between strategies in HO/N game semantics, in the spirit of the work by Schwichtenberg and Beckmann for the length of reduction in simply typed lambdacalculus. Because of the operational content of game semantics, the bounds presented here also apply to head linear reduction on lambda-terms and to the execution of programs by abstract machines (PAM/KAM), including in presence of computational effects such as non-determinism or ground type references. The proof proceeds by extracting from the games model a combinatorial rewriting rule on trees of natural numbers, which can then be analyzed independently of game semantics or lambda-calculus.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
