Re: free algebras in ASD

Re: free algebras in ASD

[Paul Taylor]

Toby Bartels and I have been discussing the relationship
between
     1-categorical ideas such as free algebras and cofree coalgebras
and
     2-level ideas such as overt discrete and compact Hausdorff.

It does seem to me to be a good question to ask why these relationships
hold, and why they break down.   Such questions arise in traditional
formulations of topology, in which other people may have some intuition.

I observed that
      N   is   overt    discrete    Hausdorff      not compact
    2^N   is   compact  Hausdorff   not discrete   overt
which Toby attributed to the fact that N is the free algebra for +1
whereas 2^N is the cofree coalgebra for a functor that is not directly
analogous.

I don't think the particular functors are very important, as (some of)
these properties hold of free algebras and cofree coalgebras in general.

So, a free algebra is
  - overt       because we can enumerate its (raw) terms,
  - discrete    because we can enumerate (proofs of) its equations,
  - not compact because there are infinitely many raw terms.

I don't have much experience of cofree coalgebras, but those that
do could probably formulate a similar argument for why they are
compact and Hausdorff.

N is peculiar in being Hausdorff (ie it has decidable equality).
This is because its theory is very simple.   Other free algebras
(my usual example is "combinatory algebra", with S and K) do not
have decidable equality.  Likewise, cofree coalgebras are not
discrete.

***** Why is Cantor space overt?
***** Do other cofree coalgebras have this property?

That would explain these particular failures of symmetry, but

***** Why does this relationship between the 1- and 2-level ideas
***** hold, and why is it this way round?

ASD might make things clearer here.   Its 1-level theory, like that
of an elementary topos, is not self-dual.   Toby observed that the
symmetry between free algebras and cofree coalgebras is only partial.
The ideas have long been well known in category theory, alhough,
if you go through the exactness properties of a pretopos, several
of them do actually hold for the dual category too.

The 2-level theory in ASD is quite interesting before we introduce
the axioms that break the duality.   These are:
- N is overt but not compact
- Scott continuity.

As I mentioned before, I tried a bit to develop things with dual ideas,
in particular starting from Cantor space instead of N.   I suspect that
there is a dual formulation of Scott continuity, although I couldn't
see what it is.  So I don't think that that's where the asymmetry lies.

I suspect that the symmetry is broken by the "convention" that
- N is overt but not compact
ie it has a quantifier, and we ("arbitrarily") call this "existential".

Paul Taylor

Re: free algebras in ASD

[Vaughan Pratt]

Paul Taylor wrote:
> I observed that
>      N   is   overt    discrete    Hausdorff      not compact
>    2^N   is   compact  Hausdorff   not discrete   overt
> which Toby attributed to the fact that N is the free algebra for +1
> whereas 2^N is the cofree coalgebra for a functor that is not directly
> analogous.

As Toby noted, the functor is x2.  However it is more than merely
analogous, it is the dual of +1 when 2 is taken to be the dual of 1 (as
with the original Stone duality for Boolean algebras, more generally
distributive lattices, more generally yet Chu(Set,2)), product of course
being the dual of sum.

> ASD might make things clearer here.   Its 1-level theory, like that
> of an elementary topos, is not self-dual.

By "1-level" do you mean first order?  *-autonomous categories
constitute a natural elementary notion of abstract Stone duality that is
self-dual.  What advantage of the elementary fragment of ASD over
*-autonomous categories justifies its failure of duality?  And how does
the *-autonomous abstraction of Stone duality relate to ASD's
abstraction of it?

Toby Bartels wrote:
> Perhaps the asymmetry is simply between initial algebras and final colagebras.
> One is a colimit and the other is a limit;
> there are already several asymmetries between these,
> such as that products distribute over sums but not vice versa.
> Indeed, if final coalgebras preserve "some"s,
> this might be more than just a bad pun.

In general 2 is not the dual of 1.  In order to exhibit a duality
between N and 2^N, they should be defined in a self-dual category that
does make 2 the dual of 1.  The most general such that I'm aware of is
Chu(Set,2) --- Chu(Set,3) embeds Chu(Set,2) (in 3x2 = 6 ways) but it
makes 3 the dual of 1.  If you know of another category that makes 2 the
dual of 1 that does not embed in Chu(Set,2) I'm all ears.  In situations
where 2 is not the dual of 1 it's not clear to me why one should expect
2^N to turn out to be dual to N in a way where all properties of one
have their dual counterpart of the other; in Chu(Set,K) the natural
functor for a final coalgebra dual to N is FX = XxK.

In the context of duality the way to think about X in a Chu space
(A,X,r) is that it is the dual of A, with the relation r characterizing
  the particular duality: the dual of (A,X,r) is (X,A,r^) where r^ is
