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

data types and initiality



   Date: Thu, 10 Nov 88 11:45:29 PDT
   From: John Mitchell <jcm@ra.stanford.edu>

   What I had in mind was that an implementation is "correct"
   iff it is observationally equivalent to the initial algebra
   iff there is a partial homomorphism from the implementation
   to the initial algebra iff the initial algebra is a partial
   quotient.  This allows implementations which
   do not even satisfy the equational axioms. For example,
   pop(push(x,stack)) = stack might fail, since pushing and
   popping might have some invisible side effect. However,
   the spec will hold if we interpret = on the type as meaning
   observationally equivalent. As far as I can tell so far,
   this isn't a standard idea. On the other hand, it isn't
   really that far off the beaten path either. 

   John

---------------
I understand wanting to interpret equality as obs-cong, but then it seems to
me the implementation might BE a homomorphic image of the initial algebra
rather than vice-versa.

For example, suppose we have two sorts called INT and BOOL,the signature
		      TRUE, FALSE:BOOL
			     ZERO:NAT
    		     	      SUC:NAT-->NAT
			 EQPARITY:NAT x NAT-->BOOL
with specifying equations
		     EQPARITY(x, SUC(SUC(x))) = TRUE
			  EQPARITY(x, SUC(x)) = FALSE.

Now assume the only observables are TRUE and FALSE.  Then the initial algebra
has NAT = the natural numbers under succcessor.  But an ``implementation''
which is obs-cong to this initial algebra has NAT={TRUE, FALSE},
SUC=complement, and EQPARITY = equivalence.

Note by the way, that the implementation can interpret ZERO to be TRUE or
FALSE; there is no final algebra in this case.  So the obs-cong approach is
not EXACTLY asking for final algebras--close though.

Regards, A.