BRICS · Contents · Programme · References

Games and Free mu-Lattices

A BRICS Mini-Course
June 7 and 9, 2000

Lectures by
Luigi Santocanale, luigis@brics.dk
BRICS

Course Contents

Interaction and communication can be modeled using games. By finding rigorous mathematical structures to games we provide mathematical structure to interaction and communication as they also occur in concurrent computation. In this way, we can decide to design programming languages guided by those mathematical intuitions; we can analyze existing concepts and problems of concurrent computation in terms of games or even translate entire programs into the language of games as strategies. However all of that would be useless if at the same time we were not supported by a strong mathematical theory about games.

The mini-course will consist of two lectures of 2 x 45=91 minutes each.

Programme

Wednesday June 7, 2000, 10:15-12:00 in Auditorium D1

During the first lecture I'll first motivate the use of games as models of interactive computation. I'll explain then the mathematical structure which has been associated to games. There are operations (or constructions) on games which model the connectives of linear logic; there are also operations - inspired from the theory of parity games - which behave like fixed points. I'll introduce to these ideas and focus then on the mathematical notions of lattice, least and greatest fixed points, the goal being that of defining what is a mu-lattice.

Friday June 9, 2000, 10:15-12:00 in Auditorium D1

In the second lecture I'll focus on the structure obtained from lattice operations and fixed points on games: I'll describe a class J(X), the elements of which are games, for a given set X of variable games. I'll describe the mathematical theory associated to this object: J(X) is a mu-lattice and its order relation is decidable; moreover it is a canonical mu-lattice, i.e. it is free over the set X. I'll explain why these mathematical results are of interest from the point of view of interactive computation.

On demand, I'll continue during another lecture developing the mathematical theory of the mu-lattice J(X). For example, I'd like also to explain the problems encountered in the proof of freeness of J(X) and their relations to logical ideas. To prove freeness of J(X) we are forced to admit that circular proofs are sometime good proofs, much better proofs than the usual ones.

References

Here is a bunch of related works. If you're interested in one of them, you'd like to attend the mini-course.

  1. A. Blass, Degrees of indeterminacy of games, 1972.
  2. A. Blass, A game semantics for linear logic, 1992.
  3. J.H. Conway, On numbers and games, 1976.
  4. H. Hu and A. Joyal, Coherence completions of categories, 1996.
  5. A. Joyal, Free lattices, communication and money games, 1997.
  6. A. Joyal, Free bicomplete categories, 1995.
  7. S. Abramsky, R. Jagaadesaan, Games and full completeness for multiplicative linear logic, 1994.
  8. M. Rabin, Decidability of second-order theories and automata on infinite trees, 1969.
  9. L. Santocanale, Sur les mu-treillis libres (my doctoral thesis, for those who like French) 1999.
  10. L. Santocanale, Free mu-lattices, (for those who prefer English) 1999.
  11. L. Santocanale, The alternation hierarchy for the theory of mu-lattices, 2000.
  12. D. Niwinsky, Equational mu-calculus, 1985.
  13. I. Walukiewicz, On completeness of the mu-calculus, 1993.
  14. R. Freese, J. Jevzek, J.B. Nation, Free lattices, 1995.
  15. P.M. Whitman, Free lattices. I/II, 1941/42.
  16. R. Milner, A calculus of communicating systems, 1980.
  17. C.A.R. Hoare, Communicating sequential processes, 1985.
  18. R. Cockett and R. Seely, Finite sum-product logic, 2000.
  19. S. Bloom and Z. Ésik, Iteration theories, 1993.