Re: [moca] Combinators i Have Known And Loved

[Joachim Parrow <joachim@xxxxxxxxxx>]

Sum is needed to represent arbitrary transition systems, and are often
convenient abstractions when low level mechanisms would clutter a
description. For example, in high level descriptions of communication
protocols or distributed algorithms, transition systems and hence sums are
often useful. In low level views, where all mechanisms are defined in
detail, they are often not needed.

Also as you mention sums are needed for complete axiomatisations through an
expansion law. In fact this is also related to viewing terms as denoting
transition systems, to get an easy operational understanding of the normal
forms.

For both these purposes guarded sum suffices. The drawback of guarded sum
is that formally an infinite family of operators is required, since n-ary
guarded sum is not reducible to a sequence of binary guarded sums, as
opposed to the situation with unguarded sum.

I guess you are aware of results by Palamidessi, Nestmann and Pierce on
situations where sum can be encoded.

Joachim Parrow

Martin Berger wrote:

> #2 sum
>
> a perennial questions in process theory is which form of summation
> to use -- if any. i'd like to know what purposes "really" require sums
> and, for each such application, what a minimal dedicated
> combinator doing the same job would look like.
>
> for example, sums can used to implement value passing. a
> corresponding dedicated combinator would be conventional value passing,
> equivalent, seemingly, to input guarded sums where all the
> guards wait on the same name. another example is using sums to
> model a rudimentary form of timers. here one seems to use mixed
> choice. the dedicated combinator would be a proper timer. other
> examples i can think of are be expansion theorems, locking,
> internal choice and solving consensus problems for symmetric
> asynchronous processes.
>
> are you aware of more examples where you think some form of sums is
> necessary?
>
> martin
>
>
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
>  http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html

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