Strong functors and interleaving fixpoints in game semantics

Clairambault, Pierre

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 47 (2013) no. 1, pp. 25-68.

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.

[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. | Zbl

[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. | Zbl

[3] A. Arnold and D. Niwiński, Rudiments of μ-Calculus, Studies in Logic and the Foundations of Mathematics. North-Holland 146 (2001). | Zbl

[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. | Zbl

[5] E.S. Bainbridge, P.J. Freyd, A. Scedrov and P.J. Scott, Functorial polymorphism. Theoret. Comput. Sci. 70 (1990) 35-64. | MR | Zbl

[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. | Zbl

[7] A. Blass, A game semantics for linear logic. Ann. Pure Appl. Log. 56 (1992) 183-220. | MR | Zbl

[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. | MR | Zbl

[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. | MR | Zbl

[10] P. Clairambault, Logique et interaction : une étude sémantique de la totalité. Ph.D. thesis, Université Paris Diderot, Paris 7 (2010).

[11] P. Clairambault and R. Harmer, Totality in arena games. Ann. Pure Appl. Log. 161 (2010) 673-689. | MR | Zbl

[12] J.R.B. Cockett and T. Fukushima, About Charity, Technical report. University of Calgary (1992).

[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. | MR | Zbl

[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. | MR | Zbl

[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. | MR

[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. | MR | Zbl

[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. | MR | Zbl

[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. | MR

[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. | MR | Zbl

[20] J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types, Cambridge University Press. Cambridge Tracts in Theoret. Comput. Sci. 7 (1989). | MR | Zbl

[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] 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. | MR | Zbl

[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. | MR | Zbl

[24] A. Joyal and R. Street, Braided monoidal categories, Math. Report 860081. Macquarie University (1986). | Zbl

[25] A. Kock, Monads on symmetric monoidal closed categories. Arch. Math. 21 (1970) 1-10. | MR | Zbl

[26] J. Lambek and P.J. Scott, Introduction to Higher Order Categorical Logic. Cambridge University Press. Cambridge Studies in Adv. Math. 7 (1988). | MR | Zbl

[27] O. Laurent, Classical isomorphisms of types. Math. Struct. Comput. Sci. 15 (2005) 969-1004. | MR | Zbl

[28] T. Leinster, Higher Operads, Higher Categories, London Math. Soc. Cambridge University Press. Lect. Notes Ser. 298 (2004). | MR | Zbl

[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. | MR | Zbl

[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). | MR | Zbl

[31] G. Mccusker, Games and full abstraction for FPC. Inf. Comput. 160 (2000) 1-61. | MR | Zbl

[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. | MR | Zbl

[33] M. Okada and P.J. Scott, A note on rewriting theory for uniqueness of iteration. Theory. Appl. Categ. 6 (1999) 47-64. | MR | Zbl

[34] J. Power and G. Rosolini, Fixpoint operators for domain equations. Theoret. Comput. Sci. 278 (2002) 323-333. | MR | Zbl

[35] L. Santocanale, Free μ-lattices. J. Pure Appl. Algebra 168 (2002) 227-264. | Zbl

[36] L. Santocanale, μ-bicomplete categories and parity games. Theor. Inform. Appl. 36 (2002) 195-227. | Numdam | MR | Zbl

[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. | MR | Zbl