[Prev][Next][Index][Thread]

[meyer: TYPE:TYPE]

   From: mcvax!doc.ic.ac.uk!sa@uunet.UU.NET <SAMSON ABRAMSKY>
   Date: Mon, 23 Nov 87 11:05:25 GMT
   To: meyer@theory.lcs.mit.edu
   Subject: Re:  [meyer: TYPE:TYPE]

   I will send you the draft paper (which incidentally is by me; Luke Ong
   is writing his thesis on extensions to what I have done.  His thesis
   is shaping up as a very nice piece of work; he should have a draft
   version to circulate by the end of the year, and plans to submit next
   summer.  If you are interested, I will ask him to send you a copy of
   the draft.)

   Meanwhile, here is a hint. Say we are in the untyped pure lambda
   calculus, and we have defined a notion of convergence (e.g. to weak
   head normal form, i.e. an abstraction).  Then we define, for closed
   terms M, N:

    M preord N <-> M converges to lambda x. M' implies N converges to
		    lambda y.N', and for all P, M'[P/x] preord N'[P/x].

   This recursive definition unwinds into a maximal fixpoint; the closure
   ordinal is omega. The realtion can then be extended to all terms by
   ground instances.

   Because there is no non-determinism in this particular language, the
   relation would perhaps better be called simulation; however, the
   analogy with bisimulation in CCS etc. is clear.  Moreover, this notion
   can be extended to typed calculi such as Plotkin's meta-language; once
   powerdomains enter the picture, calling the relation a bisimulation
   becomes fully justified.

   Regards, Samson
-------------------------------
I'd like your draft paper.  I'll wait on the thesis till it's done, but send
it to me then please.

The relation you describe as `simulation' in this deterministic setting
looks to me like Bohm-tree equivalence straightforwardly modified to handle
weak heads forms.  Offhand, I question the rationale for generalizing it to
something like bisimulation in the nondeterministic case---how does
bisimulation arise from nondeterminism and powerdomains?  My
prejudice here comes from my POPL paper on bisimulation: I don't see how to
arrive at bisimulation as the congruence refining equivalence wrt to
observing some primitive computational outcome like (possible and/or
necessary) termination.

Regards, A.