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 λ-calculus. Because of the operational content of game semantics, the bounds presented here also apply to head linear reduction on λ-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 analysed independently of game semantics or λ-calculus.
Chapter PDF
Similar content being viewed by others
References
Abramsky, S., McCusker, G.: Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions (1997)
Abramsky, S., McCusker, G.: Call-by-value games. In: Nielsen, M., Thomas, W. (eds.) CSL 1997. LNCS, vol. 1414, pp. 1–17. Springer, Heidelberg (1998)
Beckmann, A.: Exact bounds for lengths of reductions in typed λ-calculus. Journal of Symbolic Logic 66(3), 1277–1285 (2001)
Blum, W.: Thesis fascicle: Local computation of β-reduction. PhD thesis, University of Oxford (2008)
Clairambault, P.: Logique et Interaction: une Étude Sémantique de la Totalité. PhD thesis, Université Paris Diderot (2010)
Clairambault, P., Harmer, R.: Totality in arena games. Annals of Pure and Applied Logic (2009)
Coquand, T.: A semantics of evidence for classical arithmetic. Journal of Symbolic Logic 60(1), 325–337 (1995)
Danos, V., Herbelin, H., Regnier, L.: Game semantics and abstract machines. In: 11th IEEE Symposium on Logic in Computer Science, pp. 394–405 (1996)
Danos, V., Regnier, L.: How abstract machines implement head linear reduction (2003) (unpublished)
de Bruijn, N.G.: Generalizing Automath by means of a lambda-typed lambda calculus. Mathematical Logic and Theoretical Computer Science 106, 71–92 (1987)
Girard, J.-Y.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998)
Greenland, W.: Game semantics for region analysis. PhD thesis, University of Oxford (2004)
Harmer, R.: Innocent game semantics. Lecture notes (2004-2007)
Harmer, R., Hyland, M., Melliès, P.-A.: Categorical combinatorics for innocent strategies. In: IEEE Symposium on Logic in Computer Science, pp. 379–388 (2007)
Harmer, R., McCusker, G.: A fully abstract game semantics for finite nondeterminism. In: IEEE Symposium on Logic in Computer Science, pp. 422–430 (1999)
Hyland, M., Luke Ong, C.-H.: On full abstraction for PCF: I, II and III. Information and Computation 163(2), 285–408 (2000)
Krivine, J.-L.: Un interpréteur du λ-calcul (1985) (unpublished)
Dal Lago, U., Laurent, O.: Quantitative game semantics for linear logic. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 230–245. Springer, Heidelberg (2008)
Laird, J.: Full abstraction for functional languages with control. In: IEEE Symposium on Logic in Computer Science, pp. 58–67 (1997)
Laird, J.: A game semantics of the asynchronous π-calculus. In: Jayaraman, K., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 51–65. Springer, Heidelberg (2005)
Mascari, G., Pedicini, M.: Head linear reduction and pure proof net extraction. Theoretical Computer Science 135(1), 111–137 (1994)
McCusker, G.: Games and Full Abstraction for FPC. Information and Computation 160(1-2), 1–61 (2000)
Nakajima, R.: Infinite normal forms for the λ-calculus. In: λ-Calculus and Computer Science Theory, pp. 62–82 (1975)
Schwichtenberg, H.: Complexity of normalization in the pure typed lambda-calculus. Studies in Logic and the Foundations of Mathematics 110, 453–457 (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clairambault, P. (2011). Estimation of the Length of Interactions in Arena Game Semantics. In: Hofmann, M. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2011. Lecture Notes in Computer Science, vol 6604. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19805-2_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-19805-2_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19804-5
Online ISBN: 978-3-642-19805-2
eBook Packages: Computer ScienceComputer Science (R0)