PROTOCOLLO Home Page Other Workshop Information

Invited Speakers to ProToCoLLo Final Workshop

Jean-Yves GIRARD     Ludics and the CAR algebras

In joint work with Harmer and Mellies I describe
the outlines of a theory which may be applied
inter alia to construct interesting categories
of games and strategies.
Our construction starts from a basic model
of intuitionistic linear logic augmented by
further computational structure. The key
new elements are a distributive law of the
standard exponential comonad $!$ over an
exponential monad $?$, and an additive version
of implication, the whole satisfying axioms which we
make precise. It seems that there are many
examples of this computaional situation.
Our construction is the bi-Kleisli category
derived from the distributive law. In the cases
we identify this produces a cartesian closed
category, and so a model of typed lambda
Generally we expect these models to be new. However
in one case we get the cartesian closed category of arena
games and innocent strategies. The notion of
innocent strategy as currently understood was one
component in a games model for PCF, and has become
an established part of game semantics. However the
notion has seemed ad hoc to many and honest proofs
of its properties can seem fiddly. Our approach derives
the problematic (and seldom proved) result that innocent
strategies compose from the distributive law. This
uncovers the implicit combinatorics of innocence and
allows that to be organised in a comprehensible fashion.
This work provides a categorical context allowing a
rational reconstruction of innocent strategies and
the construction of other similar classes of strategies.

                            Semantics and Complexity

        The typical AI problem of making a plan of the actions to be
        performed by a robot so that it could get into a set of final
        situations, if it started with a certain initial situation, is
        generally very complex.
        We introduce Horn linear logic as a comprehensive logical system
        capable of handling the typical AI problem of making a plan.
        We show that linear logic provides a convenient and adequate
        tool for representing planning problems in nondeterministic domains:
        among other things, linear logic formalism allows us to
        show that the planning problem under uncertainty,
        is decidable for the general case of nondeterministic domains.
        The planning problem under uncertainty about the effects of
        actions, or games `Robot against Nature', is proved to beEXPTIME-complete.

        Fixing a finite signature,
        that is a finite set of predicates and their finite domains,
        we get a polynomial time procedure
        of making plans for the robot system over this signature.
        The planning complexity is reduced to PSPACE
        for the robot systems with only pure deterministic actions.
        As a result, the AI planners are very sensitive to the number of
        the variables involved, the inherent symmetry of the problem,
        and the nature of the logic formalisms being used.
        A particular interest of our results is focused on planning problems
        with an unbounded number of functionally identical objects.
        We show that for such problems linear logic is
        especially effective and leads to dramatic contraction of the
        search space (polynomial instead of exponential).
        Our paper addresses the key issue: ``How to automatically
        recognize functions similarity among objects and break the
        extreme combinatorial explosion caused by this symmetry,'' by means
        of replacing the unbounded number of specific names of objects
        with one generic name and contracting thereby the exponential search
        space over `real' objects to a small polynomial search space but
        over the `generic' one, with providing a more abstract formulation
        whose solutions are proved to be directly translatable into
        (optimal) polytime solutions to the original planning problem.


Last modified: September 2004