Re: x2AnyChannels do not allow alting

[Michael Goldsmith <michael@xxxxxxxx>]

Peter wrote:
> 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?
>[snip]

[I guess I probably count, more than just geographically:-).]

Yes, that's the mathematical interpretation.  What it really means is that no
process should be able to rely on distinguishing them, thereby giving liberty
to compiler writers and chip designers to treat either piece of code in a way
that suits them; as Peter correctly pointed out, equivalence is by no means a
one-way street.

Rather than work out the equivalences from the denotational semantics, people
might prefer to look at:

@Article{RoscoeHoare:LooP,
  author = 	"A.W. Roscoe and C.A.R. Hoare",
  title = 	"{The laws of\/ {\sf occam} programming}",
  journal = 	"Theoretical Computer Science",
  year = 	"1988",
  volume = 	"60",
  pages = 	"177-229"
  note =	"Previously published (1986) as Oxford University Computing
		Laboratory technical monograph PRG--53"
}

It's talking about occam 1, but that's where all the theoretically interesting
stuff is, anyway, at least for this kind of topic...

				Cheers,
									     M