|
Talk
|
| Jean-Yves GIRARD |
Ludics
and the CAR algebras
|
| Martin HYLAND |
CATEGORICAL CONSTRUCTION of INNOCENCE
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
calculus.
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.
|
| Jacqueline VAUZEILLES |
AI PLANNING PROBLEMS in the HORN LINEAR LOGIC:
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.
|
|