Re: Encoding pi calculus in Calculus of Structures

On Dec 6, 2004, at 2:12 PM, Alessio Guglielmi wrote:

> Dear Alexander,
>
> mainly, I have the papers by Eric Goubault and Maurice Herlihy in 
> mind. You can find some references in Herlihy's Goedel lecture 
> <http://www.cs.brown.edu/people/mph/finland.pdf>. You can access some 
> papers from my server 
> <http://www.ki.inf.tu-dresden.de/~guglielm/Groucho/> (login as groucho 
> marx).
>
> On the proof theory side, I think Francois is much more competent than 
> me. Francois, could you answer? I'm sure your answer could be 
> interesting for the entire list. What happened to your manifesto?
>
> Anyway, for the time being I'd only say that (at least to me) it seems 
> natural to consider proofs as traces of concurrent computation, and to 
> model this by algebraic topology methods. How exactly to do so, I 
> think nobody can say for the time being, but many would agree that 
> we'll get there pretty soon. Francois?
>
> -Alessio

Things are moving fast and I have some catching up to do in that field. 
Some recent results are sketched in

http://www.math.aau.dk/~uli/getco04/prog.html

The point of using algebraic topology for concurrency is that 
presenting a process by a trace (i.e. abbabaabbb...) is very 
bureaucratic and some quotienting has to be done; moreover if good 
notions of asynchrony have to be defined the quotients in question are 
much more subtle than your garden variety of bisimulation.

An execution trace is a one-dimensional object, and "equivalences" 
betweens bits of executions can be presented by higher-dimensional 
spaces that connect them. The idea has been around for a long time (I 
think it's Vaughn Pratt who proposed it). Now if you can describe your 
stuff as a combinatorial space (what topologists call a complex) you 
have access to very powerful tools that describe geometric invariants 
like loops and higher dimensional versions of them. This has obvious 
computational interest.

Unfortunately conventional invariants like standard homology and 
homotopy have shown themselves to be too weak to be really useable in 
concurrency. But at least ordinary homology is useful for getting 
results in rewriting theory, for example showing that a term equality 
decision problem cannot be solved by a confluent rewriting system.

So Eric Goubault has proposed a more refined version of homotopy, 
called dihomotopy, for which one the paths and homotopies between them 
are not reversibe. The "di" is for "directed". This stuff took a long 
time to get off the ground, but now they have things like van Kampen 
theorems, that allow to get practical computations. Those people have 
to reinvent algebraic topology from the start, which is a pretty 
ambitious program.

I personally think that the objects seen in the calculus of 
structures--the structures---are very much space-like. But as soon as 
you have equations like associativity and commutativity they are a bit 
"more collapsed" than ordinary spaces. I will say more about what I 
mean one of these days.

Another point of contact between logic and algebraic topology is the 
Danos Regnier contraction criterion for multiplicative linear logic. 
This stuff is extremely homotopy-like, but it also deals with spaces 
that are a bit different from those of ordinary topology. This has led 
Francois Metayer to propose a correctness criterion which is based on 
ordinary simplicial homology.

> At 10:47 AM +0000 6.12.04, A.Kurz wrote:
> > Date: Mon, 06 Dec 2004 10:47:07 +0000
> > From: "A.Kurz" <ak155-KujIM1l7rAGFxr2TtlUqVg@xxxxxxxxxxxxxxxx>
> > To: Alessio Guglielmi 
> > <Alessio.Guglielmi-r/9ln3FTDUD4ajHJ1XSv27NAH6kLmebB@xxxxxxxxxxxxxxxx>
> > Subject: Re: [Frogs] Encoding pi calculus in Calculus of Structures
> >
> >
> > Dear Alessio,
> >
> > > Instead, there are now two broad research efforts about semantics of 
> > > proofs (in whatever logics) and semantics of concurrent computation 
> > > that could very well join forces in the near future. I'm thinking 
> > > here, of course, to the use of algebraic topology methods; I think 
> > > this is our future.
> >
> > Can you explain the link to algebraic topology or give my a 
> > reference? (I am new to the list and the subject)
> >
> > Thanks,
> >
> > Alexander