Re: initial algebras

To: types@theory.LCS.MIT.EDU
Subject: Re: initial algebras
From: John Mitchell <jcm@ra.stanford.edu>
Date: Thu, 10 Nov 88 17:11:53 EST
Sender: meyer@theory.LCS.MIT.EDU
Date: Thu, 10 Nov 88 15:39:00 EST
From: tobias@dash2.lcs.mit.edu (Tobias Nipkow)
To: jcm@ra.stanford.edu
Subject: initial algebras

> What I had in mind was that an implementation is "correct"
> iff it is observationally equivalent to the initial algebra
> iff there is a partial homomorphism from the implementation
> to the initial algebra iff the initial algebra is a partial
> quotient.  This allows implementations which
> do not even satisfy the equational axioms. For example,
> pop(push(x,stack)) = stack might fail, since pushing and
> popping might have some invisible side effect. However,
> the spec will hold if we interpret = on the type as meaning
> observationally equivalent. As far as I can tell so far,
> this isn't a standard idea. On the other hand, it isn't
> really that far off the beaten path either.
> 
> John

Two remarks. I don't see the "iff" between observational equivalence and the
existence of partial homomorphisms: the initial model of John Guttag's
axiomatization of sets consisting only of the two equations for "in" are
lists. However, both sets and multisets are observationally equivalent to
those lists since the only observer is membership. Either you have to put
some additional constraints on the specification (e.g. that it's initial
model must be fully abstract in a suitable sense), or you should relax
homomorphism to logical relation.

The idea of a (partial) homomorphism from implementation to specification is
fairly standard. One of the earliest references is Hoare's "Proof of
Correctness of Data Representations", although he didn't phrase it in terms
of initial algebras and observational equivalence.

Tobias
----------------------------------------------------------------
Date: Thu, 10 Nov 88 13:39:51 PDT
From: John Mitchell <jcm@ra.stanford.edu>
To: tobias@dash2.lcs.mit.edu

Thanks for the reply. I have been having mail problems:
please reply to jcm@polya.stanford.edu, or simply
jcm@cs.stanford.edu.

You are right. I should have said logical relation
instead of partial homomorphism.  So the picture is

An implementation is "correct"
  iff it is observationally equivalent to the initial algebra
  iff there is a logical relation between the implementation
      and the initial algebra 
  iff some collapsing of the initial algebra is a partial quotient
Perhaps this leads to the final algebra, as Albert suggests.

This view allows implementations which do not satisfy the equational 
axioms. As I mentioned to you before (but not to others on the cc list)
   pop(push(x,stack)) = stack 
might fail, if pushing and popping have some invisible effect on the
way a stack is represented. (Think of stacks that maintain an inaccessible
record of their history, to pick a crude example.)

Does this sound like an accepted point of view, or something 
worth arguing about at some point? I suppose it might
not be so obvious what "observational equivalence" means. For
example, what is the connection between "observing" using algebraic
expressions or typed programs with recursion? 

This brings me to another question. With recursion around, the
initial algebra ought to be the initial object in some category
of domains. This never seems to be mentioned at all, in any
of the work on initial algebras. Is there an accepted position on
this that I should know about? 

Thanks for all of your comments.