Re: [moca] Locality and Name matching in Pi-Calculus.

[martinb@xxxxxxxxxxxxxx]

> While I would totally agree with this when it comes to globally used
> unique identifiers, such as IP addresses. I don't think this is the whole
> story, especially when you have non-global communication. I'm thinking of,
> say writing a new local library and sending it to a remote machine,

good point! you mean something like

	P = x(v).!v(w).Q,

a process you may send to a remote site. the remote site receives P and
exectues P | \overline{x}a to bind the server to the name a, say
a local port.

this is almost locality: you only  bind input names at the very beginning
of P's active life. maybe that's the reason why sangiorgi and
others (if i remember correctly) send parameterisable rather than
raw processes: instead of

      \overline<P> | a(p).(p | \overline{x}<a>)

they would probably write

      \overline<!v(w).Q> | a(p).p<a>

where !v(w).Q is an agent with the uninstantiated name w.

this way the problem would somehow go away. on the other hand, one
could argue that this is just a syntactic artefact.

upon further reflection, i'm inclined to say that the point of
locality is not (or should not be) that input subjects are never
input bound, but rather that input subjects are stably available.
in particular, we want to avoid the situation that a process
outputs \overline<x><y>, yet initially without a receiver ...
then, after a lot of computations some other process is suddenly
of the form !x(v).P or x(v).P and can consume the aforementioned
output particle. this is straightforwardly guaranteed by locality,
but it is also enforced if we ensure (statically) that
any input bound subjects are discharged "at the beginning".
this can be formalised in various ways ...

martin (http://www.dcs.qmul.ac.uk/~martinb)
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html