🚀 go-pugleaf

In article <1992Dec31.000439.8884@gmuvax2.gmu.edu>, ofut@gmuvax2.gmu.edu (A. Jeff Offutt) writes:
> Generally, are there _known_ fundamental limitations of algebraic
> specifications?  Has anyone studied the "classes" of ADTs that can be
> specified using various specification approaches?  If so, I would
> appreciate a reference (or a short synopsis, if possible).

Some standard references on this topic are:

   J. Thatcher, E. Wagner and J. Wright.  Data type specification:
   parameterization and the power of specification techniques.  ACM Trans. on
   Programming Languages and Systems 4, 711-773 (1982).

   J. Bergstra, M. Broy, J. Tucker and M. Wirsing.  On the power of algebraic
   specifications.  Proc. 1981 Symp. on Mathematical Foundations of Computer
   Science.  Springer LNCS 118, 193-204 (1981).

   J. Bergstra and J. Tucker.  Initial and final algebra semantics: two
   characterization theorems.  SIAM Journal on Computing 12(2), 366-387 (1983).

   J. Bergstra and J. Tucker.  Algebraic specifications of computable and
   semicomputable data types.  Theoretical Computer Science 50, 137-181 (1987).

Briefly, there are different approaches to algebraic specification and
the expressive power of a particular approach depends on whether or not it
offers certain features.  One of the simplest approaches and the most classical
is the so-called "initial algebra approach" via finite lists of equational
axioms as described in:

   H. Ehrig and B. Mahr.  Fundamentals of Algebraic Specification 1. Equations
   and Initial Semantics.  EATCS Monographs on Theoretical Computer Science.
   Springer (1985).

This approach is not powerful enough to specify all recursive data structures
(using "recursive" here in its recursion-theoretic sense).  Allowing hidden
sorts and hidden functions makes this approach powerful enough to describe
exactly all the semicomputable algebras.  Adding so-called "data constraints"
or "hierarchy constraints" (or using a specification language in which the
specification of new types of data cannot side-effect the interpretation of
existing types, e.g. ASL) makes it possible to code universal and existential
quantifiers over the natural numbers and so adds considerable expressive power,
enough to allow the specification of any algebra you are likely to want (for
the details of that vague statement see [BBTW81]).

A paper which explains some of the above and discusses its relevance to
completeness of systems for proving theorems about specifications is:

   D. MacQueen and D. Sannella.  Completeness of proof systems for equational
   specifications.  IEEE Trans. on Software Engineering SE-11(5), 454-461
   (1985).

Of course, all of these expressiveness results are obtained via codings which,
if used in practice, would make specifications difficult (if not impossible)
to read.  Whether or not a particular data type can be *conveniently* specified
is a different question.


Don Sannella
University of Edinburgh