data types and initiality

To: types@theory.LCS.MIT.EDU
Subject: data types and initiality
From: meyer@theory.LCS.MIT.EDU
Date: Thu, 10 Nov 88 12:21:48 EST
Sender: meyer@theory.LCS.MIT.EDU

Date: Thu, 10 Nov 88 06:23:28 EST
To: jcm@ra.stanford.edu
In-reply-to: John Mitchell's message of Wed, 9 Nov 88 17:46:55 EST <8811092246.AA02684@stork.LCS.MIT.EDU>
cc: riecke, lalita, bard, tobias@dash2

Taking the ``observational equivalence'' perspective on correct
implementations of abstract data types seems more in the spirit of FINAL,
rather than initial, algebra interpretations.  The issue hinges on whether
equality is to be taken as part of the signatures of the specifying and
implementing algebras.  If it is, then isomorphism and observational
congruence will coincide.  If it isn't, then observational congruence to the
spec algebra will reduce to having the FINAL algebra as a ``homomorphic''
image, viz., every algebra in the variety is an implementation.

Since it's the middle of the night, or was when I started composing this
note, I hope you'll forgive me for being cryptic.  Let me know if the above
makes any sense to you.  I'll hold off cc'ing TYPES till I hear from you.

Regards, A.