[Prev][Next][Index][Thread]
EQPARITY
Date: Thu, 17 Nov 88 09:32:29 PST
Item 1. I'm wrong, but the bug is easily fixed.
From: Don Sannella <dts%lfcs.edinburgh.ac.uk@nss.cs.ucl.ac.uk>
To Albert Meyer (EQPARITY example): This does have a final model,
since the two Albert mentions are isomorphic, as observed by Joe
Fasel. I believe the same applies to Vaughan Pratt's examples.
My apologies, Joe and Don are right, at least for the examples we've
seen thus far. In Albert's example I was neglecting the contribution
of the constant ZERO, which has the effect of preventing nontrivial
automorphisms, by forcing the value of ZERO to be a fixpoint of any
automorphism. And in my example I was neglecting the contribution of
INT, which also prevents nontrivial automorphisms but for a more
delicate reason, namely that any homomorphism of heterogeneous algebras
some of whose sorts are fixed should act as the identity on the fixed
sorts.
One might wonder why I make things hard for myself with such
complicated reasoning when Joe and Don's reason is so simple? Well,
take the empty signature and apply their reason to the class of
algebras of cardinality greater than one (i.e. the full subcategory of
Set obtained by deleting the empty set and the singletons). If
anything is final in that class it must be the two-element algebras.
And indeed they are all isomorphic, so they ought to be final. Well
they aren't. One way to see this is that they aren't *uniquely*
isomorphic.
While I don't see for now how to revive my example, Albert's example
can be made to illustrate his point simply by deleting ZERO:NAT from
the signature. The example then becomes
Sorts:
Given: BOOL
Wanted: NAT
Signature:
Given: TRUE,FALSE:BOOL
Wanted: SUC: NAT->NAT
EQPARITY: NAT x NAT->BOOL
Specifications
EQPARITY(x, SUC(SUC(x))) = TRUE
EQPARITY(x, SUC(x)) = FALSE
I think the reasoning is more subtle than people have been giving it
credit for, so it seems worthwhile to spell things out a bit more than
we've been doing.
1. This specification has no model in which NAT is a singleton.
(There may or may not be a model in which NAT is empty, depending on
whether you allow empty algebras; some authors do, some don't. If you
do then the (unique) algebra with empty NAT is initial, though it
obviously can't be final. Either way it doesn't affect the following,
though it does affect my proposed use of penultimate algebras, which
will work for this example only if empty algebras are disallowed.)
2. The specification has a model in which NAT has two values.
3. All models of the specification in which NAT has two values are
isomorphic to each other IN TWO WAYS (i.e. given any models M and N,
not necessarily distinct, there exist exactly two isomorphisms from M
to N).
So this modified example of Albert's does not have final algebras.
Hopefully 1 and 2 should not be controversial. However 3 may bother
people, so let me supply yet further mindnumbing details.
A model of the spec is the heterogeneous algebra
<BOOL,NAT,TRUE,FALSE,SUC,EQPARITY>, with BOOL, TRUE, and FALSE fixed.
Thus BOOL={TRUE,FALSE} (identifying object language and metalanguage as
usual). Let NAT be any two-element algebra, for definiteness take it
to be {0,1} (only to avoid confusing the elements of NAT and BOOL in
the sequel, there need not be any requirement that NAT and BOOL should
be disjoint, though some people may prefer to define things that way
and there is no harm in so doing). Then in any model of this spec
SUC(0)=1, SUC(1)=0, EQPARITY(0,0)=EQPARITY(1,1)=TRUE,
EQPARITY(0,1)=EQPARITY(1,0)=FALSE. This information now determines a
heterogeneous algebra constituting a model of the specified sort, call
it M.
Now let h:M->M be an endomorphism of M, having two components
hB:BOOL->BOOL and hN:NAT->NAT. Since hB is by definition the identity,
h is determined by hN. There are only four possibilities: hN(0) is
either 0 or 1, and likewise for hN(1).
Now suppose hN(0)=hN(1)=0. Then FALSE = hB(FALSE) = hB(EQPARITY(0,1)) =
EQPARITY(hN(0),hN(1)) = EQPARITY(0,0) = TRUE, a contradiction, whence
hN(0) and hN(1) cannot both be 0. Similarly they cannot both be 1.
The identity on M is of course a homomorphism of M.
This leaves just the case hN(0)=1, hN(1)=0, the nontrivial automorphism.
This can be verified to be a homomorphism of M, along the lines of:
hB(EQPARITY(0,1)) = hB(FALSE)
= FALSE
= EQPARITY(1,0)
= EQPARITY(hN(0),hN(1))
hN(SUC(0)) = hN(1)
= 0
= SUC(1)
= SUC(hN(0))
The conclusion is that any two-element model of Albert's spec as
modified has two endomorphisms (which as it happens are automorphisms),
and hence cannot be a final algebra of the class of models of that
spec.
Item 2. Definitions
For the record it might be worthwhile defining exactly which category
we're in. One morphism can ruin your whole limit. Here's my
understanding of which category we're measuring finality in.
Objects: those heterogeneous algebras of the given signature satisfying
the given theory (equational in the examples we've been considering),
*with the imported sorts being held constant*. (We might be in
disagreement on this last point, but the only alternative to this that
I'm aware of is to drop that restriction altogether, in which case the
final algebra of an equational theory will have all sorts singletons,
which is clearly not what we've been talking about.)
(Another seemingly minor point to disagree on is whether empty sorts
are permitted, an issue only in the absence of constants (zeroary
operations). Some universal algebra texts, e.g. MMT
(McKenzie-McNulty-Taylor) disallow them, others don't. My usual
preference is to allow them on the ground of the more colimits the
merrier, though this has the unfortunate side effect of spoiling my
penultimate-algebra idea in examples such as the above.)
Morphisms: all homomorphisms between those algebras, such that the
imported components of each homomorphism are identity maps. (For n
sorts a homomorphism consists of n maps, one per sort. If m of the n
sorts are imported then m of the n components of the homomorphism must
be identity maps.)
Item 3. Another bug of mine.
While I'm retracting things, let me retract my
>It seems to be open for
>countable algebras in general, but (unless I've misinterpreted
>something) it does hold between any two algebras when one of the two
>epimorphisms between them is of finite index...
My caveat was appropriate, I had indeed misinterpreted something.
Walt Taylor supplied a straightforward counterexample of two countable
nonisomorphic algebras with an epimorphism between them in each
direction, which can be expressed cryptically as (112)^omega and
(121)^omega, or less cryptically thus:
>From: Walter Taylor <wtaylor@boulder.Colorado.EDU>
>Consider lattices L_1 and L_2 that are drawn as follows:
>
> . .
> . .
> . .
>
> o o
> / \ |
> o o o
> A: \ / B: / \
> o o o
> | \ /
> o o
> / \ |
> o o o
> \ / / \
> o o o
> | \ /
> o o
>
>(The little o's denote lattice elements. The three periods at the top
>of each figure indicate that the pattern continues upwards, alternating
>2's and 2x2's.) Same pattern, except they terminate differently at
>the ground floor. Now you can easily get a homomorphism f:A --->> B
>by collapsing the bottom two elements. You get a homormorpism g:B --->> A
>by collapsing the bottom four elements of B. Clearly each homomorphism
>has index <= 4.
>-----------------------------
This counterexample shows that it is possible to have a pair of
nonisomorphic countable algebras, e.g. the above two lattices, and
a pair of epimorphisms between them. So the question for the countable
case is not open after all, and the counterexample even covers the case
of finite index.
While this doesn't constitute a counterexample to my conjecture that
penultimate algebras are final in any class of models of an algebraic
specification, it does shake my confidence in the conjecture
considerably.
======================================
From: jhf%chaco@lanl.gov (Joe Fasel)
By the way, either I'm confused, or the equations above aren't the
whole story, since EQPARITY in the implementation relates every pair of
NATS, but the equations don't yield TRUE or FALSE for terms like
EQPARITY(ZERO, SUC(SUC(SUC(ZERO)))).
Not in an arbitrary model of Albert's spec, but it does hold in any
two-element model, which I think are the ones Albert had in mind as
being "close to final."
-v