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

data types and initiality



Date: Wed, 9 Nov 88 10:27:32 PDT
Cc: bhoward@polya.lcs.mit.edu, eswolf@polya.lcs.mit.edu

In preparing a lecture about algebraic data types,
I came across the claim (in several places, including the
book by Ehrig and Mahr) that a "correct" implementation
of a specification is any algebra that is isomorphic
to the initial algebra. While I am willing to believe that
the initial algebra is OK, this seems unreasonably
restrictive. I would propose, at the very least,
that anything observably equivalent to the initial
algebra is OK. In fact, this seems like a reasonable
definition of acceptable, since one could claim that
proofs by induction are sound (in some suitable sense)
even for these non-initial algebras, and should
fail otherwise. 

Does anyone want to argue in favor of this "standard"
point of view? Do you know anyone else who really 
believes this, or am I just attacking a straw man?

John Mitchell