Observational equiv.

• To: types@theory.LCS.MIT.EDU
• Subject: Observational equiv.
• From: guttag@larch.lcs.mit.edu (John Guttag)
• Date: Thu, 10 Nov 88 12:24:04 EST
• Sender: meyer@theory.LCS.MIT.EDU

Date: Thu, 10 Nov 88 08:57:51 est
To: guttag@theory.LCS.MIT.EDU, jcm%ra.stanford.edu@xx.lcs.mit.edu,
        meyer%theory.lcs.mit.edu@xx.lcs.mit.edu, tobias@theory.LCS.MIT.EDU

John,

This dispute dates to the mid 70's.  The ADJ group (Goguen, Thatcher,
Wagner and Wright) and Zilles argued in favor of the initial algebra
viewpoint.  I argued in favor of the observational view in my thesis and
in articles based on it.

The following specification of sets illustrates the issues nicely:

    empty: -> Set
    insert: Elem, Set -> Set
    in: Elem, Set -> Bool

    in(e, empty) == false
    in(e, insert(e1, s)) == (e=e1) | in(e, s)

If one insists on isomorphism to the initial algebra one is restricted to
implementations that preserve the order of insertion.  If one wants to allow
an implementation in which it is not preserved, one must add an axiom:

    insert(e, insert(e1, s)) == insert(e1, insert(e1, s))

By this time most people who have thought seriously about the issue have come
done on the observational equivalence side.  Of course, this still leaves
room to debate the the precise definition of observational equivalence.

Personally, I think that purely algebraic specifications are probably a bad
idea anyway.

John

• Prev: data types and initiality
• Next: ADTs - In reply to Albert's note
• Index(es):
  • Main
  • Thread