[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [moca] Locality and Name Matching in pi-calculus
More generally, any other such examples of equivalences that
relate to common practice would be interesting.
following the time-honoured tradition of academics using perfectly
reasonable questions as an excuse to wibble about fancyful ideas
of theirs rather than giving a straightforward answer, i would
like to venture a conjecture:
given any finite set of pairs (P1, Q1), ...,(Pn, Qn) of processes
in your favourite calculus (maybe with the mild restriction that
we can't find i, j, C[] such that (Pi, Qi) = (C[Pj], C[Qj]), but
i'm not sure this is really necessary) we can identify a sub-
calculus containing at least P1, ..., Qn such that the induced
canonical reduction/barbed congruence equates P1 with Q1, P2 with
Q2 ... and Pn with Qn.
the construction that i think makes this work does not allow for
infinite sets of equations, though i suspect one could make
it work if they were "very well behaved". the resulting subcalculi
are usually probably pretty "ugly", so my conjecture, should its
graduation to theoremhood be possible, will not be of much use!
what it seems to show is that equations on their own are not very
interesting. what we want is as many equations as possible (to
simplify reasoning) without loosing expressivity.
martin
http://dcs.qmul.ac.uk/~martinb
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html