ADTs - In reply to Albert's note

To: types@theory.LCS.MIT.EDU
Subject: ADTs - In reply to Albert's note
From: meyer@theory.LCS.MIT.EDU
Date: Thu, 10 Nov 88 12:26:18 EST
Sender: meyer@theory.LCS.MIT.EDU

Date: Thu, 10 Nov 88 11:50:37 EST
To: tobias@dash2.lcs.mit.edu
In-reply-to: Tobias Nipkow's message of Thu, 10 Nov 88 11:42:32 EST <8811101642.AA02508@dash2.LCS.MIT.EDU>

   Date: Thu, 10 Nov 88 11:42:32 EST
   From: tobias@dash2.lcs.mit.edu (Tobias Nipkow)

   Your note makes sense but I disagree on one point: Even if equality is
   part of the signature (which is not the usual point of view), you can have
   non-isomorphic models of the spec which are observationally equivalent.
   The reason is that now you can implement equality by something which is
   not really the equality on the algebra but just a congruence. The
   specification of sets can be implemented by lists with a suitable equality
   function defined on them.

   Tobias

--------------------
Yes, but then equality is not part of the signature of the implementing
algebra, only the binary relation symbol for equivalence.  This is perfectly
ok, of course, but suggests that there is something inconsistent about
including equality in the signature.  If one does not, then the decision to
define implementation as meaning ``has the initial model as a homomorphic
image'' starts to seem more arbitrary.

Regards, A.