* Thomas Hildebrandt (hilde@xxxxxx) wrote: > Hi Alan, > > thank you for your reply, the typo does explain some of my confusion, > but I am still a bit puzzled > exactly which definitions that contain typos, maybe you can clarify > that for me. The confusion is entirely my fault: I was looking at our working version when I answered, not the old one I put online, and several other things have been fixed since. I will update to the current version soon. > >Surprisingly enough, we did not know Howe's method when we started > >working on bisimulations for the Kell Calculus. As generalizing it to > >nested locations seemed as hard as the approach we were using, we did > >not pursue it. > > > > I can recommend the presentation of Baldamus and Frauenstein. It can be > found online in a technical report 95-21 from Berlin University of > Technology, 1995. Thanks for the link. We looked at "Bisimilarity as a Theroy of Functional Programming" by Andrew Gordon (BRICS NS-95-3, 1995) here. > > > It do clarify some things... But just to be precise: > > - you change the definition of barbed bisimulation ~b to closed terms > (Def. 8). Yes. > > - you change the definition of barbed congruence (Def. 9) such that you > close the two processes > before inserting them in a closed context, i.e. two open processes P > and Q, define P~bc Q if > for all closing substitutions s, and all closed contexts K, K(Ps)~b > K(Qs). Yes, for all substitution s from variables to processes _and_ for names to names (this is necessary to prove that ~bc is a congruence under input prefixing for pattern languages that allow name passing). > > If that is the case it looks consistent with what you write below. > > However, then I can not see that ~bc is the largest congruence included > in ~b (as you state in proposition 2). ~bc is defined on open terms > and ~b is defined on closed terms, right? Yes, ~bc restricted to closed termes is the largest congruence included in ~b. > > Clearly ~bc is included in the open extension ~bo of ~b defined by P~bo > Q if for all closing substitutions s it holds that Ps~b Qs. > But I can not convince my self that ~bc is a congruence in the usual > sense, i.e. is it a congruence wrt input prefix on open terms?? That > is, if P~bc Q are two open terms, will a<x> >P and a<x> > Q be related? Yes, they are related. We are cleaning up the proofs right now, we should have a technical report out shortly. > > I agree that it would be very interesting in getting normal > bisimulations extended to calculi > with locations.This is also one of our current topics for Homer. We have found that the most complex issue in developing these equivalences is dealing with the interaction between restriction and copying of running processes. This is even more acute when designing a form of normal bisimulation. Is it your impression as well? > > Only the EXPRESS paper is available so far. The others may be available > in old versions, but I would recommend waiting for the technical report > to come within the next 10 days..., since the others do contain bugs. OK, thanks a lot. Best, Alan Schmitt -- The hacker: someone who figured things out and made something cool happen. .O. ..O OOO
Attachment:
pgpJPsPaOwmhB.pgp
Description: PGP signature