[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Assistance requested on a Hoare-y problem
Greetings -
In my formatting below, I write the expression a -> (P || Q) as
a -> (P
||
Q)
Roy Wilson wrote:
>
>
> Hi,
>
> I'm working my way through Hoare's Communicating Sequential Processes book. I
> am semi-stuck on Example X1 on p. 69. It seems that the chief tool ought to be
> L6 on p. 71, but I've had no luck.
>
> I have done graduate work (in the US :-)) in theory of computation, category
> theory, and the kind of stuff in Appendix A of Roscoe's book, so I'm not a
> stranger to symbolic manipulation, despite my possible stupidity in this
> matter.
>
> If anyone who has actually done a line by line derivation would care to
> communicate the first and second lines (please, no use of "clearly" :-)) of
> the proof, I'd be most appreciative.
>
> Roy
>
> Roy Wilson
> designrw@xxxxxxxxxxxxxxxx
NOISYVM = (coin -> clink -> choc -> clunk -> NOISYVM)
CUST = (coin -> (toffee -> CUST | curse -> choc -> CUST))
NOISYVM || CUST = (coin -> clink -> choc -> clunk -> NOISYVM)
||
(coin -> (toffee -> CUST | curse ->
choc -> CUST))
by L4A: = coin -> (clink -> choc -> clunk -> NOISYVM)
||
(toffee -> CUST | curse -> choc
-> CUST)
by L6: = coin -> (clink -> ((choc -> clunk -> NOISYVM)
||
(toffee -> CUST
| curse -> choc -> CUST))
|
(toffee -> ((clink -> choc ->
clunk -> NOISYVM)
||
CUST))
Since NOISYVM cannot engage in toffee, but any occurrence of toffee must
involve both NOISYVM and CUST - since it appears in both alphabets - the event
toffee
can never occur - leading to
NOISYVM || CUST = coin -> (clink -> (choc -> clunk ->
NOISYVM))
||
(curse -> choc ->
CUST)
Using L6 again:
NOISYVM || CUST = coin -> (clink -> ((choc -> clunk ->
NOISYVM)
||
(curse -> choc -> CUST)))
|
(curse ->
((clink -> choc -> clunk -> NOISYVM)
||
(choc -> CUST)))
Applying L5B to the first component of the |, and L5A to the second:
(NOISYVM || CUST) = coin -> (clink -> curse -> ((choc -> clunk ->
NOISYVM)
||
(choc -> CUST)))
|
(curse -> clink
-> ((choc -> clunk -> NOISYVM)
||
(choc -> CUST)))
Applying L4A twice to both ||:
NOISYVM || CUST = coin -> (clink -> curse -> choc -> clunk ->
(NOISYVM
||
CUST))
|
(curse -> clink ->
choc -> clunk -> (NOISYVM
||
CUST))
NOISYVM || CUST = uX.(coin -> ((clink -> curse -> choc -> clunk -> X)
|
(curse -> clink ->
choc -> clunk -> X))
Does this do it???
Dyke.
--
======================================================================
Dyke Stiles >>>>>> new address!!>>> dyke.stiles@xxxxxxxxxxx
Professor and Chair, Graduate Committee
Department of Electrical and Computer Engineering
Utah State University
4120 Old Main Hill
Logan UT 84322-4120
Voice: +1-435-797-2840 FAX: +1-435-797-3054
Research: http://www.engineering.usu.edu/ece/research/rtpc/
Play: http://www.engineering.usu.edu/ece/research/rtpc/utah/utah.html
======================================================================