[Prev][Next][Index][Thread]

Re: initiality, etc.

Date: Wed, 16 Nov 88 13:35:28 GMT

Forgive the slowness of my response to this debate; mail on the machine I use
was broken for 5 days.  I have short comments on some of the messages which
did reach me.

To Satish Thatte (the initial method is universally applicable and the final
method only works under certain assumptions):  If one is interested in initial
*extensions* of existing models, then the same problem arises with initial
models.  I can provide an example if required. The "pure" initial algebra
approach doesn't have this problem because it doesn't support hierarchical
specification and so although you always get an initial model it is probably
not the model you want.

To John Guttag ("I think that purely algebraic specifications are probably a
bad idea anyway"): I emphatically agree, if "algebraic" means equational or
say conditional equational.  If you discard the initial/final dogma, there
is no reason to limit yourself to such an inexpressive logic.  Andrzej Tarlecki
and I (mis)use the term "algebraic specification" to mean a specification
containing axioms (not necessarily equations) which describes a class of
algebra-like structures.  To anybody interested in why this is a far more
interesting and useful concept than boring old initial models of lists of
equations: I would be happy to explain or refer you to appropriate papers.

To John Mitchell ("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."):  See Reichel's book "Initial Computability, Algebraic
Specifications and Partial Algebras" (Oxford Univ. Press 1987).  There is also
a recent paper by Nivela and Orejas of Barcelona on this topic (Springer
LNCS Vol 332).

To Albert Meyer (EQPARITY example):  This does have a final model, since the
two Albert mentions are isomorphic, as observed by Joe Fasel.  I believe the
same applies to Vaughan Pratt's examples.

To Carolyn Talcott (Has anyone considered the relationship between
observational equivalence on the element level and on the algebra level?):
See Reichel's book.  Unfortunately, Reichel's approach is complicated enough
that the ideas are hard to see.

To John Mitchell
1. ("... logical relations and obs-cong are the important notions, and all the
dogmatic initial-final-loose algebraic interpretation arguments irrelevant."):
Yes, with the change irrelevant => secondary.
2. ("I was trying to decide whether I should encourage a student to look into
this"): Definitely yes; there is an obvious connection between these two
schools and I think the only reason why the link has not been made is that
hardly anybody knows enough about current work in both camps.

-- Don

P.S. I already mentioned my paper with Andrzej Tarlecki on observational
equivalence in a previous message which discusses many of these issues.  See
also our paper in Information and Computation 76, 165-210 (1988) which includes
some arguments against initiality (section 4.3).