RE: A question about structural congruence

["fu yx" <fu-yx@xxxxxxxxxxxxxx>]

Some points:

(i) If n \notin fn(P) & m \notin fn(Q) then definitely P==Q.

(ii) We are talking about a pair of structural scissors,
not a pair of semantic scissors. (nu n)n and (nu n)n.n
are semantically congruent. But I don't think they are 
structurally congruent. For another example, (nu n)n
and (nu a)(nu b)(a|b) are semantic congruent. But there
is no reason why they are structurally congruent. 
Ben's argument is reasonable for semantic congruence. 
I am not convinced that it is also a reasonable argument 
for structural congruence.

(iii) The point about n!=m is that it is a correct thing
to assume. There is little point in assuming n=m.

Yuxi


-----Original Message-----
From: Benyamin Aziz [mailto:baziz@xxxxxxxxxxxxxx]
Sent: 2001年5月12日 18:15
To: Davide Sangiorgi
Cc: Luis Caires; moca@xxxxxxxxxxxxxxx
Subject: Re: A question about structural congruence


Does this mean that we can affirm the following statement?
n \notin fn(P) & m \notin fn(Q)   ==>   P=Q
Whereas in any other case, nothing can be said about P and Q.
I think this is reasonable.  If you imagine (nu n) and (nu m) as a pair of
scissors that cuts any external communication channels (free names), then you
can never tell, unless you know the inner structure of both P & Q, as to how
many channels you have cut! (or, in other words, as to how many free names did
P and Q have before the restrictions).  The only case when you are able to
know is when that number is 0.  And this is precisely when n is not in fn(P)
"and" m is not in fn(Q).
I don't think that whether n = m really matters.
Ben

Davide Sangiorgi wrote:

> Sorry, i overlooked n!=m, my examples were using n=m and hence do not
> apply -- thanks Luis (see below)
>
> davide
>
> ---------------------------
>
>  From: Luis Caires <Luis.Caires@xxxxxxxxxxxxx>
>  Subject: Re: A question about structural congruence
>
> Hi Davide,
>
> Note that there are two alternative cases (a) and (b);
> and (b) should apply when the roles of the
> topmost restrictions do not "match":
>
> >  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' [ for some
> P' and Q' ].
>
> In your first example,
> (nu n)P = (nu n) n.0 == (nu m)(nu n) n.0 = (nu m)Q
> hence P = n.0 and Q = (nu n) n.0
> But then P == (nu m) n.0 (since m is not free in n.0) so we
> can pick P' = n.0 and P == (nu m)P'.
> On the other hand, we may pick Q' = n.0.
> So Q == (nu n)Q' and therefore P' == Q'. So (b) holds.
> Your second example also goes through
> in a similar way,  note that in (nu n)P == (nu m)Q
> I'm assuming n!=m, so we need to start from say
> (nu x)(nu y) (x.x + y)  ==   (nu z)(nu y) (y.y + z)...
>
> Luis
>
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
>  http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html

--
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Benjamin Aziz
PhD student
Department of Computer Applications
Dublin City University
Dublin 9, Ireland
email: baziz@xxxxxxxxxxxxxx
Webpage: http://www.compapp.dcu.ie/~baziz
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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