the converse of r.  The first component constitutes the underlying set
while the second can be thought of as a generalized frame of open sets,
generalized by dispensing with the traditional frame operations of
finite meets and arbitrary sups, with r simply the binary relation of
membership of points in open sets.

For this reason, absent alternatives to Chu(Set,2) there is no
alternative to taking 1 to be the Chu space (1,2) if you want 2 to turn
out to be the dual of 1.  Note that in doing so 2 becomes the Chu space
(2,1), the coarsest possible consistent topology on 2 (thinking of (2,0)
as inconsistent).  It should be distinguished from discrete 2 = 1+1,
which is (2,4).

Taking 1 in Chu(Set,2) to be the discrete Chu space (1,2), the initial
algebra for +1 is (1,2) + (1,2) + ... = (N,2^N), 2^N being the power set
of N, a complete atomic Boolean algebra.  The final coalgebra for x2
when 2 = (2,1), as the dual of the initial algebra for +1, is the dual
of (N,2^N), namely (2^N,N).

Back to Paul:
 > The symmetry between
 >      =>  T  /\   =    some   overt    discrete   free     algebra
 > and  <=  F  \/   !=   all   compact   Hausdorff  cofree   coalgebra
 > is very strong in this, but not perfect, because
 >      N   is   overt    discrete    Hausdorff      not compact
 >    2^N   is   compact  Hausdorff   not discrete   overt
 > I have not managed to isolate convincingly the precise point where
 > the symmetry breaks down.

If ASD makes 2 the dual of 1 then it's suspiciously non-abstract.  The
only framework I know of for analyzing this duality is Chu(Set,K) for K
= 2.  Any larger K doesn't work, the concreteness of Chu(Set,3) etc.
notwithstanding, unless you set things up so that the final coalgebra of
the functor XxK is independent of the cardinality of K (which can be
done as Bill Lawvere noted long ago, making 3^N equivalent to 2^N, but
I'd be very impressed if ASD incorporated Bill's machinery).

In Chu(Set,2), if one takes X in (A,X,r) to be the open sets, with
r(a,x) membership of a in x, then (N,2^N,r) is discrete (the discrete
Chu spaces over 2 being those of the form (A,2^A,r)), Hausdorff (by
discreteness), not compact (because infinite and discrete), and overt
(because spatial, Elephant C3.1.16).

There are two ways of computing which of these four properties
(2^N,N,r^) has, depending on whether one applies the elementary
definitions of the properties to the "chupology" (taking r^ to be the
converse of membership, i.e. a subset of N can "belong" to an element of
N), or organizes 2^N as a topological Boolean algebra with the (Stone)
topology serving to make it a CABA so that the continuous ultrafilters
are all and only the elements of N, in order for the duality to work.
Here are the two ways, alongside what Paul claims for comparison.

Chupology   not compact   not Hausdorff   not discrete  ?~?overt?
Stone          compact       Hausdorff    not discrete  overt
Paul           compact       Hausdorff    not discrete  overt

