Re: [moca] shooting from the hip: Mobility FAQ ?

[Martin Berger <martinb@xxxxxxxxxxxxxx>]

* what on earth is bound output and why do you use it?

Bound output \overline{x}(y)P  is an abbreviation for

     (\nu y)( \overline{x}y | P)

where y \neq x. the reason it is sometimes convenient to use is that
it simplifies things (such as typing systems): unlike free output,
using bound output guarantees that all the names being output are
fresh to the receiver.  work by sangiorgi and others has shown that
the restriction to bound outputs does not sacrifice much expressivity.



* why are typing systems for pi calculi so complicated?

[i don't have a really good answer to this]



* can typing systems for pi calculi be made simpler?

unlikely!



* do you have a list of well established open problems that i can have
  a go at?

No, but it would be nice if we had.



* I was wondering the other day about mapping processes to unix
  processes/ threads and I realised that your fancy calculi don't
  provide a notion of thread ID. why not and how can you live without?

Thread IDs are an artifact of the UNIX concurrency model. Concurrency
theory has much more elegant ways of naming things now. don't use
thread IDs (unless you are implementing a concurrency package, and
even then they might not be necessary).



* what is the relation between UNIX threads/processes and pi
  processes?  can I map the latter to the former in implementations?

pi processes are very lightweight, UNIX threads/processes are heavy.
implementing the former by the latter is unlikely to be a good idea
and bound to lead to something really slow.



* You do all this message passing, what about shared memory
  concurrency?  Isn't it more efficient?

The precise relationship between message passing and SMC is still not
clear but message passing seems more fine-grained and is conceptually
simpler.  In some sense both can implement each other, but message
passing encoding of shared memory is more simple and elegant than the
other way round.

In any case, in many implementations both amount to the same thing,
once you see the correspondence between the event notification
mechanisms: names and condition variables. in both cases, the
operating system will implement them as queues where processes get
stored until some relevant event happens.



* what is this fabled thing compositionality?

[to be written]



* what is pi known to be bad at?

The semantics of pi-like calculi assume failure free routing of
messages for example.  The infinite availability of new names is
sometimes a problem, eg the sliding window protocols have been
invented to overcome a finite supply of names. pi-calculi with just a
finite supply of new names have not been investigated.



* Process calculists for ever go on about expressivity? Doesn't the
  Church Turing Thesis solve everything in this regard?

Yes and no. As a matter of practical programming experience, some
problems are much more easily solved in certain programming languages
rather than others, the CTT notwithstanding. The study of expressivity
seeks to put these intuitions on a firm footing. It is not clear how
to best do this, but most current approaches focusing on what
properties translations between languages can or cannot have.  The
properties that we are currently most interested in are

   - closure under renaming, ie it does not matter if we (injectivly)
     rename a program from a language L first and then translate it into L'
     or vice versa.

   - compositionality: if f(p1, ..., p1) is an L-program then its translation
     into L' should be of the form g(q1, ..., qn) where qi depends on pi only
     and g on f only.

others are possible.



* a lot in pi reminds me of objects or actors. both pass messages to
  each other, both are boundaries in some sense. Aren't they the same
  really?

There are many similarities and influences. Pi is rigorously formal
for a start, unlike some accounts of objects or actors. Objects also
come with additional constructs like subtyping, classes, inheritance
which are not basic in pi calculi (although they can be expressed
conveniently).



* I do model checking, hence pi-calculi are useless for me as they are
  undecidable.

You can easily get to decidable fragments by typing. doing so has the
benefit of providing a rich set of reasoning tools for free.



* Pi calculus looks very much like continuations. What's the
  connection?

Indeed, pi can be understood as a generalisation of continuation
passing.  As pi has parallel composition, does not rely on beta
reduction and can conveniently express lambda based CPS, it would
appear that CPS is a peculiar form of pi-calculus.



* at a party i meet this beautiful girl/boy who asked me what i do. by
  the time i had explained bisimulations her/his eyes had glazed and
  she/he left to chat with a hunky car-mechanic/curvy hairdresser. what
  did i do wrong?

sorry mate, you are on your own here. being a semanticist diminishes
your reproductive fitness! but doesn't knowing about relative pushouts
more than compensate?

 martin

 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html