University of Birmingham > Talks@bham > Lab Lunch >  A dual calculus for unconstrained strategies

A dual calculus for unconstrained strategies

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Neel Krishnaswami.

The aim of the lambda lambda-bar calculus is to represent as faithfully as possible the structure of non-deterministic, non-innocent, non-visible strategies in game semantics. Non-innocent strategies are known to model functional languages extended with references. The typical approach is to model the purely functional fragment with innocent strategies, to which a “memory-cell” strategy is added. Instead, our starting point is a simple concrete syntax of finite strategies, which are inherently non-innocent.

This approach is syntax driven, and the resulting language is a dualization of the lambda calculus. A new binder, the lambda-bar, names arguments which have been passed to the environment (whereas the lambda names arguments which have been received). This makes explicit the act of answering a function call, and allows this answer to change over time, granting the power of general states.

This syntax can then be used to build languages which are simple—i.e. for which interesting properties are decidable—while still allowing for the power of references. We do so by proceeding from the ground up, starting with very simple fragments of the lambda lambda-bar calculus. The duality of the general calculus allows us to give syntactic restrictions which apply uniformly to the Player and Opponent moves, and more directly affect the ability of the strategy to have “complex” behavior. An example of a simple behavior is one that only uses a bounded amount of memory; this can be obtained by checking, syntactically, that only a finite amount of names is needed (after garbage collection). This situation does not occur for any non-trivial innocent interaction; however it does for “pseudo-normal” terms of the calculus.

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.