# Impl. correctness for alg. spec.'s

```Date: Fri, 11 Nov 88 11:23:09 cst

Re: John Mitchell's query about the proper definition of
``implementation'':

I agree with Nipkow and Guttag that observational equivalence wins
(see also Sannella and Tarlecki's work).  In fact, I would say that
``correctness = isomorphism'' is indeed a straw man;  I haven't seen
this definition in print for a long time.

I do believe that ``correctness = observational equivalence'' and
``correctness = homomorphism from implementation to final algebra''
are essentially equivalent, at least for *total* algebras.  (I don't
understand Albert's counter-example;  perhaps he could explain it
further.)  Note that both notions depend upon a pre-defined set, or
algebra, of ``observables.''  You can't just look at a set of axioms
and say ``take the final algebra.''

Actually, the two definitions of correctness *are* slightly different,
in this sense: non-reachable algebras may be observationally equivalent
but have no homomorphism.  Of course, the unreachable elements are
not observable at all, even indirectly (they can never occur in
a computation), so this definition of correctness should, technically,
be ``correctness = homomorphism from reachable sub-algebra of
implementation to final algebra.''

Partial implementations are another story.  Suppose algebra C has two
elements {0, 1}, succ is defined thus: succ(0) = succ(1) = 1,
and the only other defined operation is isZero.  There is no
homomorphism from C to Nat, although C is partially observationally
equivalent to Nat.  (I might mention that using axioms to prove
correctness of partial implementations is also problematic, in the
other sense:  an algebra can satisfy the equations in a partial sense
without being partially observationally equivalent to the initial
algebra.)  In this case, logical relations may help.  In Myla Archer's
thesis, she defines ``generalized homomorphism,'' which I believe is
much like logical relations.  Nipkow has similar ideas.

Sam Kamin

```