ramesh@saul.cis.upenn.edu (Ramesh Subrahmanyam) (06/09/91)
Upon reading Mitch Wand's paper "Final Algebra Semantics and Data Type Extensions" (JCSS 1979), certain questions arise, and I would be very grateful if someone can answer them for me, and/or point me to the right sources. 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 implementation (in Wand's paper) is a functor from some algebraic theory (in the sense of Lawvere) to Sets. The main theorem in Wand's 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 the category of domains (or some such category for modelling the types of a programming language). 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.