Re: [moca] confused by Sangiogi & Walker's ``up to'' lemmas

[Davide Sangiorgi <Davide.Sangiorgi@xxxxxxxxxxx>]

Dear James, sorry for not answering earlier 
-- i was away from my office last week. Yes, Ole and Damien are quite
right: the condition on monotonicity was introduced precisely for the
reasons they say.  I do not know how far one can go without the
condition: the up-to context technique is useful, and normally one
uses it in combination with other techniques, so one would not want to
rule it out.
Your (and Ole) comments on RPO transitions are intriguing: 
it would be interesting to know whether one can get cleaner
definitions along that way.
Regards,
Davide


James Leifer writes:
> Dear pi friends (and Davide and David in particular!),
> 
> I've been reading the Sangiorgi and Walker pi book, and became
> confused by their presentation of ``up to'' techniques. There appears
> to be (an apparently) superfluous conditions in a key definition. I
> may well be missing something and would be grateful for any comments.
> 
> They first say (Def 2.3.1, p.82) that a relation R _strongly
> progresses_ to S, written R~>S if for all (P,Q) in R and P-{alpha}->P'
> there exists Q' such that Q-{alpha}->Q' and (P',Q') in S:
> 
>            alpha
>      P ------------> P'
>      |               .
>      |R              .S
>      |     alpha     .
>      Q ............> Q'
>     
> 
> Then go on to define that a function F on relations is _strongly safe_
> if
> 
>    R subseteq S and R~>S   implies   F(R) subseteq F(S) and F(R)~>F(S)
> 
> My problem: I don't see the use of the monotonicity with respect to
> subseteq.  In particular, Lemma 2.3.8,
> 
>    If F is strongly safe and R~>F(R) then R and F(R) are included in ~
>    (strong bisimilarity).
> 
> seems to have a simpler proof (requiring no use of
> subseteq-monotonicity) if recast as follows:
> 
>    If F is monotonic wrt ~> and R~>F(R) then R and F(R) are included
>    in ~.
> 
> My proof:
> 
>    Let F^{omega}(R) = Union_{n in omega} F^n(R).
> 
>    Claim: F^{omega}(R) is a bisimulation.
> 
>       Proof of claim: Suppose (P,Q) in F^{omega}(R) and P-{alpha}->P'.
>       By definition, there exists i in omega such that (P,Q) in
>       F^i(R). Since F is monotonic wrt ~> and R~>F(R), we have
>       F^i(R)~>F^{i+1}(R) by repeated application of F.  Thus, there
>       exists Q' such that Q-{alpha}->Q' and (P',Q') in F^{i+1}(R).
>       Hence (P',Q') in F^{omega}(R).
> 
>    End of Claim.
> 
>    Thus, R union F(R) subseteq F^{omega}(R) subseteq ~, as desired.
> 
> End of proof.
> 
> Comments?
> 
> Warm regards,
> -James Leifer
>  INRIA Rocquencourt
>   
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> 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