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

data types and initiality

Date: Sat, 12 Nov 88 01:14:25 PST
To: meyer@theory.LCS.MIT.EDU

Albert's EQPARITY example is an instance of the general observation
that any algebra A with a nontrivial endomorphism h can be neither
initial nor final, since then A would have two homomorphisms both from
and to A, namely h and the identity on A.

An advantage of this method of demonstrating non-initiality or
non-finality is its robustness, in that it makes no assumptions
whatsoever about the class of algebras in which we are looking for
initial objects, other than that A belong to it.  In Albert's example
the endomorphism is an automorphism, so in equipping the class with
morphisms to make it a category, most restrictions on what morphisms to
allow between algebras of the class, such as only surjective or
injective homomorphisms, or even only isomorphisms, do not affect the
example, making it even more robust.

An example of this phenomenon arising in nature is provided by the
group of integers, which has negation as a nontrivial automorphism.
Hence <Z,+,-,0> is neither initial nor final and hence has neither an
initial or a final algebra specification.

Nevertheless a "close-to-final" algebra specification of <Z,+,-,0> is
possible, by a specification which, as with Albert's EQPARITY example,
has no final algebra but has <Z,+,-,0> as the closest we can get to
final (I don't have a formal definition either).  We take <N,+,0>, the
natural numbers, as the given sort, playing the same role as the sort
{TRUE, FALSE} in the EQPARITY example.

Sorts:
	Given:	N (natnums)
	Wanted:	Z (integers)
Signatures:
	Given:	NZERO: N	NPLUS: NxN->N
	Wanted:	ZPLUS: ZxZ->Z	NEG:   Z->Z	ZZERO: Z
		INT:   N->Z	ABS:   Z->N
Specifying equations:
		ABS(INT(n)) = n				(1)
		ZZERO = INT(NZERO)			(2)
		ZPLUS(INT(m),INT(n)) = INT(NPLUS(m,n))	(3)
		ZPLUS(i,NEG(i)) = ZZERO			(4)
		ABS(i) = ABS(NEG(i))			(5)

Equation (1) forces INT to be injective, while (2)-(3) make the
range-of-INT part of <Z,+,0> isomorphic to <N,+,0>.  Equation (4) (the
group axiom) ensures inter alia that NEG(INT(n)) is not in the range of
INT for n nonzero (taking advantage of NPLUS, given).  (5) nails down
ABS for the sake of definiteness.  Either of (4) or (5) suffices to
make NEG injective on the range of INT.  (1)-(5) should then suffice to
make the "close-to-final" models of this specification isomorphic to
<Z,+,-,0>.  But they can't be final because of the nontrivial
automorphism of <Z,+,-,0>.

On the other hand this group happens to be the free group on one
generator.  So by including the generator in the signature we obtain the
initial algebra <Z,+,-,0,1>.

OR, we can expand the above specification with NONE: N (that is, the
natnum 1, given), ZONE: N, ZONE=INT(NONE).  It should then turn out
that <Z,+,-,0,1> is the (up to isomorphism) final algebra of the class
of models of this specification.  So we have both an initial and a
final algebra specification of the integers, the former standing alone,
the latter helped along with the natural numbers.  (In a purely
equational system of this kind, any final algebra would be trivial
without some such help.)

This shows just how sensitive to signature this sort of thing can be.
Merely adjoining the constant 1 made possible both an initial and a
final algebra specification, which we had shown was not possible without
the 1.

As a side remark, since <Z,+,-,0,1> is also the free *abelian* group on
one generator we have here another example (besides the usual ones
involving induction) of initiality contributing to the equational
theory, in this case contributing the equation xy=yx.
-v