Higher
dimensional rewriting, concurrency and directed homotopy
Monday February 20
- 14h-14h45 Exploring
homotopy in defining bisimulation for higher dimensional automata
by Rob van Glabbeek
History preserving bisimulation is a
semantic equivalence relation on models of concurrency that tells when
two systems have the same causal and branching structure. In this talk
I show how to define this notion, which originally was proposed on
event structures and related models, in the setting of higher
dimensional automata. The definition is closely related to the concept
of homotopy of paths in a higher dimensional automaton.
Studying the timely behaviour of
concurrent processes by means of process graphs has been known since
Dijkstra, yet the modern approach to the subject by algebro-topological
means, intitiated by Fajstrup, Goubault and Raussen, has appeared only
in the middle 1980's. The key observation was that a process graph is
an ordered topological space and variants of classical
algebro-topological tools were worked out in order to study invariants
of such objects. There are basically two relevant variants of orders on
topological spaces: global and local orders. The former are easier to
handle and therefore better studied, with the drawback that no loops
can be represented. The latter, called local po-spaces, do not exhibit
this drawback, yet they are more complex artifacts. We present partial
results about model structures for local po-spaces. The key observation
here is a certain similarity with the situation in the category of
(affine) schemes, leading to variants of methods introduced by
Voevodsky when setting up the celebrated homotopy theory of schemes.
In this talk, we apply the polygraphic
translation of term rewriting systems to SKS, a calculus of
structures-type formalism describing the proofs of propositional
calculus. We get a 3-polygraph which has three main advantages over the
initial formulation: it allows an easy control over "structural
bureaucracy"; it yields 3-dimensional representations for proofs;
finally, local transformations of proofs have the rich algebraic
structure of 4-dimensional objects.
- 16h45-17h30
Non abelian complexes 1 :
polygraphs and
resolutions by Yves
Lafont
Non abelian complexes are higher
dimensional categories generalizing rewrite systems as well as
CW-complexes. We introduce the fundamental notions for a homotopical
theory of computation.
Tuesday February 21
- 11h-12h30 The
fundamental category of a directed space by Eric Goubault and
Emmanuel Haucourt
During this week, we will deal with the
problem of customizing the construction of the components category to
the case of models containing loops. We also try to go deeper in the
understanding of the relations between M. Grandis spectra and our
components categories,
mostly when the underlying space is compact. Moreover, the fundamental
category construction can be made in a purely categorical abstract
setting that we will present. The purpose of this abstract approach is
the comparison of the fundamental category functors over dTop, PoTop,
LPoTop, Flow ... in other words the different known topological models
for concurrency.
Wednesday February 22
- 9h-10h30 Discussion on model categories
We prove that for any monoid M, the
homology defined in terms of non abelian resolutions coincides with the
homology defined in terms of resolutions by free ZM-modules.
Thursday February 23
Pour une catégorie C
complète et cocomplète, un foncteur nerf pour C
apparaît comme un foncteur de la forme N : C -> Smpl et
admettant un adjoint à gauche. Ce foncteur permet de ramener
l'étude topologique d'un objet X de C à celle de
l'ensemble simplicial N(X). La donnée de l'adjoint N' : Smpl
-> C est le prolongement universel par limites inductives d'un objet
cosimplicial de C. Dans tous les cas observés et familiers
où un tel foncteur N est utilisé, on observe que l'objet
cosimplicial est donné par l'application d'une monade T à
l'objet initial (i.e. vide) de C. En particulier, ce schéma
d'idée s'applique à la catégorie C des
oméga-catégories strictes et l'objet cosimplic, al obtenu
par ces méthodes fonctorielles (très différentes
des
méthodes combinatoires de Street) donne les orientaux de Street.
Ces orientaux semblent être un outil de calcul adapté
à l'homotopie dirigée. Nous donnerons également
une description des algèbres de la monade T.
We study multinomial lattices, or
lattices of paths in higher dimension, which arise from simple rewrite
systems modeling concurrency. We propose a lattice theoretic notion of
dimension, we point out relations to dihomotopy theory.
Friday February 24
- 14h-14h45 Non abelian
complexes 3 : caracterisation of free objects by François
Métayer
We define trivial fibrations and
cofibrations in the category of strict
n-categories, and show that the cofibrant objects are the free ones,
that is those generated by polygraphs.
- 14h45-16h
Discussion on homotopical theory
of computation
Lecture
notes
- Eric Goubault and
Emmanuel Haucourt, The
fundamental category of a directed space (pdf)
- Yves
Lafont, Non abelian complexes 1
:
polygraphs and
resolutions (pdf)
Related papers
- Yves Guiraud, The three dimensions of proofs,
Annals of pure and applied logic (in press), 2005 (pdf)
- François
Métayer, Resolutions by
polygraphs, Theory and Applications of Categories 11 (7),
148-184, 2003 (pdf)