Re: [moca] Combinators i Have Known And Loved

[Ilaria.Castellani@xxxxxxxxxxxxxxx]

If I may follow up on Joachim's reply :

Quoting 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

I agree with Joachim : guarded sums (defined up to the commutative monoid laws 
for +) are a notation for labelled transition systems, which in turn are the 
most commonly agreed model for process calculi. 

Since sum seems to be required more at the specification level ("behaviour") 
than at the descriptive level ("implementation"), one may say that it is more a 
specification than a programming primitive, and as such is somehow less 
fundamental than, say, parallel composition - for instance, it is considered 
more serious that an equivalence fails to be preserved by parallel composition 
than by sum. Moreover, since (abstract) specifications are often tied to the 
particular semantics one has in mind, the choice of a specific sum operator 
will depend on the intended semantics. For instance, if you are interested in 
testing semantics (a la De Nicola and Hennessy) or in failure semantics, you 
will use the two operators of internal and external choice, rather than CCS 
sum.

The choice of mixing programming and specification constructs in the same 
language makes it possible to directly compare a process with its specification 
(through an equivalence, or algebraic laws). On the other hand, to my 
view, having specification constructs in the language is a way to "introduce 
semantics into syntax".

Now, what is to be considered as a specification construct may vary not only 
according to the abstract semantics but also to the basic operational model of 
reference. If one's preferred model is not transition systems but some "true 
concurrency model" like Petri nets, event structures, asynchronous transition 
systems or transition systems with independence, for instance, one would 
probably see parallel composition also as a specification (as well as a 
programming) construct.

All this is to say that if you want to compare different sum operators, Martin, 
and possibly decompose them into simpler ones, you might have to consider an 
additional parameter, namely semantics

-Ilaria


> 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 
> 




-------------------------------------------------
This mail sent through IMP: http://horde.org/imp/

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