Re: dynamic binding

[Alan Schmitt <alan.schmitt@xxxxxxxx>]

Hi,

The dynamic join calculus I am developing seems to satisfy the needs
you express.

In this calculus the notion of name scope is different from the notion
of implementation scope (as in pi-calculus with blocking). New dynamic
names are introduced with a nu operator, and implementation for these
names are introduced in new locations. The scope of names is static,
in the sense that to know a given name you need to be in the lexical
scope of its nu, but the implementation scope is dynamic: when sending
a dynamic message, it is routed to the closest enclosing location that
has an implementation for this name (the nice thing is that I still
have the join calculus requirement that routing is deterministic and
locally resolved, except that now it depends on where the routing
occurs). Thus dynamic rebinding occurs at migration.

I think the static scoping of names relates to most lookup and
discovery protocols, where you first need to know some port to access
a given resource, and the dynamic scoping of implementation gives you
access to the local resource that resides on the well-known port (I
need to know that finger is on port 79, but when I call the port 79
service, I don't specify which machine I'm interested in, it's the
local one).

On top of this, there is a type system that ensures resource
availability: when a message is sent on a dynamic name, there is an
enclosing location that implements it (it's a kind of receiptiveness,
even though this notion is not as strong in the join calculus as in
the pi calculus, since there is always a definition for static
names. For dynamic names, however, it is possible to create a new name
without having any implementation for it, so I just need to check that
the name is implemented.) This type system deals with the creation of
new names (ie nu that are guarded by a join pattern) and the creation
of locations implementing dynamic names (it can type a process that
receives a dynamic name, creates a new location implementing a
definition for this name and sends back the location. In this case, I
use polymorphism to talk about this dynamic name without knowing what
it is). The main issue I had when proving subject reduction is that
names occur in types, and substitution and alpha-conversion get a
little tricky.

Best regards,

Alan Schmitt

++ 08/03/01 14:41 +0100 - Joachim Parrow:
<snip>
>What I am
>loking for is an abstract way of describing that V here immediately
>gains access to local names. This has some dramatic consequences, for
>example these local names will no longer be alpha-convertible.
>
>I agree that all this can be encoded in pi if we superimpose a protocol
>where all local names are first transmitted to incoming processes. But
>this is not a very abstract way to look at it (and also does not really
>conform to what happens computationally in migrating code, where for
>example V would not necessarily be trusted to conform to any protocol).
>Certainly Luca's ambients is a more abstract solution but this issue
>seems not much discussed.
>
>This LISP-paradigm is a rather special case (where S is the caller and V
>the called function).
>
>Joachim



--
The hacker: someone who figured things out and made something cool happen.

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