[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.