Re: [moca] all-you-can-eat calculi

[Martin Berger <martinb@xxxxxxxxxxxxxx>]

thanks to all who replied to my query. some further comments below.

martin

-------- From: Uwe Nestmann --------

> MB> i call it "all-you-can-eat" -- where one input consumes
> MB> as many outputs as possible in one go.
>
> Do you mean "as many as available" or "as many as wanted"?

the former, but i suspect that both share features.

> MB>     x.P | \overline{x} | ... \overline{x}  --->  P
>
> "As many as available" is not expressed by this rule alone,
> because it does not enforce it, but only enables it.

that's true. i didn't want to burden my post with too much formal
detail. in addition, "As many as available" can be achieved by various
formal means, none of which has emerged as a clear favourite.

> Apart from this, you may want to look into the (early?)
> works on LOTOS,

thanks, i shall have a look.

-------- From: Pawel Wojciechowski --------

>  > one input consumes as many outputs as possible in one go.
>
> why only one, not all inputs on 'x' ?  :-)

that's an interesting question. the application i have in mind needs
exactly one input on x interacting with arbitrarily many outputs on
that channel. i use a typing system to models this, starting from an
untyped calculus that allows to have many inputs on x in
parallel. there are various ways one can set up the semantics for
multiple parallel inputs, but they all resolve to the same behaviour
for the restriction to unique inputs.

> not sure if useful (probably not) but perhaps you might
> think of distributed algorithms with unknown number
> of processes (that can dynamically join/leave/crash/
> migrate in ad-hoc networks etc.)
>
> e.g. a distributed consensus algorithm accepts a number
> of outputs (each with a possibly different value) and
> completes by reducing some number of inputs (each input
> consumes exactly the _same_ value, chosen from those that
> were output).

thanks, this is very interesting. so you are saying, each process
nondeterministically chooses to output a number on x. if all numbers
coincide the interaction happens between all outputting participants
and the receiver(s)? i see a little problem with this: either

 * the set of numbers to be used is finite, in which case the
   algorithm has a scalability limit and is not compositional, or

 * it is unlimited. then all participants may agree on a number that
   does not correspond to an existing process, which means the
   election needs to be redone. but then it may fail again etc leading
   to the possibility of divergence.


-------- From: GOUAICH Abdelkader --------

> Can't you already express this by the (infinite) recursion operator?

I'm not sure how to do this in a compositional way








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