Estimation of the Length of Interactions in Arena Game Semantics

  • Pierre Clairambault
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6604)


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.


  1. 1.
    Abramsky, S., McCusker, G.: Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions (1997)CrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Beckmann, A.: Exact bounds for lengths of reductions in typed λ-calculus. Journal of Symbolic Logic 66(3), 1277–1285 (2001)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Blum, W.: Thesis fascicle: Local computation of β-reduction. PhD thesis, University of Oxford (2008)Google Scholar
  5. 5.
    Clairambault, P.: Logique et Interaction: une Étude Sémantique de la Totalité. PhD thesis, Université Paris Diderot (2010)Google Scholar
  6. 6.
    Clairambault, P., Harmer, R.: Totality in arena games. Annals of Pure and Applied Logic (2009)Google Scholar
  7. 7.
    Coquand, T.: A semantics of evidence for classical arithmetic. Journal of Symbolic Logic 60(1), 325–337 (1995)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Danos, V., Herbelin, H., Regnier, L.: Game semantics and abstract machines. In: 11th IEEE Symposium on Logic in Computer Science, pp. 394–405 (1996)Google Scholar
  9. 9.
    Danos, V., Regnier, L.: How abstract machines implement head linear reduction (2003) (unpublished) Google Scholar
  10. 10.
    de Bruijn, N.G.: Generalizing Automath by means of a lambda-typed lambda calculus. Mathematical Logic and Theoretical Computer Science 106, 71–92 (1987)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Girard, J.-Y.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Greenland, W.: Game semantics for region analysis. PhD thesis, University of Oxford (2004)Google Scholar
  13. 13.
    Harmer, R.: Innocent game semantics. Lecture notes (2004-2007)Google Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    Harmer, R., McCusker, G.: A fully abstract game semantics for finite nondeterminism. In: IEEE Symposium on Logic in Computer Science, pp. 422–430 (1999)Google Scholar
  16. 16.
    Hyland, M., Luke Ong, C.-H.: On full abstraction for PCF: I, II and III. Information and Computation 163(2), 285–408 (2000)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Krivine, J.-L.: Un interpréteur du λ-calcul (1985) (unpublished) Google Scholar
  18. 18.
    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)CrossRefGoogle Scholar
  19. 19.
    Laird, J.: Full abstraction for functional languages with control. In: IEEE Symposium on Logic in Computer Science, pp. 58–67 (1997)Google Scholar
  20. 20.
    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)CrossRefGoogle Scholar
  21. 21.
    Mascari, G., Pedicini, M.: Head linear reduction and pure proof net extraction. Theoretical Computer Science 135(1), 111–137 (1994)MathSciNetCrossRefGoogle Scholar
  22. 22.
    McCusker, G.: Games and Full Abstraction for FPC. Information and Computation 160(1-2), 1–61 (2000)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Nakajima, R.: Infinite normal forms for the λ-calculus. In: λ-Calculus and Computer Science Theory, pp. 62–82 (1975)Google Scholar
  24. 24.
    Schwichtenberg, H.: Complexity of normalization in the pure typed lambda-calculus. Studies in Logic and the Foundations of Mathematics 110, 453–457 (1982)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Pierre Clairambault
    • 1
  1. 1.University of BathUK

Personalised recommendations