Re: x2AnyChannels do not allow alting

["P.H.Welch" <P.H.Welch@xxxxxxxxx>]

Barry wrote:

> > In CSP, the PAR operator is defined in terms of external choice (sort of
> > ALTing).  In occam, we all know the following equivalencees:
> > 
> >   PAR                    ==             ALT
> >     in0 ? x0                              in0 ? x0
> >     in1 ? x1                                in1 ? x1
> >                                           in1 ? x1
> >                                             in0 ? x0
> 
> I didn't!
> 
> Maybe it's a question of what "==" means, see below.

It means equivalent under the denotational semantics for occam (or, in its
CSP form, for CSP).  See the Transputer Communications article for the full
definitions ;-) ...

At least, I'm pretty sure that's right - confirmation please from Oxford?

> My interpretation ...
> 
> The ALT case indicates that we either do SEQ( in0?x0; in1?x1 ) or
> SEQ( in1?x1; in0?x0 ) which give the same result as each other and as
> concurrent execution of both inputs. So, the ALT form is a valid
> IMPLEMENTATION of PAR, but not the only one - true concurrency is also
> valid.

But, also, the PAR form is a valid implementation of that ALT and a clever
compiler targetting a multiprocessor or silicon could choose to do that
transformation.

Peter.