Implementation. correctness etc

To: types@theory.LCS.MIT.EDU
Subject: Implementation. correctness etc
From: Carolyn Talcott <CLT@sail.stanford.edu>
Date: Sat, 12 Nov 88 21:26:54 EST
Sender: meyer@theory.LCS.MIT.EDU

Date: 12 Nov 88  1542 PST

A few remarks inspiered by the recent discussion of implementation correctness.

()  I too am confused by Meyer's counter-example.  Doesn't one
usually take the carriers of different sorts to be disjoint?
At least an isomorphism is a family of maps indexed by the sorts
and the isomorphism on BOOL need not be the same as that on NAT.
Thus the maps {h_BOOL, h_NAT} where h_BOOL is the identity and
h_NAT interchanges TRUE and FALSE constitute an isomorphism between
the two algebras.

() I agree that observational equivalence is an important notion
(logical relations too, tho I have less experience with them).  
There seem to be two notions of `observational equivalence':
  (a) two terms or elements of a model being `observational equivalence'
      or indistinguishable in some set of contexts.
  (b) two models/algebras being `observational equivalence'
      i.e. agreeing in their interpretation of some set of sentences
        in a common language.
Has anyone considered the following questions?
   (i) under what conditions / in what sense do these notions agree. 
  (ii) for what purposes is one notion more useful than the other.
In either case, it seems to me that the set of observations needs to 
be made explicit (Sannella and Tarlecki do this)  and we need
to understand the relations of equivalences induced by different
sets of observations. (Algebras of observations?)

() Regarding recursion --  Broy, Pepper, and Wirsing (TOPLAS 1987) propose
methods for using partial algebras for programming language semantics.
They treat recursive definition in the spec language by considering the 
class of minimally defined models.   They seem to find initial and
final models and observational equivalence all to be relevant notions
useful in appropriate places.