data types and initiality

To: types@theory.LCS.MIT.EDU
Subject: data types and initiality
From: Don Sannella <dts%lfcs.edinburgh.ac.uk@nss.cs.ucl.ac.uk>
Date: Mon, 14 Nov 88 11:20:33 EST
Sender: meyer@theory.LCS.MIT.EDU

Date: Fri, 11 Nov 88 15:11:11 GMT
To: types@theory.LCS.MIT.EDU
Cc: tobias%dash2.lcs.mit.edu@nss.cs.ucl.ac.uk,
        jcm%ra.stanford.edu@nss.cs.ucl.ac.uk
In-Reply-To: Tobias Nipkow's message of Wed, 9 Nov 88 20:49:08 EST <8811100149.AA02880@stork.LCS.MIT.EDU>

This is in response to John Mitchell's message about initial algebras and
Tobias Nipkow's reply.  I agree with what Tobias said, but I want to add a
little clarification.  I also respond to a point in John's message.

1) Clarification: The words "implementation" and "correctness" are used in a
technical way in the algebraic specification community.  This seems to have
led to confusion.

Ehrig/Mahr talks about correctness only, which is to do with whether or not the
initial model of a specification corresponds with some standard one.  Roughly,
a specification is correct wrt a given algebra iff the initial model of that
specification is isomorphic to that algebra.  This means that the specification
is an accurate and complete description of the algebra.  This makes sense if
you are trying to specify something well-known like the natural numbers.

Implementation has to do with programs which realize specifications.  This
is a relation between a specification and either an algebra or a specification,
depending on which paper you read.  This is what Tobias was referring to, and
as he says, there are several possible definitions of precisely what
implementation means.  [An advertisement: see my paper with Andrzej Tarlecki
in Acta Informatica 25, 233-281 (1988) which discusses a general notion of
implementation which subsumes most (maybe all) other definitions.]

2) John suggests that proofs by induction are sound (in some suitable sense)
for algebras which are observably equivalent to the initial model, and only
for such algebras.  This is probably correct, but only if you pick the right
kind of induction, and the right sense of sound.  One problem is that axioms in
the specification might not even be true in algebras which are only observably
equivalent to the initial model.  Another problem is that when you do induction
over a non-observable type, you are using the fact that all the values of that
type are generated by ground terms; this is not the case in some of the
algebras which are only observably equivalent to the initial model.

Don Sannella