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

Wand on final algebra semantics

In-Reply-To: Your message of Fri, 18 Nov 88 12:16:27 EST.
	     <8811181716.AA01035@stork.LCS.MIT.EDU>
Date: 20 Nov 88 23:26:49 PST (Sun)

	From: thatte%cs@ucsd.edu (Satish Thatte)
	I thought that for final algebras, one usually restricted attention
	to the class of *reachable* algebras.

Wand indeed does just this in the paper you cite.  With a title of
"Final Algebra Semantics" it would seem to be must reading for the
present discussion.  A few words about it here should therefore be in
order.  T0, T1 etc. refer to equational theories of the kind we've been
discussing.

Wand's main theorem is that every standard conservative extension has a
maximal base-conservative augment.

		     i       j
		T0>>---->T1----->>T2		>>-  =  standard conservative
		  >>------------->		->>  =  maximal augment
			 j;i

By a conservative extension i:T0->T1 I mean here one in which any
identity of T1 between terms of T0 is an identity of T0.  An augment
j:T1->T2 is a signature-preserving extension: it can only identify (add
equations between) existing terms, it cannot create new terms.  A
base-conservative extension of an extension T0->T1 is an extension of
T1 which conservatively extends the base T0 (the composition j;i in the
diagram).  By maximal augment of a given kind we mean one that includes
every augment of that kind; equivalently, the union of all augments of
that kind.  I'll call T1 a *standard* extension of T0 when T1
identifies every T0-sorted ground term of T1 with a ground term of T0.
(Clearly if T1 standardly extends T0 so does T2.  In this case the
restriction to T0 of the initial algebra of T2 *is* the initial algebra
of T0, as opposed to being just an extension of it.  That is, without
standardness "nonstandard" individuals of old sorts may show up in T2's
initial algebra.)

I'm not entirely sure, but it seems to me it ought to be possible to
drop "standard" from the theorem.  Counterexample, anyone?

The interest in the theorem is that it provides an alternative
representation of T2.  As an example Wand takes for T0 a theory of
natural numbers and for T2 a theory of arrays which would seem to be
better represented by a certain simple subtheory T1 of T2 along the
above lines than by an explicit axiomatization.

So what does all this have to do with final algebra semantics?  Well,
Wand exhibits a category whose final algebra turns out to be the
initial algebra of T2.  The category consists of those models of T1
which have no proper subalgebras (are "reachable") and whose
restriction to the signature of T0 is the initial algebra of T0.  (The
proof that the category has a final algebra involves the construction
of T2 along the way.)

Presumably the point of this final algebra approach is that it is very
convenient to be able to nail down a wanted algebra as simply the final
algebra of some category.  However when you add in the description of
the category itself the cost approximates that of the noncategorical
account of the real problem being solved (assuming equally fluency with
algebraic theories and old-fashioned equational logic).

So while I think Wand's application of final algebras gives one
reasonable if not clearly preferable way to define the maximal
base-conservative augment of a conservative extension, I don't think we
should regard it as the only possible application of the general notion
of final algebra.  And for other applications of the notion we should
not feel obliged to retain all of Wand's criteria for membership in the
category in which we are computing finality.  For each such criterion,
don't ask whether it was used before but only whether you need it for
your application.

	Leaving the second equation out destroys the example because it
	now has no final algebra (VAL(1,EMPTY) can be any natural
	number in a model).

My explanation above makes clear the effect of leaving out the second
equation.  With it in, the extension of the theory T0 of natural
numbers to the theory T1 of arrays is standard.  Without it we still
have a T2 (if I'm right) but it lets in VAL(1,EMPTY) as a nonstandard
natural number in the initial algebra of T2 = final algebra of Wand's
category.

If we add to Wand's conditions for membership in his category the
requirement that its objects contain no nonstandard elements (a
stronger condition than his requirement that the restriction to T0 be
the initial algebra of T0, since restriction throws out the nonstandard
elements) this makes your example work as you intended:  there is now
no final algebra in the resulting smaller category.

The essence of your example lies in:

Sorts
	Given:	A
	Wanted:	B
Signatures
	Given:	X,Y:A
	Wanted:	Z:B
		F:B->A
Equations
	none

Here A = {X,Y} in the initial algebra of the given theory T0, but in
that of the wanted theory T2 it becomes {X,Y,F(Z)}.

Aside from its role in Wand's theorem, are you sure you want the
no-proper-subalgebras condition?  One justification for it is that
unreachable elements must be unobservable and so unwanted.  However as
Tobias Nipkow observed in an earlier message, observability is a
function of language.  In particular elements unreachable by equational
observers are not unreachable by first-order observers, whose
quantifiers can reach all elements.

The bottom line for me is that I have found *all* of the examples to date
to be enlightening.  That some fail some criteria merely adds to the
enlightenment.
-v