Strong functors and interleaving fixpoints in game semantics

Pierre Clairambault

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2013)

  • Volume: 47, Issue: 1, page 25-68
  • ISSN: 0988-3754

Abstract

top
We describe a sequent calculus μLJ with primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of Gödel’s system T. We introduce the notion of a μ-closed category, relying on a uniform interpretation of open μLJ formulas as strong functors. We show that any μ-closed category is a sound model for μLJ. We then turn to the construction of a concrete μ-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients: the construction of a general class of strong functors called open functors acting on the category of games and strategies, the solution of recursive arena equations by exploiting cycles in arenas, and the adaptation of the winning conditions of parity games to build initial algebras and terminal coalgebras for many open functors. We also prove a weak completeness result for this model, yielding a normalisation proof for μLJ.

How to cite

top

Clairambault, Pierre. "Strong functors and interleaving fixpoints in game semantics." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 47.1 (2013): 25-68. <http://eudml.org/doc/273044>.

@article{Clairambault2013,
abstract = {We describe a sequent calculus μLJ with primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of Gödel’s system T. We introduce the notion of a μ-closed category, relying on a uniform interpretation of open μLJ formulas as strong functors. We show that any μ-closed category is a sound model for μLJ. We then turn to the construction of a concrete μ-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients: the construction of a general class of strong functors called open functors acting on the category of games and strategies, the solution of recursive arena equations by exploiting cycles in arenas, and the adaptation of the winning conditions of parity games to build initial algebras and terminal coalgebras for many open functors. We also prove a weak completeness result for this model, yielding a normalisation proof for μLJ.},
author = {Clairambault, Pierre},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {game semantics; strong functors; initial algebras; terminal coalgebras; inductive types; coinductive types},
language = {eng},
number = {1},
pages = {25-68},
publisher = {EDP-Sciences},
title = {Strong functors and interleaving fixpoints in game semantics},
url = {http://eudml.org/doc/273044},
volume = {47},
year = {2013},
}

TY - JOUR
AU - Clairambault, Pierre
TI - Strong functors and interleaving fixpoints in game semantics
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2013
PB - EDP-Sciences
VL - 47
IS - 1
SP - 25
EP - 68
AB - We describe a sequent calculus μLJ with primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of Gödel’s system T. We introduce the notion of a μ-closed category, relying on a uniform interpretation of open μLJ formulas as strong functors. We show that any μ-closed category is a sound model for μLJ. We then turn to the construction of a concrete μ-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients: the construction of a general class of strong functors called open functors acting on the category of games and strategies, the solution of recursive arena equations by exploiting cycles in arenas, and the adaptation of the winning conditions of parity games to build initial algebras and terminal coalgebras for many open functors. We also prove a weak completeness result for this model, yielding a normalisation proof for μLJ.
LA - eng
KW - game semantics; strong functors; initial algebras; terminal coalgebras; inductive types; coinductive types
UR - http://eudml.org/doc/273044
ER -

References

top
  1. [1] A. Abel and T. Altenkirch, A predicative strong normalisation proof for a lambda-calculus with interleaving inductive types, in Selected Papers from Int. Workshop on Types for Proofs and Programs, TYPES ’99 (Lökeberg, June 1999), edited by T. Coquand, P. Dybjer, B. Nordström and J.M. Smith, Springer. Lect. Notes Comput. Sci. 1956 (2000) 21–40. Zbl0988.03029
  2. [2] S. Abramsky, Semantics of interaction : an introduction to game semantics, in Semantics and Logics of Computation, edited by A. Pitts and P. Dybjer. Publications of the Newton Institute, Cambridge University Press 14 (1996) 1–31. Zbl0938.91500
  3. [3] A. Arnold and D. Niwiński, Rudiments of μ-Calculus, Studies in Logic and the Foundations of Mathematics. North-Holland 146 (2001). Zbl0968.03002
  4. [4] D. Baelde and D. Miller, Least and greatest fixed points in linear logic, in Proc. of 14th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2007 (Yerevan, Oct. 2007), edited by N. Dershowitz and A. Voronkov, Springer. Lect. Notes Artif. Intell. 4790 (2007) 92–106. Zbl1137.03323
  5. [5] E.S. Bainbridge, P.J. Freyd, A. Scedrov and P.J. Scott, Functorial polymorphism. Theoret. Comput. Sci.70 (1990) 35–64. Zbl0717.18005MR1047051
  6. [6] W. Belkhir and L. Santocanale, The variable hierarchy for the lattice μ-calculus, in Proc. of 15th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2008 (Doha, Nov. 2008), edited by I. Cervesato, H. Veith and A. Voronkov, Springer. Lect. Notes Artif. Intell. 5330 (2008) 605–620. Zbl1182.03064
  7. [7] A. Blass, A game semantics for linear logic. Ann. Pure Appl. Log.56 (1992) 183–220. Zbl0763.03008MR1167694
  8. [8] P. Clairambault, Least and greatest fixpoints in game semantics, in Proc. of 12th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2009 (York, March 2009), edited by L. de Alfaro Springer. Lect. Notes in Comput. Sci. 5504 (2009) 16–31. Zbl1234.03017MR2545209
  9. [9] P. Clairambault. Least and greatest fixpoints in game semantics 2: strong functors and interleaving types. Informal proceedings of the workshop on Fixed Points in Computer Science, Coimbra, Portugal, September 2009. Zbl1234.03017MR2545209
  10. [10] P. Clairambault, Logique et interaction : une étude sémantique de la totalité. Ph.D. thesis, Université Paris Diderot, Paris 7 (2010). 
  11. [11] P. Clairambault and R. Harmer, Totality in arena games. Ann. Pure Appl. Log.161 (2010) 673–689. Zbl1225.03029MR2591775
  12. [12] J.R.B. Cockett and T. Fukushima, About Charity, Technical report. University of Calgary (1992). 
  13. [13] J.R.B. Cockett and D. Spencer, Strong categorical datatypes I, in Proc. of Int. Summer Category Theory Meeting (Montréal, June 1991), edited by R.A.G. Seely. Canadian Math. Soc. Conference Proceedings. Amer. Math. Soc. 13 (1992) 141–169. Zbl0792.18008MR1192145
  14. [14] J.R.B. Cockett and D. Spencer, Strong categorical datatypes II: A term logic for categorical programming. Theoret. Comput. Sci.139 (1995) 69–113. Zbl0874.68033MR1320236
  15. [15] V. Danos, H. Herbelin and L. Regnier, Game semantics & abstract machines, in Proc. of 11th Ann. IEEE Symp. on Logic in Computer Science, LICS ’96 (New Brunswick, NJ, July 1996). IEEE CS Press (1996) 394–405. MR1461851
  16. [16] P. Dybjer, Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, in Logical Frameworks, edited by G. Huet and G. Plotkin. Cambridge University Press (1991) 280–306. Zbl0755.03033MR1139788
  17. [17] P.J. Freyd, Algebraically complete categories, in Proc. of Int. Category Theory Conf., CT ’90 (Como, July 1990), edited by A. Carboni and M.C. Pedicchio and G. Rosolini, Springer. Lect. Notes Math. 1488 (1990) 95–104. Zbl0815.18005MR1173007
  18. [18] P.J. Freyd, Recursive types reduced to inductive types, in Proc. of 5th IEEE Ann. Symp. on Logic in Computer Science, LICS ’90 (Philadelphia, PA, June 1990). IEEE CS Press (1990) 498–507. MR1099200
  19. [19] P.J. Freyd, Remarks on algebraically compact categories, in Proc. of LMS Symp. on Applications of Categories in Computer Science (Durham, July 1991), edited by M.P. Fourman, P.T. Johnstone and A.M. Pitts. Cambridge University Press. London Math. Soc. Lect. Notes Ser. 177 (1992) 95–106. Zbl0803.18002MR1176959
  20. [20] J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types, Cambridge University Press. Cambridge Tracts in Theoret. Comput. Sci. 7 (1989). Zbl0671.68002MR1003608
  21. [21] R. Harmer, J.M.E. Hyland and P.-A. Melliès, Categorical combinatorics for innocent strategies, in Proc. of 22nd Ann. IEEE Symp. on Logic in Computer Science, LICS ’07 (Wrocław, July 2007). IEEE CS Press (2007) 379–388. 
  22. [22] J.M.E. Hyland, Game semantics, in Semantics and Logics of Computation, edited by A. Pitts and P. Dybjer. Publications of the Newton Institute, Cambridge University Press 14 (1996) 131–184. Zbl0919.68084MR1629523
  23. [23] J.M.E. Hyland and C.H.L. Ong, On full abstraction for PCF: I, II, and III. Inf. Comput.163 (2000) 285–408. Zbl1006.68027MR1808886
  24. [24] A. Joyal and R. Street, Braided monoidal categories, Math. Report 860081. Macquarie University (1986). Zbl0845.18005
  25. [25] A. Kock, Monads on symmetric monoidal closed categories. Arch. Math.21 (1970) 1–10. Zbl0196.03403MR260825
  26. [26] J. Lambek and P.J. Scott, Introduction to Higher Order Categorical Logic. Cambridge University Press. Cambridge Studies in Adv. Math. 7 (1988). Zbl0642.03002MR939612
  27. [27] O. Laurent, Classical isomorphisms of types. Math. Struct. Comput. Sci.15 (2005) 969–1004. Zbl1084.68025MR2172905
  28. [28] T. Leinster, Higher Operads, Higher Categories, London Math. Soc. Cambridge University Press. Lect. Notes Ser. 298 (2004). Zbl1160.18001MR2094071
  29. [29] P. Martin-Löf, Hauptsatz for the intuitionistic theory of iterated inductive definitions, in Proc. of 2nd Scandinavian Logic Symp. (Oslo, June 1970), edited by J.E. Fenstad, North-Holland. Stud. Logic Found. Math. 63 (1971) 179–216. Zbl0231.02040MR387023
  30. [30] G. McCusker, Games and full abstraction for a functional metalanguage with recursive types, Ph.D. thesis, Imperial College (1996). Also published in Springer’s Distinguished Dissertations in Comput. Sci. ser. (1998). Zbl0917.68192MR1667038
  31. [31] G. McCusker, Games and full abstraction for FPC. Inf. Comput.160 (2000) 1–61. Zbl1046.68508MR1784038
  32. [32] P.-A. Melliés, Typed lambda-calculi with explicit substitutions may not terminate, in Proc. of 2nd Int. Conf. on Typed Lambda Calculi and Applications, TLCA ’95 (Edinburgh, Apr. 1995), edited by M. Dezani-Ciancaglini and G. Plotkin, Springer. Lect. Notes Comput. Sci. 902 (1995) 328–334. Zbl1063.03522MR1477992
  33. [33] M. Okada and P.J. Scott, A note on rewriting theory for uniqueness of iteration. Theory. Appl. Categ.6 (1999) 47–64. Zbl0933.68067MR1732462
  34. [34] J. Power and G. Rosolini, Fixpoint operators for domain equations. Theoret. Comput. Sci.278 (2002) 323–333. Zbl1002.68087MR1901610
  35. [35] L. Santocanale, Free μ-lattices. J. Pure Appl. Algebra168 (2002) 227–264. Zbl0990.06004
  36. [36] L. Santocanale, μ-bicomplete categories and parity games. Theor. Inform. Appl.36 (2002) 195–227. Zbl1024.18001MR1948769
  37. [37] W. Thomas, Languages, Automata, and Logic, in Handbook of Formal Languages, Beyond Words, edited by G. Rozenberg and A. Salomaa. Springer 3 (1997) 389–455. Zbl0866.68057MR1470024

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.