🚀 go-pugleaf

Upon reading Mitch Wand's JCSS paper "Final Algebra Semantics and Data
Type Extensions" , certain questions arise, and I would be very
grateful if someone can answer them for me, and/or point me to 
relevant literature. 

As I see it, the basic idea of algebraic specification of Abstract
Data Types is two-fold: One specifies a valid class of
implementations, and simultaneously specifies a model.  In the Initial
Algebra approach, the model specified is the initial algebra of the
given set of equations/conditional equations. In the Final Algebra
approach the model specified is the final algebra in the category of
legal implementations.  An implementations (in Wand's paper) is a functor
from some algebraic theory (in the sense of Lawvere) to Sets with
certain conditions imposed.  

The main theorem in the paper is the existence of the Final Object
in the category of implementations K(i) (parameterized by a datatype
extension 'i').  This assures us that specifications will always have
a meaning.  In any specification methodology, the following two
questions are important : How do we check (mechanically or by hand)
whether an implementation meets a specification? How do I reason about
the  model that is the semantics of the specification?

In Wand's approach,  verification of the correctness of the
implementation can be achieved by checking the conditions postulated
of the algebras in K(i).  This is tedious to do by hand.  As for
mechanizing it, can one set up a logic to do the same?

As for the second question, consider the initial algebra approach :
initial algebras of equations cannot, in general, be effectively
axiomatized.  However , an induction principle over constructors (the
constructors must have the property that every ground term is provably
equal to a constructor term) is sound.  In practice, along with the
specifying equations, it is very useful.  Is there some similar logic
for reasoning about Final Algebras?

If the language supporting the datatype has general recursion there
are problems.  Implementations treated as functors into Sets (see
above) are no longer adequate.  One needs to consider Implementations
as functors from algebraic theories to domains.  Does Wand's theorem
carry over? Does anyone have pointers to studies on this and related
questions? 


Ramesh

------------------------------------------------------------------------
Ramesh Subrahmanyam   |  Diplomat: A person who can tell you to go
Computer & Info. Sc.  |            to hell in such a way that you
U. of Pennsylvania    |            would look forward to the trip.