[Prev][Index][Thread]
[mcvax!doc.ic.ac.uk!sa@uunet.UU.NET: Re: [meyer: TYPE:TYPE]]
From: mcvax!doc.ic.ac.uk!sa@uunet.UU.NET
Date: Mon, 7 Dec 87 17:34:20 GMT
To: meyer@theory.lcs.mit.edu
Subject: Re: [meyer: TYPE:TYPE]
The question of whether simulation is just Bohm tree equivalence
modified to handle weak hnf's is carefully examined by Ong in Chapter 2
of his thesis.
Surprisingly enough, he shows that it isn't.
How does bisimulation arise from non-determinism and powerdomains?
I have a clear technical answer for finitary SCCS; one gets a fully
abstract semantics (wrt bisimulation) using a domain equation
involving the Plotkin powerdomain:
D = P[Sigma_{a in Act} D]
where Act is the action monoid, and Sigma(-) is extended separated sum
(and P is the Plotkin powerdomain with empty set).
Each iteration of the process of constructing a solution for this equation
corresponds to one level in the inductive definition of bisimulation;
the quantifier forms in the definition of bisimulation correspond to the
Egli-Milner ordering.
A detailed treatment of this and related matters is given in another draft
paper. Perhaps I should promise at this stage to send no more tantalising
hints until you have had a chance to see the details.
Best regards, Samson (Abramsky)