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.
@article{ITA_2013__47_1_25_0,
author = {Clairambault, Pierre},
title = {Strong functors and interleaving fixpoints in game semantics},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
volume = {47},
year = {2013},
pages = {25-68},
doi = {10.1051/ita/2012028},
mrnumber = {3072310},
zbl = {1302.03072},
language = {en},
url = {http://dml.mathdoc.fr/item/ITA_2013__47_1_25_0}
}
Clairambault, Pierre. Strong functors and interleaving fixpoints in game semantics. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 47 (2013) pp. 25-68. doi : 10.1051/ita/2012028. http://gdmltest.u-ga.fr/item/ITA_2013__47_1_25_0/
[1] and , 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 0988.03029
[2] , 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 0938.91500
[3] and , Rudiments of μ-Calculus, Studies in Logic and the Foundations of Mathematics. North-Holland 146 (2001). | Zbl 0968.03002
[4] and , 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 1137.03323
[5] , , and , Functorial polymorphism. Theoret. Comput. Sci. 70 (1990) 35-64. | MR 1047051 | Zbl 0717.18005
[6] and , 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 1182.03064
[7] , A game semantics for linear logic. Ann. Pure Appl. Log. 56 (1992) 183-220. | MR 1167694 | Zbl 0763.03008
[8] , 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 2545209 | Zbl 1234.03017
[9] . 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 2545209 | Zbl 1234.03017
[10] , Logique et interaction : une étude sémantique de la totalité. Ph.D. thesis, Université Paris Diderot, Paris 7 (2010).
[11] and , Totality in arena games. Ann. Pure Appl. Log. 161 (2010) 673-689. | MR 2591775 | Zbl 1225.03029
[12] and , About Charity, Technical report. University of Calgary (1992).
[13] and , 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 1192145 | Zbl 0792.18008
[14] and , Strong categorical datatypes II: A term logic for categorical programming. Theoret. Comput. Sci. 139 (1995) 69-113. | MR 1320236 | Zbl 0874.68033
[15] , and , 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 1461851
[16] , 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 1139788 | Zbl 0755.03033
[17] , 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 1173007 | Zbl 0815.18005
[18] , 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 1099200
[19] , 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 1176959 | Zbl 0803.18002
[20] , and , Proofs and Types, Cambridge University Press. Cambridge Tracts in Theoret. Comput. Sci. 7 (1989). | MR 1003608 | Zbl 0671.68002
[21] , and , 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] , 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 1629523 | Zbl 0919.68084
[23] and , On full abstraction for PCF: I, II, and III. Inf. Comput. 163 (2000) 285-408. | MR 1808886 | Zbl 1006.68027
[24] and , Braided monoidal categories, Math. Report 860081. Macquarie University (1986). | Zbl 0845.18005
[25] , Monads on symmetric monoidal closed categories. Arch. Math. 21 (1970) 1-10. | MR 260825 | Zbl 0196.03403
[26] and , Introduction to Higher Order Categorical Logic. Cambridge University Press. Cambridge Studies in Adv. Math. 7 (1988). | MR 939612 | Zbl 0642.03002
[27] , Classical isomorphisms of types. Math. Struct. Comput. Sci. 15 (2005) 969-1004. | MR 2172905 | Zbl 1084.68025
[28] , Higher Operads, Higher Categories, London Math. Soc. Cambridge University Press. Lect. Notes Ser. 298 (2004). | MR 2094071 | Zbl 1160.18001
[29] , 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 387023 | Zbl 0231.02040
[30] , 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 1667038 | Zbl 0917.68192
[31] , Games and full abstraction for FPC. Inf. Comput. 160 (2000) 1-61. | MR 1784038 | Zbl 1046.68508
[32] , 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 1477992 | Zbl 1063.03522
[33] and , A note on rewriting theory for uniqueness of iteration. Theory. Appl. Categ. 6 (1999) 47-64. | MR 1732462 | Zbl 0933.68067
[34] and , Fixpoint operators for domain equations. Theoret. Comput. Sci. 278 (2002) 323-333. | MR 1901610 | Zbl 1002.68087
[35] , Free μ-lattices. J. Pure Appl. Algebra 168 (2002) 227-264. | Zbl 0990.06004
[36] , μ-bicomplete categories and parity games. Theor. Inform. Appl. 36 (2002) 195-227. | Numdam | MR 1948769 | Zbl 1024.18001
[37] , Languages, Automata, and Logic, in Handbook of Formal Languages, Beyond Words, edited by G. Rozenberg and A. Salomaa. Springer 3 (1997) 389-455. | MR 1470024 | Zbl 0866.68057