Re: A question about structural congruence

[Davide Sangiorgi <Davide.Sangiorgi@xxxxxxxxxxxxxxx>]

I do not know the answer. 

The statement you propose is not true if n and m are not required to
occur free in P and Q. For instance
 (nu n) n.0 == (nu m)(nu n) n.0
but n.0 and (nu n) n.0 are unrelated. 

One can repeat similar examples if n and m are required to occur free 
and you have a matching operator in the calculus.  
If n and m are required to occur free and you do not have matching,
there is still a counterexample (which i learned from Marco Pistore):
 (nu x)(nu y) (x.x + y)  ==   (nu x)(nu y) (y.y + x) 
However (nu y) (x.x + y)  and    (nu y) (y.y + x) 
are unrelated.


Davide




Luis Caires writes:
> Hello all,
> 
> I would like to place a question about structural
> congruence as defined say in Milner's "Functions
> as Processes".
> 
> Let == be pi-calculus structural congruence,
> and P and Q processes such that
> 
> (nu n)P == (nu m)Q                                  (1)
> 
> where wlog assume n != m.
> 
> What can be said in general about P and Q? Does anyone
> know of some proven result relating P and Q under ==  given (1)?
> 
> A conjecture may be something like:
> 
>  either (a) P == Q{n<->m} (where {n<->m} denotes exchange of n and m),
>  or          (b) P == (nu m)P' and Q == (nu n)Q' and P' == Q'
> 
> Thanks for any help...
> 
> Best,
> 
> Luis
> 
> 
> 
> 
>   
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> 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