[Prev][Next][Index][Thread]
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