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

[James Leifer <James.Leifer@xxxxxxxx>]

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