Logic and Semantics Club 06 12 2002
When considering simple programming languages with recursion we can think of recursion constructs as syntactic abbreviations of their infinite expansions. This simplifies the operational semantics on one hand, but on the other hand it means that we have to consider (and provide semantics for) infinite terms, i.e., we have to work with cpos (rather than sets) of terms.
A question arises: what is the right notion of bisimulation for transition systems with cpos as the carriers. In an unpublished work, G. Plotkin argued that the notion based on spans of coalgebras is not sufficient, because even in simple cases the final semantics is not fully abstract with respect to this kind of bisimulation. Instead, he suggested another approach based on topologies of tests.
I will show a relational characterization of the latter notion. It very much resembles the usual Milner's notion of (partial) bisimulation. The result shows that the topological notion indeed seems to be "right".