RE: Dynamic binding

[Luca Cardelli <luca@xxxxxxxxxxxxx>]

Hi, I do not know of a better way to say this then you did:

> lexical scoping means static binding, ie, something that satisfies
alpha-convertibility

More operationally, by "lexical" or "static" binding I mean that you can
tell for each "usage occurrence" of a variable/name where its "binding
occurrence" is. In particular, if the binding occurrences are
type-annotated, you can tell the type of each usage occurrence. I
believe that static scoping is pretty much essential to have a type
system at all, although I am sure one can come up with exceptions.

Dynamic scoping is the opposite.

However, "dynamic binding" has assumed a fairly standard meaning of "not
knowing which piece of code will run" (as opposed to, e.g., Fortran).
For example. in object oriented programming, people talk of "dynamic
binding" when referring to virtual method invocation, while perfectly
aware of being in a statically scoped language (in most cases). In this
view, a function parameter should be considered as "dynamically binding"
a behavior to a name: it is "just" a higher-order (static) binding.

In agent languages, however, you want to go further and talk about
"unbinding" and "rebinding", which are certainly dynamic, and cannot be
seen (easily?) as higher-order static bindings. As you say, the above
notion of dynamic binding is not sufficient in open systems.

So, by dynamic binding, in general, I mean pretty much what Jose says in
his introduction, that a name can refer to different behaviors in
different contexts. But this should not be equated to dynamic scoping.
As a counterexample:

The ambient calculus distinguishes between the scope of a name (which
may include type information), from what the name may refer to at any
particular time. For example, if I say "in n.P" the binding and type of
n is determined, but the ambient called "n" that is entered (if any) is
not statically determined. If an ambient called "n" floats by, then "in
n" is "dynamically bound" to it, in the sense that the "in n" operation
may not apply to it. If it floats away, it is un-bound. Still, the
ambient calculus obeys alpha-conversion for restricted names.

	Luca

-----Original Message-----
From: Joachim Parrow [mailto:joachim@xxxxxxxxx]
Sent: Friday, March 02, 2001 12:36
To: Luca Cardelli
Cc: mobile calculi mailinglist; Joachim Parrow
Subject: Re: Dynamic binding


Luca, could you enlighten me about what you mean by the difference
between
"dynamic binding" and "dynamic scoping"? I am not sure there is a
consistent
use of this terminology in the literature.

Certainly, your Ambients use dynamic binding, and as such have been a
significant inspiration for our work. Though I am not sure what you mean
when you say that this is a "perfectly normal lexically scoped calculus"
-
to me lexical scoping means static binding, ie, something that satisfies
alpha-convertibility.

My feeling is that "dynamic binding" and "static binding" are two
fundamental and orthogonal mechanisms, and that both are needed in any
complex system. You can to some extent, as Michael says, encode dynamic
binding by communicating lambda-closures, but this scheme is not
satisfactory in open systems where the complete interfaces are not known
at
compile-time. Or you can emulate dynamic binding by explicit symbol
table
manipulations, but that is not a very abstract way to look at it.

Joachim

Luca Cardelli wrote:

> Before anybody rushes to revive dynamic scoping, I would like to point
> out that there is a difference between dynamic scoping and dynamic
> binding. The Ambient Calculus formalized dynamic binding (in the sense
> of, e.g., dynamically linking and unlinking program modules or
> agents/servers) within a perfectly normal lexically scoped calculus.
>
> You are absolutely right, though, that dynamic binding is of
fundamental
> importance, and that there is virtually no programming language that
> supports it with specific constructs.
>
>         Luca
>
> -----Original Message-----
> From: Joachim Parrow [mailto:joachim@xxxxxxxxx]
> Sent: Thursday, March 01, 2001 14:43
> To: Joachim Parrow; mobile calculi mailinglist
> Subject: Dynamic binding
>
> Dear Mocanese,
>
> I would like to introduce a discussion topic: the issue of dynamic
> binding in mobile calculi.
>
> I don't propose to reopen all philosophical old arguments about
dynamic
> binding, but there are some quite focussed technical questions
involved.
> In mobile code dynamic binding is a reality, in associated
higher-order
> formalisms like HO-pi it is most often absent. Now, supposing that the
> dynamic binding should be formally modelled, what is the best way to
do
> it? Would you encode it or use some new primitve for it, if so how and
> what?
>
> My reson for introducing this at this time is that my student Jose
Vivas
> recently finished his PhD thesis on dynamic binding in mobile calculi.
> Personally I have always been a hardliner in favour of static binding
> but Jose has managed to convince me to be more open-minded. But
dynamic
> binding seems still very little discussed among theoreticians, so it
> would be interesting to hear what you all think.
>
> Jose's thesis can be found at
>
> http://www.it.kth.se/~josev/thesis.html
>
> Joachim Parrow

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