I have a question for anyone who happens to know: are bisimulations more common in process calculi such as the π-calculus because of τ transitions?
Lately I've been proving some simulation theorems for λ calculi, and none of them is a bisimulation; there are too many "administrative" reductions in the implementation semantics, so it's not possible to guarantee that every one-step reduction in the implementation semantics corresponds to a reduction sequence in the specification semantics.
Now, it's been a while since I looked at the π-calculus, but I seem to recall that you can hide a sequence of reductions inside a "black box" and call them a single transition τ. I suspect this facility allows you to pretend a sequence of transitions is a single transition in order to hide the details of an implementation semantics, effectively producing a completely indistinguishable simulation.
(This is admittedly all a little vague since my knowledge of bisimulations is scant.)
Showing posts with label bisimulations. Show all posts
Showing posts with label bisimulations. Show all posts
Sunday, March 25, 2007
Subscribe to:
Posts (Atom)