(The chupology is not compact because the whole space is not open, in
fact {} is not "in" any natural number.  It is not Hausdorff because no
two opens are disjoint to begin with.  And it's obviously not discrete.
  However unless there's a definition of "overt" meaningful for all
chupologies I don't know what "overt" would mean for chupologies whose
open sets don't form frames---they do in (N,2^N) but not in (2^N,N).)

Interestingly we have perfect agreement between the usual Stone topology
one imposes on a Boolean algebra to make it a CABA (to make the duality
work) and the topology Paul has in mind for 2^N.  Paul, is this because
you have in mind the Stone topology, with 2^N obviously being spatial
hence overt, or for some other reason?

If the former then that is the "precise point where the symmetry breaks
down:"  you don't take the precise dual of this when dualizing back to
(N,2^N), which you leave instead as the original Chu space (N,2^N).
This is a perfectly fine discrete, Hausdorff, overt, but not compact
space, again in perfect agreement with you.  However comparing it with
the topology of a topological Boolean algebra is apples to oranges.

If the latter however then I have no explanation and the ball is back in
your court.

Vaughan Pratt

Re: free algebras in ASD

[Toby Bartels]

Paul Taylor wrote in part:

>Toby Bartels asked me:

>>My intuition is that polynomials with overt discrete coefficients
>>should have overt discrete initial algebras,
>>while those with compact Hausdorff coefficients
>>should have compact Hausdorff final coalgebras.
>>Have you any thoughts about that question?

>In fact, what I have to say about this (in the setting of the
>existing established theory for locally compact spaces) is little
>more than Toby's "intuition".  The existence of these spaces
>would follow from the limit--colimit coincidence, which is sketched
>in Remark 10.16 of
>    "Geometric and higher-order logic in ASD"
>    www.PaulTaylor.EU/ASD/loccpct#geohol

Yes, there it is!  That's what I get for not reading them in order.  (^_^)

>The symmetry between
>     =>  T  /\   =    some   overt    discrete   free     algebra
>and  <=  F  \/   !=   all   compact   Hausdorff  cofree   coalgebra
>is very strong in this, but not perfect, because
>     N   is   overt    discrete    Hausdorff      not compact
>   2^N   is   compact  Hausdorff   not discrete   overt
>I have not managed to isolate convincingly the precise point where
>the symmetry breaks down.

I was about to say that this comparison is not really fair,
since N is the initial algebra of X |-> X + 1,
while 2^N is the final coalgebra of X |-> 2 x X,
but I guess that the final coalgebra of X |-> X + 1
is also overt but not discrete.

Perhaps the asymmetry is simply between initial algebras and final colagebras.
One is a colimit and the other is a limit;
there are already several asymmetries between these,
such as that products distribute over sums but not vice versa.
Indeed, if final coalgebras preserve "some"s,
this might be more than just a bad pun.


--Toby

free algebras in ASD

[Paul Taylor]

During the discussion on Dedekind vs Cauchy reals, Toby Bartels asked me

> to what extent does ASD have inductive and coinductive objects;
> in other words: to what extent do polynomial functors have
> initial algebras and final (terminal) coalgebras?
>
> Of course, N is put in by hand as the initial algebra of X |-> 1 + X.
>
> And I know that you've constructed Cantor space as 2^N  (through
> a bit of argument since exponentials don't always exist) and the
> proof that this is the final coalgebra of X |-> 2 x X goes through.
>
> But the final coalgebra of X |-> N x X would be Baire space,
> which is not locally compact, so we don't expect that to work.
>
> My intuition is that polynomials with overt discrete coefficients
> should have overt discrete initial algebras,
> while those with compact Hausdorff coefficients
> should have compact Hausdorff final coalgebras.
> Have you any thoughts about that question?

In fact, what I have to say about this (in the setting of the
existing established theory for locally compact spaces) is little
more than Toby's "intuition".  The existence of these spaces
would follow from the limit--colimit coincidence, which is sketched
in Remark 10.16 of
     "Geometric and higher-order logic in ASD"
     www.PaulTaylor.EU/ASD/loccpct#geohol

I did have in mind (in 2003, largely as a way of avoiding doing
any real analysis) to formulate a language for free algebras and
cofree coalgebras based on this idea.   I then spent half a year
on the construction of the free monoid ("set of lists") and free
semilattice ("finite powerset") on an overt discrete object, ie
writing the paper
     "Inside every model of ASD lies an arithmetic  universe"
     www.PaulTaylor.EU/ASD/loccpct#insema
At no point did this present any insuperable obstacles, but it did
keep presenting obstacles, so I got heartily sick of discrete maths
in ASD, and was then amenable to being persuaded to do some analysis.

The symmetry between
      =>  T  /\   =    some   overt    discrete   free     algebra
and  <=  F  \/   !=   all   compact   Hausdorff  cofree   coalgebra
is very strong in this, but not perfect, because
      N   is   overt    discrete    Hausdorff      not compact
    2^N   is   compact  Hausdorff   not discrete   overt
I have not managed to isolate convincingly the precise point where
the symmetry breaks down.

For example, my paper
     "Computably based locally compact spaces"
     www.PaulTaylor.EU/ASD/loccpct#comblc
investigates the formula
     phi x   =   Some n:N.  A_n phi  /\   beta^n x
that captures the way in which locally compact spaces and locales
have bases of compact/open pairs.   (Note that the spatial and
localic cases are different -- in an interesting topological way,
not just regarding Choice.)

So I thought, "what if" we write down the dual formula
     phi x   =   All k:K.   A_k phi  \/    beta^k x
which we think of as a system of overt/closed pairs indexed by
a compact Hausdorff space K.   (Having used the phrase "dual base"
already,  I called this a "canopy".)

It turns out that every locally compact space has a canopy.
This is proved in the notes
     "Tychonov's theorem in ASD".
     www.PaulTaylor.EU/ASD/misclc#tyctas
which also contain the construction of Cantor space that Toby
mentioned.

All of this is, as I said, within the existing established theory
of locally compact spaces.   Extending the theory beyond this is
something that has occupied my mind for some time without coming
to any satisfactory conclusions.   However, the "equideductive
logic" that arises in any CCC with all finite limits is very
promising as a framework.   I have given three lectures about this,
     www.PaulTaylor.EU/slides/
and described in in the final section of
     "Foundations for Computable Topology"
     www.PaulTaylor.EU/ASD/foufct/

Paul Taylor

PS   The transfer of my website and email to a new hosting company
is now complete.   (PrimeXeon is a small outfit in Cambridge that
provides intelligent  helpful personal service for a mere 20 pounds
per annum.)  There were brief technical and admin problems over the
weekend (I didn't understand MX records) that may have resulted in
a failure to deliver mail to me.  So if you tried to contact me on
Sunday or Monday, please send your message again.