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

[James Leifer <James.Leifer@xxxxxxxx>]

Ole Hoegh Jensen <ohj@xxxxxxxxx> writes:

> You are right that Lemma 2.3.8 does not need subseteq-monotonicity.
> However, the "up-to-context" function would not be safe if you left out
> subseteq-monotonicity from the definition.  (See the proof of Lemma 2.3.21
> and the remarks immediately below it.)

Hi Ole!

Aha. Got it,

> The reason you need subseteq-monotonicity for "up-to-context" is,
> essentially, that in most process calculi you DON'T have this property:
>
>   If C[P] -a-> P' then P -b-> P'' for some b and P'' related to a and P'
>
> I.e., there is no reason to assume that P "contributes" to a transition of
> C[P].  I suspect your interest in this stuff may have something to do with
> reactive systems and RPO-transitions.  :)

Not this time. In fact it arose because I'm teaching pi calculus to
the masters students in Paris.

>  It is worth noting that the above property DOES hold for
> RPO-transitions, as (b,P'') would be an RPO "within" the RPO of the
> first transition.

Right on! Let me refer to my thesis (there are so few times in life
when one can, so I'm going to make the most of it ;-)):

   http://pauillac.inria.fr/~leifer/articles/leifer-thesis-tech.ps.gz

I remarked on this anomaly (bottom of p.33) and proposed a system of
multi-hole contexts where the distinction between the context acting
alone and it acting in concert with the process in the hole is clear
(para before Theorem 3.33, p.58).

Thanks again for the pointers.

Warmest wishes,
-J
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html