Re: question about structural congruence

[Luis Caires <Luis.Caires@xxxxxxxxxxxxx>]

Daniel Hirschkoff wrote:

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

Hi, thanks.

The idea of using some kind of normal form (or a good semantics for SC
as Joachim Parrow mentioned) seems a promising way of doing this kind
of things; but  ... Let me give some extra background:

The motivation for establishing these kind of "fine" properties of
structural congruence arises for example in the study of the satisfaction
relation of spatial logics.  This is the case of the ambient logics of
Cardelli and Gordon,  and of a logic for async-pi that Cardelli and I have
been working on.  In this setting, we preferred to adopt a presentation of
structural congruence known to be decidable: this is convenient for
model-checking purposes. So we adapted spatial congruence
(as defined for ambients) to the async-pi: this congruence includes the
distribution axioms of ! and the prefix commutation axiom mentioned by
Daniel Hirschkoff. Wrt this extended congruence, some "inversion" lemmas
of the kind have been shown by Silvano Dal-Zilio and Witold Charatonik
(both seem to think that the conjecture is true) using related proofs and
techniques; these kind of results are not easy to obtain; and perhaps this
one is even harded.

So, although we are indeed working with the extended SC, I described
the problem in a more general context, because it's connection with the
decidability of SC (which seems to be an open issue: I learned this
recently from Luca) is not that clear.

Luis


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