Re: question about structural congruence

[Daniel Hirschkoff <hirschko@xxxxxxxxxxx>]

Hi,

My impression is that the conjecture first mentioned by Luis Caires
indeed holds in an extended version of structural congruence. Maybe a
way to establish this kind of "inversion result" would be to exploit
the notions of normal form for structural congruence given in works of
Engelfriet, Dal-Zilio (dealing with structural congruence for Mobile
Ambients) and myself.


An idea in computing these normal forms is to push restrictions
upwards in the term, and regroup them. It is often the case that in
doing this, an extra axiom is added in order to let restrictions "go
through" prefixes like this (but tihs is not mandatory):

	 p(nu x).P  ==  (nu x)p.P     if x \notin fn(p), p being a prefix

This way, creation of new names only happens under the replication
operator, except for toplevel restrictions. 

So in general you can reason on normal terms and write

	  (nu n1)...(nu nk)P0  ==  (nu m1)...(nu mk)Q0		(1)

The terms P0 and Q0 don't start with a restriction operator, and all
restrictions on the nis and mjs are "useful" in the sense that these
names occur free in P0 and Q0 respectively. In this case, I have the
impression that there should be the same number of restrictions on
both sides. Then the conjecture should hold: it basically says that in
writing (1) above, permutation of consecutive restrictions is allowed,
so that either n1 "corresponds" to m1 modulo alpha conversion (this is
the (a) case of the conjecture), or n1 and m1 correspond to different
names (case (b)), but then the respective "partners" are to be found
in the remaining restricted names. The fact that you can either
actually replace n with m in case (a) (using your statement of the
conjecture) or find a restriction on m in P and a restriction on n in
Q should hold because structural congruent processes have the same set
of free names (so leave the same names "available" to designate bound
names).


A key point in deciding structural congruence (which is needed to
establish a notion of normal form for \equiv), though, is the addition
of a law stating distributivity of replication w.r.t. parallel
composition (and other less important properties of replication):

	    !(P|Q)  ==  !P | !Q

This law is not present in Milner's "Functions as processes", and I'm
not aware of decidability results for "original" structural
congruence, that is without addition of laws for replication. So if
you're interested in structural congruence without these extra axioms
for replication, then I really don't know the answer to your
question! Hope this helps, still.

daniel
	

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