Abstract
We show how solutions to many recursive arena equations can be computed in a natural way by allowing loops in arenas. We then equip arenas with winning functions and total winning strategies. We present two natural winning conditions compatible with the loop construction which respectively provide initial algebras and terminal coalgebras for a large class of continuous functors. Finally, we introduce an intuitionistic sequent calculus, extended with syntactic constructions for least and greatest fixed points, and prove it has a sound and (in a certain weak sense) complete interpretation in our game model.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abel, A., Altenkirch, T.: A predicative strong normalisation proof for a lambda-calculus with interleaving inductive types. In: Coquand, T., Nordström, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol. 1956, pp. 21–40. Springer, Heidelberg (2000)
Abramsky, S.: Semantics of interaction: an introduction to game semantics. In: Semantics and Logics of Computation, pp. 1–31 (1996)
Abramsky, S., Jagadeesan, R.: Games and full completeness for multiplicative linear logic. J. Symb. Log. 59(2), 543–574 (1994)
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full Abstraction for PCF. Info. & Comp. (2000)
Abramsky, S., Kohei, H., McCusker, G.: A fully abstract game semantics for general references. In: LICS, pp. 334–344 (1998)
Baelde, D., Miller, D.: Least and greatest fixed points in linear logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol. 4790, pp. 92–106. Springer, Heidelberg (2007)
Clairambault, P., Harmer, R.: Totality in Arena Games (submitted, 2008)
Conway, J.H.: On Numbers and Games. AK Peters, Ltd. (2001)
De Lataillade, J.: Second-order type isomorphisms through game semantics. Ann. Pure Appl. Logic 151(2-3), 115–150 (2008)
Dybjer, P.: Inductive sets and families in Martin-Löfs Type Theory and their set-theoretic semantics: An inversion principle for Martin-Lös type theory. Logical Frameworks 14, 59–79 (1991)
Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log. 65(2), 525–549 (2000)
Freyd, P.: Algebraically complete categories. In: Proc. 1990 Como Category Theory Conference, vol. 1488, pp. 95–104. Springer, Heidelberg (1990)
Godel, K.: Über eine bisher noch nicht bentzte Erweiterung des finiten Standpunktes. Dialectica (1958)
Harmer, R.: Innocent game semantics. Lecture notes (2004)
Harmer, R., Hyland, J.M.E., Melliès, P.-A.: Categorical combinatorics for innocent strategies. In: LICS, pp. 379–388 (2007)
Hyland, J.M.E.: Game semantics. Semantics and Logics of Computation (1996)
Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000)
Joyal, A.: Remarques sur la théorie des jeux à deux personnes. Gaz. Sc. Math. Qu. (1977)
Laurent, O.: Classical isomorphisms of types. Mathematical Structures in Computer Science 15(5), 969–1004 (2005)
Loader, R.: Equational theories for inductive types. Ann. Pure Appl. Logic 84(2), 175–217 (1997)
Lorenzen, P.: Logik und Agon. Atti Congr. Internat. di Filosofia (1960)
McCusker, G.: Games and full abstraction for FPC. Inf. Comput. 160(1-2), 1–61 (2000)
Melliès, P.-A.: Asynchronous games 4: A fully complete model of propositional linear logic. In: LICS, pp. 386–395 (2005)
Santocanale, L.: Free μ-lattices. J. Pure Appl. Algebra 168(2-3), 227–264 (2002)
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2), 285–309 (1955)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clairambault, P. (2009). Least and Greatest Fixpoints in Game Semantics. In: de Alfaro, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2009. Lecture Notes in Computer Science, vol 5504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00596-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-00596-1_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00595-4
Online ISBN: 978-3-642-00596-1
eBook Packages: Computer ScienceComputer Science (R0)