From MAILER-DAEMON Wed Mar 4 17:51:35 2009
Date: 04 Mar 2009 17:51:35 -0400
From: Mail System Internal Data <MAILER-DAEMON@mta.ca>
Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA
Message-ID: <1236203495@mta.ca>
X-IMAP: 1233509219 0000000078
Status: RO
This text is part of the internal format of your mail folder, and is not
a real message. It is created automatically by the mail system software.
If deleted, important folder data will be lost, and it will be re-created
with the data reset to initial values.
From rrosebru@mta.ca Sun Feb 1 13:24:58 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 01 Feb 2009 13:24:58 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LTg2y-0005xO-Ox
for categories-list@mta.ca; Sun, 01 Feb 2009 13:23:52 -0400
Mime-Version: 1.0 (Apple Message framework v624)
Content-Type: text/plain; charset=US-ASCII; format=flowed
Content-Transfer-Encoding: 7bit
From: Paul Taylor <pt09@PaulTaylor.EU>
Subject: categories: Kantor dust
Date: Sun, 1 Feb 2009 16:14:33 +0000
To: Categories list <categories@mta.ca>
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Paul Taylor <pt09@PaulTaylor.EU>
Message-Id: <E1LTg2y-0005xO-Ox@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 1
There are some significant mathematical points that can be made in
response to Vasili Galchin's question about the "constructive"
existence of Cantor space, but I fear that these are going to get
lost in the cross-fire of comments that neither state their background
assumptions nor lay out the mathematics. It is well over a century
since we discovered that it is meaningless to talk about the absolute
truth or falsity of (semantical) statements in mathematics.
There are many many people and foundational positions that call
themselves "constructive". Unfortunately the experts in these
theories have a tendency to assert a monopoly on the word, and ignore
the existence of the other points of view, whilst non-experts
repeat half-remembered and mis-understood opinions that may originate
from the opponents and not the proponents of the theories. On the
other hand, Peter Schuster and Giovanni Sambin have made some effort
in recent years to bring these disciplines together.
I am not going to attempt to make a list of "constructive" theories,
and I would strongly advise against referring to such lists elsewhere,
ESPECIALLY in Wikipedia. Nor am I going to try to represent positions
other than my own -- I invite the respective experts to do this.
Traditionally, Cantor space is described as a subspace of R or [0,1]
using the "middle third" construction, but I learned it like that
long before I became a constructivist of any kind, so I don't know
whether there are any constructive subtleties associated with this view.
I think of Cantor as the exponential 2^N, so FOR EXAMPLE it makes
sense to talk about it in any CCC, or a topos. However, the
interesting question is what it looks like as a TOPOLOGICAL SPACE,
in the many different interpretations of that phrase.
We can do topology starting from the points, or starting from the
open sets. In the latter case, these have a basis whose members are
named by FINITE sets of integers: a point of Cantor space is a
decidable (possibly) infinite set of integers, and lies in a basic
open set if the infinite set includes the finite one.
The first interesting mathematical question is this: if we define
Cantor space starting from its points, but take these to be given
by TOTAL RECURSIVE FUNCTIONS N-->2, and then put the topology
that I have just mentioned on it, what are the properties of this
topology? In particular, is it compact?
The answer is no, because of the "Kleene Tree". This is a computably
defined infnite tree that has no infinite computable path. There
are many descriptions of this, including one by Andrej Bauer:
math.andrej.com/2006/04/25/konigs-lemma-and-the-kleene-tree/
The second interesting mathematical point is that, by looking at the
open sets instead of the points as our formulation of topology, the
answer is different.
The whole of this discussion can be conducted using the closed real
interval in place of Cantor space, so many things are better
documented in the literature for one example rather than the other.
In particular, compactness of the interval has more careful
descriptions in:
LOCALE THEORY: Michael Fourman and Martin Hyland, "Sheaf models for
analysis", in Michael Fourman, Chris Mulvey, and Dana Scott, editors,
"Applications of Sheaves", number 753 in Lecture Notes in Mathematics,
pages 280--301. Springer-Verlag, 1979.
FORMAL TOPOLOGY: Jan Cederquist and Sara Negri, "A constructive proof
of the Heine--Borel covering theorem for formal reals", in
Stefano Beradi and Mario Coppo, editors, "Types for Proofs and
Programs", number 1158 in Lecture Notes in Computer Science,
page 6275. Springer-Verlag, 1996.
ABSTRACT STONE DUALITY: Andrej Bauer and Paul Taylor, "The Dedekind
reals in abstract Stone duality", www.PaulTaylor.EU/ASD/dedras
I wrote a sketch (not a properly written paper) about the construction
of Cantor Space in ASD and its compactness in "Tychonov's Theorem in
ASD",
www.PaulTaylor.EU/ASD/misclc.php#tyctas
Paul Taylor
PS Please refer to my website as paultaylor.eu, not monad.me.uk, as
it will be moving home shortly, and I will be better able to ensure
continuity of service for the name paultaylor.eu, whilst I would like
to discontinue monad.me.uk at some stage.
From rrosebru@mta.ca Sun Feb 1 19:29:23 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 01 Feb 2009 19:29:23 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LTlk6-0001eI-Aw
for categories-list@mta.ca; Sun, 01 Feb 2009 19:28:46 -0400
Date: Sun, 1 Feb 2009 18:53:52 +0000 (GMT)
From: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
To: Vaughan Pratt <pratt@cs.stanford.edu>, categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
Message-Id: <E1LTlk6-0001eI-Aw@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 2
On Sat, 31 Jan 2009, Vaughan Pratt wrote:
> I'm not aware of any reason why a topos with a Cantor set object K has
> to also have a natural number object N, though I'm not enough of a topos
> hacker myself to know how to produce one with K but without N (but would
> be happy to learn). Does such a topos exist in nature? And what can be
> said of the free topos with Cantor set object?
>
A topos with a Cantor set object (i.e. a final coalgebra for FX = X+X)
necessarily has a natural number object. Observe that the Cantor set K
necessarily has a point (since 1 has an F-coalgebra structure), so the
isomorphism K+K \cong K yields a monomorphism K \to K and a point
disjoint from its image. From there on, use Corollary D5.1.3 in the
Elephant.
Peter Johnstone
From rrosebru@mta.ca Sun Feb 1 19:29:23 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 01 Feb 2009 19:29:23 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LTljM-0001bb-Oc
for categories-list@mta.ca; Sun, 01 Feb 2009 19:28:00 -0400
Date: Sun, 1 Feb 2009 19:18:33 +0100
From: gcuri@math.unipd.it
To: categories@mta.ca
Subject: categories: Re: Kantor dust
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: gcuri@math.unipd.it
Message-Id: <E1LTljM-0001bb-Oc@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 3
Further references on the constructive presentation of Cantor space are:
1. P. Martin-Lof, Notes on Constructive Mathematics. Almqvist and Wiksel=
l,
1970.
2. M. Fourman, R. Grayson, Formal Spaces. In: The L.E.J. Brouwer Centenar=
y
Symposium, A.S. Troelstra and D. van Dalen, eds. North Holland, 1982, pp=
.
107-122.
Compactness of Cantor space is equivalent to the fan theorem which is equ=
ivalent
to spatiality of formal Cantor space (Cantor locale).
Best regards,
Giovanni Curi
Quoting Paul Taylor <pt09@PaulTaylor.EU>:
> There are some significant mathematical points that can be made in
> response to Vasili Galchin's question about the "constructive"
> existence of Cantor space, but I fear that these are going to get
> lost in the cross-fire of comments that neither state their background
> assumptions nor lay out the mathematics. It is well over a century
> since we discovered that it is meaningless to talk about the absolute
> truth or falsity of (semantical) statements in mathematics.
>
> There are many many people and foundational positions that call
> themselves "constructive". Unfortunately the experts in these
> theories have a tendency to assert a monopoly on the word, and ignore
> the existence of the other points of view, whilst non-experts
> repeat half-remembered and mis-understood opinions that may originate
> from the opponents and not the proponents of the theories. On the
> other hand, Peter Schuster and Giovanni Sambin have made some effort
> in recent years to bring these disciplines together.
>
> I am not going to attempt to make a list of "constructive" theories,
> and I would strongly advise against referring to such lists elsewhere,
> ESPECIALLY in Wikipedia. Nor am I going to try to represent positions
> other than my own -- I invite the respective experts to do this.
>
> Traditionally, Cantor space is described as a subspace of R or [0,1]
> using the "middle third" construction, but I learned it like that
> long before I became a constructivist of any kind, so I don't know
> whether there are any constructive subtleties associated with this view=
.
>
> I think of Cantor as the exponential 2^N, so FOR EXAMPLE it makes
> sense to talk about it in any CCC, or a topos. However, the
> interesting question is what it looks like as a TOPOLOGICAL SPACE,
> in the many different interpretations of that phrase.
>
> We can do topology starting from the points, or starting from the
> open sets. In the latter case, these have a basis whose members are
> named by FINITE sets of integers: a point of Cantor space is a
> decidable (possibly) infinite set of integers, and lies in a basic
> open set if the infinite set includes the finite one.
>
> The first interesting mathematical question is this: if we define
> Cantor space starting from its points, but take these to be given
> by TOTAL RECURSIVE FUNCTIONS N-->2, and then put the topology
> that I have just mentioned on it, what are the properties of this
> topology? In particular, is it compact?
>
> The answer is no, because of the "Kleene Tree". This is a computably
> defined infnite tree that has no infinite computable path. There
> are many descriptions of this, including one by Andrej Bauer:
> math.andrej.com/2006/04/25/konigs-lemma-and-the-kleene-tree/
>
> The second interesting mathematical point is that, by looking at the
> open sets instead of the points as our formulation of topology, the
> answer is different.
>
> The whole of this discussion can be conducted using the closed real
> interval in place of Cantor space, so many things are better
> documented in the literature for one example rather than the other.
> In particular, compactness of the interval has more careful
> descriptions in:
>
> LOCALE THEORY: Michael Fourman and Martin Hyland, "Sheaf models for
> analysis", in Michael Fourman, Chris Mulvey, and Dana Scott, editors,
> "Applications of Sheaves", number 753 in Lecture Notes in Mathematics=
,
> pages 280--301. Springer-Verlag, 1979.
>
> FORMAL TOPOLOGY: Jan Cederquist and Sara Negri, "A constructive proof
> of the Heine--Borel covering theorem for formal reals", in
> Stefano Beradi and Mario Coppo, editors, "Types for Proofs and
> Programs", number 1158 in Lecture Notes in Computer Science,
> page 6275. Springer-Verlag, 1996.
>
> ABSTRACT STONE DUALITY: Andrej Bauer and Paul Taylor, "The Dedekind
> reals in abstract Stone duality", www.PaulTaylor.EU/ASD/dedras
>
> I wrote a sketch (not a properly written paper) about the construction
> of Cantor Space in ASD and its compactness in "Tychonov's Theorem in
> ASD",
> www.PaulTaylor.EU/ASD/misclc.php#tyctas
>
> Paul Taylor
>
> PS Please refer to my website as paultaylor.eu, not monad.me.uk, as
> it will be moving home shortly, and I will be better able to ensure
> continuity of service for the name paultaylor.eu, whilst I would like
> to discontinue monad.me.uk at some stage.
>
>
>
>
>
>
>
-----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.
Dipartimento di Matematica Pura ed Applicata
Universita' degli Studi di Padova
www.math.unipd.it
From rrosebru@mta.ca Sun Feb 1 19:30:14 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 01 Feb 2009 19:30:14 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LTllR-0001i6-Pf
for categories-list@mta.ca; Sun, 01 Feb 2009 19:30:09 -0400
MIME-Version: 1.0
Date: Sun, 1 Feb 2009 20:11:25 +0100
Subject: categories: Question on "On Closed Categories of Functors"
From: Tony Meman <tonymeman1@googlemail.com>
To: categories <categories@mta.ca>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Tony Meman <tonymeman1@googlemail.com>
Message-Id: <E1LTllR-0001i6-Pf@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 4
Dear category theorists,
I have a question concerning the paper "On Closed Categories of Functors"
from Brian Day (By the way, this is an excellent paper).
Let V be a symmetric monoidal closed category and C a small V-category.
The (ordinary) category [C,V] of V-functors admits the sturcure of a
V-category in a canonical way.
A symmetric monoidal V-category is the enriched analogue of a
symmetric-monoidal structure on an ordinary category, i.e. all the structure
morphisms are V-morphisms and the coherence conditions are fullfilled. The
underlaying category of a symmetric monoidal V-category admits the structure
of an ordinary symmetric monoidal category.
Brian Day constructs a symmetric monoidal closed structure ([C,V],@,E) on
the V-category of V-functors [C,V] for some cases [3.3, 3.6], e.g. if
(C,*,e) is a symmetric monoidal V-category [4.1]. The underlaying *category*
[C,V] of V-functors admits a closed symmetric monoidal structure from the
enriched one by taking the underlaying functor of each V-functor, the
underlaying natural transformation of each V-natural transformation.
Because a closed symmetric monoidal category is canonically enriched over
itself, the category [C,V] gets a [C,V] enrichment in this way.
My question is: What does this [C,V]-enrichment of [C,V] have to do with the
V-enrichment of [C,V]?
Suppose C have a terminal object t. One gets a evaluation functor
Ev_t:[C,V]-CAT-->V-CAT. Is this the connection between the two enrichments?
Thank you in advance for any help.
Tony
From rrosebru@mta.ca Mon Feb 2 17:33:39 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 02 Feb 2009 17:33:39 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LU6NX-0000v6-1t
for categories-list@mta.ca; Mon, 02 Feb 2009 17:30:51 -0400
Date: Sun, 01 Feb 2009 17:16:16 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories list <categories@mta.ca>
Subject: categories: Re: Kantor dust
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LU6NX-0000v6-1t@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 5
Paul Taylor wrote:
> The first interesting mathematical question is this: if we define
> Cantor space starting from its points, but take these to be given
> by TOTAL RECURSIVE FUNCTIONS N-->2, and then put the topology
> that I have just mentioned on it, what are the properties of this
> topology? In particular, is it compact?
>
> The answer is no, because of the "Kleene Tree". This is a computably
> defined infnite tree that has no infinite computable path. There
> are many descriptions of this, including one by Andrej Bauer:
> math.andrej.com/2006/04/25/konigs-lemma-and-the-kleene-tree/
> [...]
> ABSTRACT STONE DUALITY: Andrej Bauer and Paul Taylor, "The Dedekind
> reals in abstract Stone duality", www.PaulTaylor.EU/ASD/dedras
In concrete Stone duality, increasing structure on one side is offset by
decreasing structure on the other. One would hope for a similar
phenomenon in abstract Stone duality.
If we can consider constructivity as part of the structure of an object,
then we should expect that the more constructive some type of object,
the less constructive the "object of all objects of that type." So for
example if (total) recursive functions are demonstrably more
constructive than partial recursive functions by some criterion, we
should expect the set of all recursive functions to be *less*
constructive than that of partial recursive functions by the same
criterion, rather than more.
The phenomena you're observing here seem entirely consistent with this
principle, and point up the need to be clear, when judging
constructivity in some context, whether it is the collection or the
individuals therein being so judged, with the added complication that
Stone duality makes the roles of collection and individual therein
interchangeable, such as when elements of sets are understood as
ultrafilters of Boolean algebras.
Vaughan Pratt
From rrosebru@mta.ca Mon Feb 2 17:33:39 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 02 Feb 2009 17:33:39 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LU6OH-0000zG-Ju
for categories-list@mta.ca; Mon, 02 Feb 2009 17:31:37 -0400
Date: Mon, 2 Feb 2009 18:53:01 +1100 (EST)
Subject: categories: Re: Question on "On Closed Categories of Functors"
From: street@ics.mq.edu.au
To: "Tony Meman" <tonymeman1@googlemail.com>, "categories" <categories@mta.ca>
MIME-Version: 1.0
Content-Type: text/plain;charset=iso-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: street@ics.mq.edu.au
Message-Id: <E1LU6OH-0000zG-Ju@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 6
> Let V be a symmetric monoidal closed category and C a small V-category.
> Brian Day constructs a symmetric monoidal closed structure ([C,V],@,E) =
on
> the V-category of V-functors [C,V] for some cases [3.3, 3.6], e.g. if
> (C,*,e) is a symmetric monoidal V-category [4.1]. The underlying
> *category*
> [C,V] of V-functors admits a closed symmetric monoidal structure from t=
he
> enriched one by taking the underlying functor of each V-functor, the
> underlying natural transformation of each V-natural transformation.
>
> Because a closed symmetric monoidal category is canonically enriched ov=
er
> itself, the category [C,V] gets a [C,V] enrichment in this way.
>
> My question is: What does this [C,V]-enrichment of [C,V] have to do wit=
h
> the V-enrichment of [C,V]?
> Suppose C have a terminal object t. One gets a evaluation functor
> Ev_t:[C,V]-CAT-->V-CAT. Is this the connection between the two enrichme=
nts?
I think what you want here is the following observation.
Every closed monoidal V-category E is also an E-category.
The unit object j for tensor in E is a monoid and so E(j,-) : E --> V
is a monoidal V-functor. Therefore by applying it on hom objects,
it induces a 2-functor E-Cat --> V-Cat. In particular, you can apply
the 2-functor to E itself to see it as a V-category.
Your example is for E =3D [C,V].
Ross
PS I have ordinary- (not enriched-) mailed your message to Brian himself.
He may want to add something when he gets it. But I hope I have the story
you need!
From rrosebru@mta.ca Tue Feb 3 10:22:31 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 03 Feb 2009 10:22:31 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LUM8p-0003RT-Dy
for categories-list@mta.ca; Tue, 03 Feb 2009 10:20:43 -0400
Date: Mon, 02 Feb 2009 15:43:16 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LUM8p-0003RT-Dy@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 7
Prof. Peter Johnstone wrote:
> A topos with a Cantor set object (i.e. a final coalgebra for FX = X+X)
> necessarily has a natural number object. Observe that the Cantor set K
> necessarily has a point (since 1 has an F-coalgebra structure), so the
> isomorphism K+K \cong K yields a monomorphism K \to K and a point
> disjoint from its image. From there on, use Corollary D5.1.3 in the
> Elephant.
Oh, of course: pick a point out of one half and recurse on the other.
Very plausible that that would work in any topos, but it's great to be
able to stare at an actual proof. Thank you!
How about the converse: does N entail K? In any topos with NNO N the
underlying object of the final coalgebra of FX = X+X is presumably 2^N.
Does the Elephant prove that 2^N can be made a final coalgebra of X+X?
And if so, what other coalgebras are brought into existence by N? For
example can N^N be made a doubly inductive (inductive-coinductive)
coalgebra encoding the lexicographic order that gives N^N the order type
of the nonnegative reals? That would give a pretty direct construction
of the usual topology of the real line in any topos with NNO. (This is
the one-dimensional conception of the continuum, as opposed to the
zero-dimensional conception preferred by descriptive set theorists, who
take the continuum to be N^N with the ordinary product topology.)
Does \Omega^N as the final coalgebra for FX = \Omega x X ever arise in
practical situations where \Omega is more than just a pointed version of
1+1 as in Set, e.g. graph theory?
Vaughan Pratt
From rrosebru@mta.ca Tue Feb 3 20:12:06 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 03 Feb 2009 20:12:06 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LUVKt-0000tQ-SP
for categories-list@mta.ca; Tue, 03 Feb 2009 20:09:47 -0400
Date: Tue, 3 Feb 2009 17:59:58 +0000 (GMT)
From: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
To: Vaughan Pratt <pratt@cs.stanford.edu>, categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
Message-Id: <E1LUVKt-0000tQ-SP@mailserv.mta.ca>
Status: RO
X-Status:
X-Keywords:
X-UID: 8
On Mon, 2 Feb 2009, Vaughan Pratt wrote:
> How about the converse: does N entail K? In any topos with NNO N the
> underlying object of the final coalgebra of FX = X+X is presumably 2^N.
> Does the Elephant prove that 2^N can be made a final coalgebra of X+X?
>
It's not in the Elephant; but it's an easy exercise in primitive
recursion, given a coalgebra structure X \to X + X, to define the
transpose N x X \to 2 of the unique coalgebra morphism X \to 2^N.
> And if so, what other coalgebras are brought into existence by N? For
> example can N^N be made a doubly inductive (inductive-coinductive)
> coalgebra encoding the lexicographic order that gives N^N the order type
> of the nonnegative reals? That would give a pretty direct construction
> of the usual topology of the real line in any topos with NNO. (This is
> the one-dimensional conception of the continuum, as opposed to the
> zero-dimensional conception preferred by descriptive set theorists, who
> take the continuum to be N^N with the ordinary product topology.)
>
How do you (constructively) give N^N the order type of the nonnegative
reals? I know how to give it the order type of the irrationals, but
that's still zero-dimensional. However, Freyd's presentation of the
real unit interval as a final coalgebra is done constructively (for any
topos with NNO) in the Elephant, D4.7.17.
Peter Johnstone
From rrosebru@mta.ca Wed Feb 4 16:06:22 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 04 Feb 2009 16:06:22 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LUnzj-0007Cg-CY
for categories-list@mta.ca; Wed, 04 Feb 2009 16:05:11 -0400
From: Gaucher Philippe <gaucher@pps.jussieu.fr>
To: categories@mta.ca
Subject: categories: Preprint : Directed algebraic topology and higher dimensional transition system
Date: Wed, 4 Feb 2009 10:09:25 +0100
MIME-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Gaucher Philippe <gaucher@pps.jussieu.fr>
Message-Id: <E1LUnzj-0007Cg-CY@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 9
Dear all, here is a new preprint. Best regards. pg.
Title: Directed algebraic topology and higher dimensional transition system
Abstract :
Cattani-Sassone's notion of higher dimensional transition system is
interpreted as a small-orthogonality class of a locally finitely presentable
topological category of weak higher dimensional transition systems. In
particular, the higher dimensional transition system associated with the
labelled $n$-cube turns out to be the free higher dimensional transition
system generated by one $n$-dimensional transition. As a first application of
this construction, it is proved that the category of higher dimensional
transition systems is equivalent to a full reflective subcategory of the
category of labelled symmetric precubical sets. As a second application, it is
given a factorization of the mapping taking a CCS process name to a flow
through higher dimensional transition systems. The second application of this
paper can be easily adapted to other process algebras and to other topological
models of concurrency than the one of flows.
URL: http://www.pps.jussieu.fr/~gaucher/HDAparadigm.pdf
From rrosebru@mta.ca Wed Feb 4 16:06:22 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 04 Feb 2009 16:06:22 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LUnz7-00077n-2b
for categories-list@mta.ca; Wed, 04 Feb 2009 16:04:33 -0400
Content-class: urn:content-classes:message
MIME-Version: 1.0
Subject: categories: Fields Workshop on Smooth Structures in Logic, Category Theory and Physics
Date: Tue, 3 Feb 2009 20:55:48 -0500
From: "Pieter Hofstra" <phofstra@uottawa.ca>
To: <categories@mta.ca>
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Pieter Hofstra" <phofstra@uottawa.ca>
Message-Id: <E1LUnz7-00077n-2b@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 10
Fields Institute Workshop, Second Announcement:
Smooth Structures in Logic, Category Theory and Physics
University of Ottawa
May 1-3, 2009
Registration is now open: people can register online at
http://www.fields.utoronto.ca/programs/scientific/08-09/smoothstructures/=
Students who wish to apply for financial support can do so through this =
website. Since we have a limited budget for student support it is =
recommended to apply for this as soon as possible.
Anyone who wishes to contribute a talk is requested to contact one of =
the organizers. In case there are more talks than available time slots =
the organizers will make a selection.
The local website has information on hotels and B&B's near campus:
http://aix1.uottawa.ca/~scpsg/Fields09/Fields09.smoothworkshop.html
With best regards,
Richard Blute (rblute@uottawa.ca)
Pieter Hofstra (phofstra@uottawa.ca)
Philip Scott (phil@site.uottawa.ca)
Michael Warren (mwarren@uottawa.ca)
From rrosebru@mta.ca Thu Feb 5 09:17:57 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 05 Feb 2009 09:17:57 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LV45d-0006Rf-EY
for categories-list@mta.ca; Thu, 05 Feb 2009 09:16:21 -0400
Date: Wed, 4 Feb 2009 23:14:00 -0800 (PST)
From: John Edward <jeedward@yahoo.com>
Subject: categories: Draft paper submission deadline extended: Category Theory
To: categories@mta.ca
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: John Edward <jeedward@yahoo.com>
Message-Id: <E1LV45d-0006Rf-EY@mailserv.mta.ca>
Status: RO
X-Status:
X-Keywords:
X-UID: 11
Draft paper submission deadline extended: Category Theory
=A0=20
The deadline for draft paper submission at the 2009 International Conferenc=
e on Theoretical and Mathematical Foundations of Computer Science (TMFCS-09=
) (website: http://www.PromoteResearch.org ) is extended due to numerous re=
quests from the authors. As a result, the deadline for paper submission for=
the special session on Category Theory is also extended accordingly. The c=
onference and the session will be held during July 13-16 2009 in Orlando, F=
L, USA. The conference will take place at the same time and venue where sev=
eral other international conferences are taking place. The other conference=
s include:=20
=B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Artificial Intellig=
ence and Pattern Recognition (AIPR-09)=20
=B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Automation, Robotic=
s and Control Systems (ARCS-09)=20
=B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Bioinformatics, Com=
putational Biology, Genomics and Chemoinformatics (BCBGC-09)=20
=B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Enterprise Informat=
ion Systems and Web Technologies (EISWT-09)=20
=B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on High Performance Co=
mputing, Networking and Communication Systems (HPCNCS-09)=20
=B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Information Securit=
y and Privacy (ISP-09)=20
=B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Recent Advances in =
Information Technology and Applications (RAITA-09)=20
=B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Software Engineerin=
g Theory and Practice (SETP-09)=20
=B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Theory and Applicat=
ions of Computational Science (TACS-09)=20
=A0=20
The website http://www.PromoteResearch.org contains more details.=20
=A0=20
Sincerely=20
John Edward=20
Publicity committee=20
=A0 =0A=0A=0A
From rrosebru@mta.ca Thu Feb 5 09:17:57 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 05 Feb 2009 09:17:57 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LV44l-0006Jv-C9
for categories-list@mta.ca; Thu, 05 Feb 2009 09:15:27 -0400
Date: Wed, 04 Feb 2009 12:24:41 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LV44l-0006Jv-C9@mailserv.mta.ca>
Status: RO
X-Status:
X-Keywords:
X-UID: 12
Prof. Peter Johnstone wrote:
> On Mon, 2 Feb 2009, Vaughan Pratt wrote:
>
>> How about the converse: does N entail K? In any topos with NNO N the
>> underlying object of the final coalgebra of FX = X+X is presumably 2^N.
>> Does the Elephant prove that 2^N can be made a final coalgebra of X+X?
>>
> It's not in the Elephant; but it's an easy exercise in primitive
> recursion, given a coalgebra structure X \to X + X, to define the
> transpose N x X \to 2 of the unique coalgebra morphism X \to 2^N.
Ah, good, thanks. In that case it should be almost as easy, given a
suitably "easy" coalgebra structure X --> N x X, to define the transpose
N x X --> N of the unique coalgebra morphism X --> N^N.
> How do you (constructively) give N^N the order type of the nonnegative
> reals?
The easiest one is forward lexicographic order (s < t when s(i) < t(i)
at the least i where distinct sequences s and t differ), which has the
order type of [0,oo), equivalently [0,1).
One way to see this is to replace the 0's in the usual binary expansion
of x \in [0,1) by commas and read the resulting comma-separated blocks
of 1's as tally notation.
Alternatively, any monotone bijection f: [0,oo) --> [0,1), such as
x/(x+1) giving one kind of continued fraction, or 2*atan(x)/pi for
"circular continued fractions", induces the monotone bijection
R: N^N --> [0,oo) defined coinductively as
R(s) = s(0) + f(R(s o succ)).
These are among the coalgebraic presentations of the reals Dusko
Pavlovic and I spoke about in Amsterdam on 3/20/99 at CMCS, see ENTCS
19, 133-147 (1999), journal version TCS 280(1-2):105-122 (2002).
> I know how to give it the order type of the irrationals, but
> that's still zero-dimensional.
Reverse lexicographic order gives the irrationals, and is the one
usually encountered with the continued fractions used by "spigot
algorithm" programmers such as Bill Gosper, who don't seem to mind that
the space they're working in is totally disconnected. This results from
not bothering to correct for the antimonotonicity of 1/(x+1). Pedantic
spigot programmers who prefer working in a connected space can easily
substitute its monotonic complement, 1-1/(x+1) = x/(x+1), but
(digressing from mathematical reality for a moment) to what practical
advantage? Presumably Brouwer would take Gosper's side here, it's not
as if the real line is going to crumble into dust when it becomes
totally disconnected by omitting a countable subset, it's still held
together by its metric. Nature abhors topology. A demonstrably
nondiscrete Hausdorff space in either nature or computer engineering
would be a great discovery worthy of the Nobel prize in physics or the
Turing award respectively.
Back to mathematical reality.
> However, Freyd's presentation of the
> real unit interval as a final coalgebra is done constructively (for any
> topos with NNO) in the Elephant, D4.7.17.
Freyd's post of 12/22/99 to this list introducing his presentation,
http://north.ecc.edu/alsani/ct99-00(8-12)/msg00039.html
gives the general provenance for the coalgebraic approach to the reals
as our CMCS paper. Our respective approaches to connecting up the bits
of our coalgebras to form a continuum differ mainly in that Peter
explicitly glues the abutting ends of 2xX ~ X+X together while we
exploit the open-ended nature of N (least but no greatest element, as
the discretization of a half-open interval) for a glue-less connection
at the expense of the additional induction needed when replacing 2 by N.
The choice of poisons is therefore manual glue vs. double induction.
In light of your remark at the start of D4.7 that "there are different
constructions of the reals which are classically equivalent but may
yield different results in a non-Boolean topos," is there a topos in
which the order type of the Freyd coalgebra is not that of the (forward)
lexicographic ordering of N^N (modulo endpoints)? Are they the same in
Grph, for example?
Vaughan Pratt
From rrosebru@mta.ca Thu Feb 5 23:53:35 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 05 Feb 2009 23:53:35 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LVHkW-0001aP-U2
for categories-list@mta.ca; Thu, 05 Feb 2009 23:51:28 -0400
Date: Thu, 5 Feb 2009 13:44:02 -0800
From: Toby Bartels <toby+categories@ugcs.caltech.edu>
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Toby Bartels <toby+categories@ugcs.caltech.edu>
Message-Id: <E1LVHkW-0001aP-U2@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 13
Vaughan Pratt wrote in part:
>Prof. Peter Johnstone wrote:
>>How do you (constructively) give N^N the order type of the nonnegative
>>reals?
>One way to see this is to replace the 0's in the usual binary expansion
>of x \in [0,1) by commas and read the resulting comma-separated blocks
>of 1's as tally notation.
But it's not a constructive theorem that every such x has a binary expansion.
That's still a neat result, that the binary reals are given by N^N,
but the binary reals aren't constructively the same as the reals.
>is there a topos in
>which the order type of the Freyd coalgebra is not that of the (forward)
>lexicographic ordering of N^N (modulo endpoints)?
In the topos of sheaves on the real line,
every function from [0,1) to N is constant,
yet there are obviously many other functions from N^N to N.
Thus N^N and [0,1) are not constructively isomorphic as sets,
so there is no way to give N^N the order type of [0,1) constructively.
--Toby
From rrosebru@mta.ca Sat Feb 7 08:52:31 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sat, 07 Feb 2009 08:52:31 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LVmdG-0006rr-Iz
for categories-list@mta.ca; Sat, 07 Feb 2009 08:50:02 -0400
Date: Fri, 06 Feb 2009 16:37:11 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LVmdG-0006rr-Iz@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 14
Toby Bartels wrote:
> But it's not a constructive theorem that every such x has a binary expansion.
> That's still a neat result, that the binary reals are given by N^N,
> but the binary reals aren't constructively the same as the reals.
Whose reals, Cauchy's or Dedekind's? If the latter then that's no
surprise---carrying out constructions with open order filters is less
constructive than with the Cauchy sequence concept. Lubarsky and
Rathien in Logic and Analysis 1:2 131-152 have recently made the point
that whereas Cauchy reals can be understood constructively as a set, any
attempt to make Dedekind's reals constructive turns them into a proper
class.
Between Dedekind cuts and Cauchy sequences, the more appropriate notion
of reals for constructive analysis would surely be the Cauchy reals.
Are these constructively different from the binary reals? And if so, is
there any intuition underlying that difference that is as clear-cut as
the difference between either and the Dedekind reals?
>
>> is there a topos in
>> which the order type of the Freyd coalgebra is not that of the (forward)
>> lexicographic ordering of N^N (modulo endpoints)?
>
> In the topos of sheaves on the real line,
> every function from [0,1) to N is constant,
> yet there are obviously many other functions from N^N to N.
> Thus N^N and [0,1) are not constructively isomorphic as sets,
> so there is no way to give N^N the order type of [0,1) constructively.
Let's compare apples with apples here. There are presumably going to be
nonconstant *functions* from the Freyd coalgebra object to 2 in this
topos, although they won't be continuous with respect to the topology
induced on that object by its coalgebra structure. But neither will the
nonconstant functions from N^N to N be continuous with respect to the
order interval topology on N^N lexicographically ordered. So I don't
see any progress here towards distinguishing the order type of the Freyd
coalgebra from the lexicographic order on N^N, in this topos or any other.
Vaughan Pratt
From rrosebru@mta.ca Sat Feb 7 16:06:00 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sat, 07 Feb 2009 16:06:00 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LVtPW-00034X-7B
for categories-list@mta.ca; Sat, 07 Feb 2009 16:04:18 -0400
Date: Sat, 7 Feb 2009 17:18:29 +0000 (GMT)
From: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
To: Vaughan Pratt <pratt@cs.stanford.edu>, categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
Message-Id: <E1LVtPW-00034X-7B@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 15
On Fri, 6 Feb 2009, Vaughan Pratt wrote:
>
> Toby Bartels wrote:
>> But it's not a constructive theorem that every such x has a binary
>> expansion.
>> That's still a neat result, that the binary reals are given by N^N,
>> but the binary reals aren't constructively the same as the reals.
>
> Whose reals, Cauchy's or Dedekind's?
Toby was of course referring to the Dedekind reals, but your binary
reals are not constructively either the Cantor or the Dedekind reals.
The reason is that you have to know in advance that a binary
sequence isn't going to end in an infinite string of 1's; by excluding
those sequences, you make the question "Is x < 1/2?" decidable,
which is not constructively true of either the Cantor reals or the
Dedekind reals.
> If the latter then that's no
> surprise---carrying out constructions with open order filters is less
> constructive than with the Cauchy sequence concept. Lubarsky and
> Rathien in Logic and Analysis 1:2 131-152 have recently made the point
> that whereas Cauchy reals can be understood constructively as a set, any
> attempt to make Dedekind's reals constructive turns them into a proper
> class.
>
> Between Dedekind cuts and Cauchy sequences, the more appropriate notion
> of reals for constructive analysis would surely be the Cauchy reals.
I could take issue with you on this. If you insist that "constructive"
entails "predicative", then you are of course right; but in a topos-
theoretic context, where you don't have countable choice automatically
available, it's very much the other way round.
>>
>> In the topos of sheaves on the real line,
>> every function from [0,1) to N is constant,
>> yet there are obviously many other functions from N^N to N.
>> Thus N^N and [0,1) are not constructively isomorphic as sets,
>> so there is no way to give N^N the order type of [0,1) constructively.
>
> Let's compare apples with apples here. There are presumably going to be
> nonconstant *functions* from the Freyd coalgebra object to 2 in this
> topos, although they won't be continuous with respect to the topology
> induced on that object by its coalgebra structure.
No -- that's the whole point. In the topos of sheaves on R (better, in
the gros topos of sheaves on topological spaces) every function
R --> R is continuous, hence every function [0,1] --> 2 is constant.
Peter Johnstone
From rrosebru@mta.ca Sun Feb 8 09:52:32 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 08 Feb 2009 09:52:32 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWA3I-0001os-Pn
for categories-list@mta.ca; Sun, 08 Feb 2009 09:50:28 -0400
Date: Sun, 8 Feb 2009 12:56:53 +0100
From: gcuri@math.unipd.it
To: categories@mta.ca
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: gcuri@math.unipd.it
Message-Id: <E1LWA3I-0001os-Pn@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 16
Quoting "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>:
> > If the latter then that's no
> > surprise---carrying out constructions with open order filters is less
> > constructive than with the Cauchy sequence concept. Lubarsky and
> > Rathien in Logic and Analysis 1:2 131-152 have recently made the poin=
t
> > that whereas Cauchy reals can be understood constructively as a set, =
any
> > attempt to make Dedekind's reals constructive turns them into a prope=
r
> > class.
> >
> > Between Dedekind cuts and Cauchy sequences, the more appropriate noti=
on
> > of reals for constructive analysis would surely be the Cauchy reals.
>
> I could take issue with you on this. If you insist that "constructive"
> entails "predicative", then you are of course right; but in a topos-
> theoretic context, where you don't have countable choice automatically
> available, it's very much the other way round.
Even if one insists that constructive entails predicative the appropriate=
ness of
Cauchy reals is questionable: Lubarsky and Rathjen prove in fact that in =
a=20
subsystem of CZF (Aczel' constructive set theory), i.e., in CZF with
Subset Collection replaced by exponentiation, the Dedekind reals form a =
proper
class.
In ordinary CZF (that has no choice principle and no powersets),
the Dedekind reals *do* form a set (Aczel & Rathjen), as do more generall=
y the
points of any weakly set-presented T^*_1 locale (Aczel & Curi),
in particular of any locally compact regular one.
It is also useful to recall that (in "On the Cauchy Completeness of the
Constructive Cauchy Reals", MLQ, 53, No. 4-5 (2007), pp. 396-414)
Lubarsky has proved that the Cauchy Reals are not complete in intuitioni=
stic
set theory without choice.
There's then the point of view that, constructively, the reals should be
considered as a `space', rather than a set, and that in this perspective =
they
are more properly regarded e.g. as a locale/formal space (rather than as =
a
set/class of points with a topology)...
Regards,
Giovanni Curi
-----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.
Dipartimento di Matematica Pura ed Applicata
Universita' degli Studi di Padova
www.math.unipd.it
From rrosebru@mta.ca Sun Feb 8 09:52:32 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 08 Feb 2009 09:52:32 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWA2p-0001nu-3U
for categories-list@mta.ca; Sun, 08 Feb 2009 09:49:59 -0400
Date: Sat, 7 Feb 2009 14:58:19 -0800
From: Toby Bartels <toby+categories@ugcs.caltech.edu>
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Toby Bartels <toby+categories@ugcs.caltech.edu>
Message-Id: <E1LWA2p-0001nu-3U@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 17
Prof. Peter Johnstone wrote in part:
>Vaughan Pratt wrote:
>>Whose reals, Cauchy's or Dedekind's?
>Toby was of course referring to the Dedekind reals
Actually, I was trying to keep it open,
since different schools of constructivism have different opinions
about which are the correct reals (as well as which are equivalent).
But nobody uses the binary reals, since they can't subtract them.
(To get the first digit of 0.1000000000... - 0.01000000000...,
you need to know which sequence, if either, stops repeating first.)
I agree that one would default to Dedekind reals (or something equivalent),
since that seems to be agreed on by the "practising" schools
(that is, those constructivists trying to do ordinary mathematics,
albeit constructively, rather than doing metamathematics).
>>Lubarsky and
>>Rathien in Logic and Analysis 1:2 131-152 have recently made the point
>>that whereas Cauchy reals can be understood constructively as a set, any
>>attempt to make Dedekind's reals constructive turns them into a proper
>>class.
I'll have to read what they mean, but to say ~any~ attempt seems too strong.
Even in a predicative theory, countable choice implies their equivalence,
so are they claiming that countable choice is not constructive?
(In my experience, Fred Richman is the only practising non-finitist analyst
who doubts both excluded middle and countable choice.)
The Dedekind reals can also be constructed in CZF
(Peter Aczel's predicative constructive set theory)
even if you remove countable choice, using subset collection aka fullness.
Similarly, if you remove identity types from intensional type theory
(so breaking the justification of countable choice),
you can still justify the fullness axiom and so construct the Dedekind reals
(albeit not literally as sets of rational numbers).
>>Between Dedekind cuts and Cauchy sequences, the more appropriate notion
>>of reals for constructive analysis would surely be the Cauchy reals.
The experience in measure theory and Banach space theory since the 1980s
suggests that a Dedekind-complete ordered field is needed.
The only question is whether such a thing exists; most believe it does.
(If countable choice or excluded middle holds, the Cauchy reals work,
which takes care of nearly every practising analyst, constructive or not.
Fred Richman, the only exception I know, still uses the Dedekind reals,
although that's easy for him since he is not predicativist.)
Note: everything above is about the ~located~ Dedekind reals;
a located Dedekind cut is a pair (L,U) of order-open inhabited sets
such that r in L and s in U => r < s => r in L or s in U.
This is what Freyd's coalgebra construction produces,
and it's what practising analysts want to use.
--Toby
From rrosebru@mta.ca Sun Feb 8 16:39:57 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 08 Feb 2009 16:39:57 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWGQu-0002qe-G5
for categories-list@mta.ca; Sun, 08 Feb 2009 16:39:16 -0400
Mime-Version: 1.0 (Apple Message framework v624)
Content-Transfer-Encoding: 7bit
From: Paul Taylor <pt09@PaulTaylor.EU>
Subject: categories: Re: "Kantor dust"
Date: Sun, 8 Feb 2009 15:03:04 +0000
To: Categories list <categories@mta.ca>
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Paul Taylor <pt09@PaulTaylor.EU>
Message-Id: <E1LWGQu-0002qe-G5@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 18
There have been several very interesting comments on this thread,
but I would like to repeat my request that people should be clear
about
WHICH OF MANY "CONSTRUCTIVE" THEORIES OF MATHEMATICS
they mean as the context of their comments. There are, as I said,
interesting mathematical points to be made, both within each of
these theories, and by comparing them. However, without a clear
statement of the foundational context, the discussion degenerates.
The original question was about Cantor space, rather than either
the Cauchy or Dedekind reals. If you want to construct Cantor space
from the reals by the "missing third" construction, I would think
that it makes little difference whether you start from Cauchy or
Dedekind. Or, indeed, from binary sequences, which of course form
a Cantor space in the first place, so that is really a question of
how to construct the reals from Cantor space rather than vice versa.
Vaughan Pratt said
> between Dedekind cuts and Cauchy sequences, the more appropriate notion
> of reals for constructive analysis would surely be the Cauchy reals
and I am certainly aware that, as a sociological fact, many type
theorists and exact real arithmetic programmers believe this.
Can anybody point me to a reasoned critique, or justification of the
view that Cauchy sequences are "more appropriate" for purposes such
as these? All that I have ever heard is essentially a condemnation
of Dedekind for the "heresy" of impredicativity, uncountability,
non-computability, being a proper class, etc.
I gave a lecture (see PaulTaylor.EU/slides) entitled "In defence of
Dedekind and Heine--Borel", which I presented as if I were an
advocate in a court of law. Several type theorists and constructive
analysts were present. Beforehand, I had asked around for a statement
of "the case against Dedekind", but nobody seemed to be able to state
it for me.
Five years ago I had no opinion whatever on these matters, but, as you
gather, I now consider that both Dedekind completeness and the Heine--
Borel theorem are essential parts of "constructive" analysis. Of
course, I think that because the reals in Abstract Stone Duality
satisfy them (and because it puts me in agreement with mainstream
analysts). However, ASD is a recursively axiomatised and enumerable
theory. I don't like the notions of (un)countability or
(im)predicativity, but, if you must apply them, ASD is countable
and predicative.
Regarding computation, last year Andrej Bauer gave a "proof of concept"
demonstration that one can compute efficiently with Dedekind reals
in the ASD language for R. This of course uses interval arithmetic,
but in fact it also makes extremely novel use of back-to-front
("Kaucher") intervals, which appear but are very badly presented
in the interval analysis literature. I have been trying to persuade
him to make this work publicly available.
Since I'm talking about the reals in ASD, I should say what the
difference is between the Cauchy and Dedekind reals is there.
I haven't actually written out a construction of the Cauchy reals,
but the evidence that I do have is that THEY ARE THE SAME. More
precisely, Dedekind completeness is inter-derivable with sobriety
for R, just as definition by description is equivalent to sobriety
of N. This means that if you construct the "Cauchy reals" as a
quotient of Cantor space by an equivalence relation (this is known
as the "signed binary" representation of reals) within ASD then
the result will be Dedekind complete. The details of this are
set out in Section 14 of "The Dedekind reals in ASD" by Andrej and me,
www.PaulTaylor.EU/ASD/dedras
I think it is worth making a note of Vaughan's earlier comment that
> In concrete Stone duality, increasing structure on one side is offset
> by
> decreasing structure on the other. One would hope for a similar
> phenomenon in abstract Stone duality.
>
> If we can consider constructivity as part of the structure of an
> object,
> then we should expect that the more constructive some type of object,
> the less constructive the "object of all objects of that type." So
> for
> example if (total) recursive functions are demonstrably more
> constructive than partial recursive functions by some criterion, we
> should expect the set of all recursive functions to be *less*
> constructive than that of partial recursive functions by the same
> criterion, rather than more.
>
> The phenomena you're observing here seem entirely consistent with this
> principle, and point up the need to be clear, when judging
> constructivity in some context, whether it is the collection or the
> individuals therein being so judged, with the added complication that
> Stone duality makes the roles of collection and individual therein
> interchangeable, such as when elements of sets are understood as
> ultrafilters of Boolean algebras.
However, I think that the Galois--Stone contravariance applies WITHIN
a particular foundational system, and not to VARIATIONS of the degree
of constructivity. Indeed, the usual experience in setting up a
Galois connection or Stone adjunction is that, in order to make the
comparison work at all, you need to make additional assumptions.
Paul Taylor
From rrosebru@mta.ca Sun Feb 8 16:39:57 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 08 Feb 2009 16:39:57 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWGQH-0002oB-Qf
for categories-list@mta.ca; Sun, 08 Feb 2009 16:38:37 -0400
Date: Sun, 8 Feb 2009 14:51:19 +0000 (GMT)
From: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
To: Toby Bartels <toby+categories@ugcs.caltech.edu>, <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
Message-Id: <E1LWGQH-0002oB-Qf@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 19
On Sat, 7 Feb 2009, Toby Bartels wrote:
>> Toby was of course referring to the Dedekind reals
>
> Actually, I was trying to keep it open,
> since different schools of constructivism have different opinions
> about which are the correct reals (as well as which are equivalent).
> But nobody uses the binary reals, since they can't subtract them.
Never mind subtraction -- you can't even add them. As I mentioned in my
last posting, the question "Is x < 1/2?" is decidable for Vaughan's binary
reals, but "Is x < 1/3?" is not (constructively), so the operation
of adding 1/6 can't be defined.
Peter Johnstone
From rrosebru@mta.ca Mon Feb 9 13:04:35 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 09 Feb 2009 13:04:35 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWZVh-0000T8-C1
for categories-list@mta.ca; Mon, 09 Feb 2009 13:01:29 -0400
MIME-version: 1.0
Message-id: <8C91305E-226A-4D07-9604-9BA021A27B4F@me.com>
From: Steve Stevenson <fatmarauder@me.com>
To: Toby Bartels <toby+categories@ugcs.caltech.edu>, <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Date: Sun, 08 Feb 2009 15:36:37 -0500
Content-type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Content-transfer-encoding: 7BIT
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Steve Stevenson <fatmarauder@me.com>
Status: O
X-Status:
X-Keywords:
X-UID: 20
On Feb 7, 2009, at 5:58 PM, Toby Bartels wrote:
> Prof. Peter Johnstone wrote in part:
>
>> Vaughan Pratt wrote:
>
>>> Whose reals, Cauchy's or Dedekind's?
>
>> Toby was of course referring to the Dedekind reals
How about IEEE 754 reals? They're really "scientific notation". There
has been a tremendous amount of work on them by William Kahan and
others and now are the standard for the numerical analysis world and
computers. Since this is the basics for computation, I'd propose that
they can be tightened up even more to suit constructivist purposes.
Steve
--------
D. E. Stevenson, Department of Computer Science
Director, Institute for Modeling and Simulation Applications
Clemson University, Clemson, SC 29634-0974
From rrosebru@mta.ca Mon Feb 9 13:04:36 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 09 Feb 2009 13:04:36 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWZYd-0000nY-TQ
for categories-list@mta.ca; Mon, 09 Feb 2009 13:04:31 -0400
Date: Sun, 8 Feb 2009 16:31:34 -0800
From: Toby Bartels <toby+categories@ugcs.caltech.edu>
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Toby Bartels <toby+categories@ugcs.caltech.edu>
Message-Id: <E1LWZYd-0000nY-TQ@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 21
Steve Stevenson wrote in part:
>How about IEEE 754 reals? They're really "scientific notation". There
>has been a tremendous amount of work on them by William Kahan and others
>and now are the standard for the numerical analysis world and computers.
>Since this is the basics for computation, I'd propose that they can be
>tightened up even more to suit constructivist purposes.
Floating-point reals have terrible theoretical properties;
they're not even a ring (not even classically).
This is why even after all of Kahan's good work on algorithms,
rounding errors are unavoidable (the "Table-Maker's Dilemma").
A floating-point real basically consists of a rational number x
together with a rational maximum error e, subject to the condition
that, for some integer n, 10^n x is an integer and e = 10^{-n}/2.
(There is some redundancy in this simplified description.)
This is not acceptable constructively, since one cannot prove
(even with countable choice, impredicative power sets, etc)
that every real number has such a floating-point representation.
At the very least, one must add some epsilon to the maximum e;
to keep it simple, I would set e to 10^{-n} (so that 1.6 is acceptable
as the result of 5/3, although good algorithms would probably give 1.7).
This would remove rounding errors from the Table-Maker's Dilemma.
I believe (but I may be wrong through unfamiliarity with the literature)
that most researchers prefer instead to allow arbitrarily large e,
thus using interval arithmetic, even though this is more complicated.
(Actual implementations of floating-point arithmetic
usually also have maximum allowed values of both n and 10^n x,
leading to rounding errors from underflow and overflow.
However, overflow errors already arise in natural-number arithmetic,
so this is not really the fault of the floating-point idea.
One can delay all such errors until run-time memory limits.)
--Toby
From rrosebru@mta.ca Mon Feb 9 13:08:04 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 09 Feb 2009 13:08:04 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWZbu-0001Bx-OX
for categories-list@mta.ca; Mon, 09 Feb 2009 13:07:54 -0400
Date: Sun, 8 Feb 2009 17:30:31 -0800
From: Toby Bartels <toby+categories@ugcs.caltech.edu>
To: Categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Toby Bartels <toby+categories@ugcs.caltech.edu>
Message-Id: <E1LWZbu-0001Bx-OX@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 22
Paul Taylor wrote in part:
>Can anybody point me to a reasoned critique, or justification of the
>view that Cauchy sequences are "more appropriate" for purposes such
>as these? All that I have ever heard is essentially a condemnation
>of Dedekind for the "heresy" of impredicativity, uncountability,
>non-computability, being a proper class, etc.
>I gave a lecture (see PaulTaylor.EU/slides) entitled "In defence of
>Dedekind and Heine--Borel", which I presented as if I were an
>advocate in a court of law. Several type theorists and constructive
>analysts were present. Beforehand, I had asked around for a statement
>of "the case against Dedekind", but nobody seemed to be able to state
>it for me.
Besides the case that you present briefly in your slides,
there is this: The Cauchy reals exist an a Pi-W-pretopos
(equivalently, in a constructive set or type theory
with exponentiation but no power sets or even fullness
and with infinity but no countable choice).
But the Dedekind reals, as far as I can tell, do not;
excluded middle, power sets, fullness, or countable choice
would each do the job, but you need ~something~.
(ASD takes another approach, of course.)
And while I don't know any non-finitist practising constructivists
that doubt all of these, I do know at least one that doubts each.
Thus practising constructivists may happily use the Dedekind reals,
while formalists that want to cover all practising schools
find that they are not quite available in the obvious common denominator.
(Actually, Brouwer intuitionists don't really even accept exponenenation,
although they do accept N^N and AC_00 so do have Cauchy = Dedekind reals.)
I don't find this argument conclusive; the proper course is either
to accept the existence of the Dedekind reals as an axiom
(since everybody believes it, even if for different reasons)
or just to give up on point-set topology and use locales
(although these require subtlety to use predicatively).
But it's there, and it probably explains some logicians' positions.
>However, ASD is a recursively axiomatised and enumerable
>theory. I don't like the notions of (un)countability or
>(im)predicativity, but, if you must apply them, ASD is countable
>and predicative.
But ASD with the underlying-set axiom is impredicative, yes?
I really like ASD, so don't interpet my post as opposition to your position,
but rather an attempt to clarify what the opposition may be thinking.
--Toby
From rrosebru@mta.ca Mon Feb 9 13:12:35 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 09 Feb 2009 13:12:35 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWZgH-0001f3-1n
for categories-list@mta.ca; Mon, 09 Feb 2009 13:12:25 -0400
From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
Date: Mon, 9 Feb 2009 12:49:38 +0100
To: categories@mta.ca
Subject: categories: Dedekind versus Cauchy reals
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
Message-Id: <E1LWZgH-0001f3-1n@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 23
Paul has asked why most constructivists have a preference for Cauchy numerals.
Well, most constructivists haven't since under the widely accepted AC_N they
coincide. This, of course, doesn't deny the fact that in many sheaf toposes
AC_n fails. But from point of view of the BHK interpretation AC_N is most
natural.
But I think the reason for prefering Cauchy over Dedekind has a quite
pragmatic reason. What you are interested in is a Cauchy sequence of reals
with a fixed rate of convergence (ensuring e.g. that the n-th item has distance
< 2^{-n} to the limit). AC_N of course allows you to magically find a modulus
of convergence for every Cauchy sequence. But like Church's Thesis or Brouwer's
Theorem this is sort of a Deus ex machina (actually those are 2 contradictory
dei ex machina!) and thus of moderate help for exact computation on the reals.
If you base your reals on Dedekind's idea you may certainly compute with them
but the result isn't very telling because a computable Dedkind real is a
semidecision procedure telling you whether a given rational interval contains
the (ideal) real under consideration. This doesn't help you at all to compute
the real up to a given precision because you have to first guess the right
interval. Of course, you may consider a partition of some area of guesses
and apply the semidecision procedure to all those intervals in parallel. But
that's very inefficient and can't be implemented within usual sequential
programming languages.
Thomas
From rrosebru@mta.ca Mon Feb 9 14:51:50 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 09 Feb 2009 14:51:50 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWbDR-0004d2-5V
for categories-list@mta.ca; Mon, 09 Feb 2009 14:50:45 -0400
MIME-Version: 1.0
Date: Mon, 9 Feb 2009 12:26:32 +0100
Subject: categories: symmetric monoidal adjunctions
From: Tony Meman <tonymeman1@googlemail.com>
To: categories <categories@mta.ca>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Tony Meman <tonymeman1@googlemail.com>
Message-Id: <E1LWbDR-0004d2-5V@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 24
Dear category theorists,
I have a question concerning symmetric monoidal adjunctions (of symmetric
monoidal functors).
Let V and W be symmetric monoidal categories, C a small category, F, G
symmetric monoidal functors and F:V<-->W:G a symmetric monoidal adjunction.
Is f:Fun(C,V)<-->Fun(C,W):g a symmetric monoidal adjunction? The functor
categories Fun(C,V) and Fun(C,W) are endowed with the pointwise symmetric
monoidal structure and the functors f and g are defined pointwise, too.
I am sorry that I have to ask you all this things about monoidal categories
and enriched categories but I can't find a book on that. I would be very
pleased if anybody can suggest me something to read.
Thank you in advance for any help.
Tony
From rrosebru@mta.ca Tue Feb 10 08:29:39 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 10 Feb 2009 08:29:39 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWrjN-0000Be-87
for categories-list@mta.ca; Tue, 10 Feb 2009 08:28:49 -0400
Date: Mon, 9 Feb 2009 22:47:56 +0000 (GMT)
From: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
To: Dusko Pavlovic <Dusko.Pavlovic@comlab.ox.ac.uk>, <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
Message-Id: <E1LWrjN-0000Be-87@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 25
On Mon, 9 Feb 2009, Dusko Pavlovic wrote:
> QUESTION 1: re peter johnstone's
>
>> > > In the topos of sheaves on the real line,
>> > > every function from [0,1) to N is constant,
>> > > yet there are obviously many other functions from N^N to N.
>> > > Thus N^N and [0,1) are not constructively isomorphic as sets,
>> > > so there is no way to give N^N the order type of [0,1)
>> > > constructively.
>
> are you claiming that this statement is true with respect to every base topos
> and every real line in it? (the discussion seems to have touched upon the
> various constructions of the various real lines. it would be nice to know
> where is the one, over which you build the topos, is coming from.)
>
That's actually a quote from Toby Bartels, not from me.
It's a statement about a topos built over the classical topos of sets;
the argument is a rather ad hoc one, and I'm not sure to what extent
it's possible to make it constructive. However, as I said elsewhere, I
prefer to work with the gros topos of spaces (i.e. sheaves on a suitable
full subcategory of spaces for the coverage consisting of jointly-
surjective families of open inclusions) and there it's quite clear
what you need: namely, Heine--Borel (equivalently, exponentiability
of R in your category of spaces). That's not true in all toposes;
you could try to get round it by basing your gros topos on locales
rather than spaces (the locale of formal reals being constructively
locally compact), but it's not clear (to me, at least) what the
result would actually mean if you based yourself on a topos where
the formal reals aren't spatial.
> QUESTION 2: is there a branch of constructivism that would reject as
> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as the
> coefficients of continued fractions?
>
I don't think there is any doubt that the map exists. The problem is that,
for most if not all schools of constructivism, it's wildly non-surjective.
Peter Johnstone
From rrosebru@mta.ca Tue Feb 10 08:29:39 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 10 Feb 2009 08:29:39 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LWriU-000088-W1
for categories-list@mta.ca; Tue, 10 Feb 2009 08:27:55 -0400
Date: Mon, 9 Feb 2009 22:18:44 +0000 (GMT)
From: Dusko Pavlovic <Dusko.Pavlovic@comlab.ox.ac.uk>
To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>, <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Dusko Pavlovic <Dusko.Pavlovic@comlab.ox.ac.uk>
Message-Id: <E1LWriU-000088-W1@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 26
hi.
i missed most of this thread, but even this one message that i did catch
raises several questions that i would like to share.
QUESTION 1: re peter johnstone's
>>> In the topos of sheaves on the real line,
>>> every function from [0,1) to N is constant,
>>> yet there are obviously many other functions from N^N to N.
>>> Thus N^N and [0,1) are not constructively isomorphic as sets,
>>> so there is no way to give N^N the order type of [0,1) constructively.
are you claiming that this statement is true with respect to every base
topos and every real line in it? (the discussion seems to have touched
upon the various constructions of the various real lines. it would be nice
to know where is the one, over which you build the topos, is coming from.)
QUESTION 2: is there a branch of constructivism that would reject as
non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as
the coefficients of continued fractions?
COMMENT: IF the answer to either of the above questions is NO, then
maybe the tacit
SLOGAN that "constructively valid" = "true in every topos"
needs to be taken *very carefully*. when we build toposes over classical
universes, then we may be able to force away more than any constructivist
would ever reject. the strict constructivist logics have already been
marginalized as too restrictive; lets not completely bury them just for
the joy of constructing counterexamples.
moreover, EVEN IF the answer to both of the above questions is YES, the
above SLOGAN still does not tell the whole story, IMHO.
the constructivists wanted to make our computations effective. that goal
led to some great philosophical debates in the first half of XX century.
later people built computers and paid lots of programmers to make
computations effective. besides brouwer, and heyting and kolmogorov, maybe
we should admit that people like gosper, and knuth, and dijkstra, and our
own vaughan pratt, also have an idea about what is effectively computable.
peter johnstone points out that the comparison test for the binary reals
(i presume the reals in base 2; there are many other representations, of
course) is undecidable. this actually applies to every base, and even to
the continued fraction representation (because it is irredundant). but in
the practice of effective computations, this is no showstopper. there are
many things that need to be computed with the reals, and no one
representation fits for all purposes. so the statement
> nobody uses the binary reals
probably has more counterexamples than, say, the statement "nobody
uses toposes". even if "the" binary reals were completely wrong.
the study of the various effective algebraic operations on the reals,
always reduced to one binary form or another, goes back at least to gosper
and schroepel, the original "hackers" from the 70s. they were, of course,
aware that the comparison test was undecidable. buyt people prefer to run
a program that may not terminate, or will terminate fast, over a program
guaranteed to terminate between tomorrow and 2 years from now.
gosper's continued fraction representation was improved by jean
vuillemin, who proposed in 1990s a redundant representation, where the
comparison test is decidable. this is what at least some people have
really been using in their real projects, sensitive enough to bring
the chaotic effects of the floating point arithmetic to the surface.
it would be interesting to understand whether the notion of computability
as embodied in toposes is related in some rational way with the notion of
computability as embodied in computers.
-- dusko
From rrosebru@mta.ca Wed Feb 11 09:39:42 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 09:39:42 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXFJI-0002uv-BD
for categories-list@mta.ca; Wed, 11 Feb 2009 09:39:28 -0400
MIME-version: 1.0
Content-transfer-encoding: 7BIT
Content-type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Message-id: <BD697166-93F0-4319-8712-E68F1E9C7041@me.com>
From: Steve Stevenson <fatmarauder@me.com>
To: Toby Bartels <toby+categories@ugcs.caltech.edu>, <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Date: Tue, 10 Feb 2009 14:04:11 -0500
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Steve Stevenson <fatmarauder@me.com>
Status: O
X-Status:
X-Keywords:
X-UID: 27
On Feb 8, 2009, at 7:31 PM, Toby Bartels wrote:
> Steve Stevenson wrote in part:
>
>> How about IEEE 754 reals? They're really "scientific notation".
>> <snip>
>
> Floating-point reals have terrible theoretical properties;
> they're not even a ring (not even classically).
> This is why even after all of Kahan's good work on algorithms,
> rounding errors are unavoidable (the "Table-Maker's Dilemma").
<snip>
Being left-handed and old, I'll propose in my dotage that we may be
asking the wrong question. In a rewording, what constructive real
numbers are there for the purpose of
1. Being a model of an axiomatic characterization of the reals.
2 Being usable in supercomputing to compute values needed for
modeling and simulation.
Number 1 requires that we have nice theoretical properties. Number 2
requires something that is bounded only the dollars and life span.
Those interested in either purpose have (presumedly) a solution for
themselves.
The first fix for number 2 might be to go to interval arithmetic ---
now what do I need to guarantee that the "real number (in 1)" is
trapped between two #2 numbers? Given the bandwidth and memory
capacity, we should be able to do those things worth doing: H5N1
infection prediction, climate modeling, malaria control, food
production ... I'm willing to live with a demonstrably correct
approximation given that we are in an uncertain world. I'll never get
the exact answer, I'll only get an approximation.
Interval guarantees seems interesting to me.
---
Steve Stevenson
It's not that people don't know, it's so much of what they know ain't
so - Josh Billings.
From rrosebru@mta.ca Wed Feb 11 09:39:42 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 09:39:42 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXFIA-0002oj-3h
for categories-list@mta.ca; Wed, 11 Feb 2009 09:38:18 -0400
Date: Tue, 10 Feb 2009 19:03:56 +0100
From: "I. Moerdijk" <I.Moerdijk@uu.nl>
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: postdoc position in Utrecht
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "I. Moerdijk" <I.Moerdijk@uu.nl>
Message-Id: <E1LXFIA-0002oj-3h@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 28
There is a vacancy for a postdoc position in topology at our department
in Utrecht.
The position is for two or three years, and is funded by the Dutch
science organisation NWO. It is part of a specific research project,
which in practice means that we are looking for candidates working in
the convex hull of
stable homotopy theory -- topological field theory -- operads -- higher
categories.
The starting time is flexible, although we aim
to fill the position between 1 August 2009 and 1 January 2010.
If you're interested, please send me an email and append your CV.
Ieke Moerdijk
<I.Moerdijk@uu.nl>
From rrosebru@mta.ca Wed Feb 11 09:39:43 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 09:39:43 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXFH4-0002jJ-B3
for categories-list@mta.ca; Wed, 11 Feb 2009 09:37:10 -0400
Date: Tue, 10 Feb 2009 01:54:06 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LXFH4-0002jJ-B3@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 29
Prof. Peter Johnstone wrote:
> On Mon, 9 Feb 2009, Dusko Pavlovic wrote:
>> QUESTION 2: is there a branch of constructivism that would reject as
>> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N
>> as the coefficients of continued fractions?
>>
> I don't think there is any doubt that the map exists. The problem is that,
> for most if not all schools of constructivism, it's wildly non-surjective.
There is more than one notion of continued fraction. I suspect you're
thinking of one of the more commonly used ones, but in the light of
Dusko and my CMCS'99 paper, which talks about a number of notions of
continued fraction, I imagine Dusko had one in mind for which the map is
classically a bijection, and surely should continue to be so for at
least some schools of constructivism. Let me give a (hopefully) careful
proof of this here.
As I observed in a previous post, the pathological definitions of
"continued fraction" giving the behaviour you may be thinking of are
those whose coinductive step is antimonotone, e.g. via a function from
[0,oo) to (0,1] such as 1/(1+x). These appear in the literature not
from any desire to be pathological but merely because they tend to be
the first ones that come to mind, and their non-surjectivity is simply
not noticed by the naive programmer.
In contrast, monotone functions from [0,oo) to [0,1) such as x/(1+x) or
2*atan(x)/pi, with respective inverses x/(1-x) and tan(pi*x/2), do not
create this pathology in the continued fractions based on them, and give
rise to maps from N^N to [0,1) and [0,oo) that are not only surjective
but bijective, as well as monotone increasing with respect to the
lexicographic order on N^N.
Let R: N^N --> [0,oo) be the strictly monotone increasing function (with
respect to the lexicographic order on N^N) defined coinductively as
R(s) = s(0) + f(R(s o succ))
where s: N --> N is a sequence in N^N (a function on N),
f: [0,oo) --> [0,1) is a strictly monotone increasing function, for
example f(x) = x/(1+x), and succ: N --> N is the successor operation of
the NNO N.
As a (surely constructive!) witness to the surjectivity, indeed
bijectivity, of R, define the inverse S: [0,oo) --> N^N of R as
follows. (R converts sequences to Reals, which S turns back into
Sequences.)
S(x)(0) = floor(x)
S(x)(n+1) = S(g(x mod 1))(n)
where x mod 1 = x - floor(x) and g(x) = x/(1-x) : [0,1) --> [0,oo) is
the inverse of f(x) = x/(1+x) : [0,oo) --> [0,1) used in the definition
of R.
As an aside for any visual thinkers reading this, the picture
[0,oo) ~ [0,1)[1,2)[2,3)...
may help. This splits [0,oo) into N unit intervals each identifiable
with [0,1), each of which is blown back up to [0,oo) (under this
identification) by g(x) = x/(1-x). The function S: [0,oo) --> N^N
converts nonnegative reals x to sequences of natural numbers by taking
the first element of the sequence to be floor(x), thereby selecting one
of the unit intervals, leaving x mod 1 to be accounted for within that
interval, of type [0,1), which is blown back up to type [0,oo) using g
and then inductively converted to the rest of the sequence by S. In
this way we drill down into [0,oo) cranking out natural numbers as we
drill progressively deeper.
For the typing N^N --> [0,1) that Dusko asked about, the codomain of R
is easily converted from [0,oo) to [0,1) by composing the monotone
bijection f : [0,oo) --> [0,1) with the monotone bijection R : N^N -->
[0,oo) to give a monotone bijection from N^N to [0,1).
In the topos of sheaves on either R itself or the subcategory of Top you
prefer, I am not a topos hacker and have no idea whether there are more
than two functions from N^N to 2 = 1+1 when N^N is defined coinductively
as a final coalgebra (as distinct from being defined simply by
exponentiation, where surely there are more than two such functions).
Toby Bartels claims it's obvious, in which case there should be a short
construction of a nonconstant function from N^N (as a final coalgebra)
to 2 (or to N, the codomain Toby spoke of) in the topos of sheaves on R.
Toby, what is it?
Vaughan Pratt
PS. None of this contradicts the point you (PTJ) and Freyd have been
making, since around 2002 apparently, concerning the constructive merits
of apartness as an implementation of the glue used in the Freyd
coalgebra, which I only very belatedly came to appreciate, namely within
the past two days. In view of this I retract my "The choice of poisons
is therefore manual glue vs. double induction" of last Wednesday. I am
willing to believe that the Freyd coalgebra with manual glue implemented
via apartness produces the "real reals" in these toposes of sheaves, but
would like eventually to understand why of course. That said, I would
still like to know whether our final coalgebra, for FX = N x X where x
is "lexicographic product" suitably defined for an NNO N in a topos, is
or is not equally real in these toposes. If it is then this would be a
situation where apartness is not needed to produce the reals
constructively, presumably contradicting Brouwer.
From rrosebru@mta.ca Wed Feb 11 09:40:49 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 09:40:49 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXFKX-00033v-FC
for categories-list@mta.ca; Wed, 11 Feb 2009 09:40:45 -0400
MIME-Version: 1.0
Date: Tue, 10 Feb 2009 13:05:26 -0800
Subject: categories: Re: "Kantor dust"
From: Greg Meredith <lgreg.meredith@biosimilarity.com>
To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>, categories@mta.ca
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Greg Meredith <lgreg.meredith@biosimilarity.com>
Message-Id: <E1LXFKX-00033v-FC@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 30
Categorically minded,
Many thanks for an interesting thread! Just out of curiousity, is the Conway
construction clearly identified with the Dedekind reals? How does the
construction fit into the constructivist debate?
Best wishes,
--greg
On Mon, Feb 9, 2009 at 2:47 PM, Prof. Peter Johnstone <
P.T.Johnstone@dpmms.cam.ac.uk> wrote:
> On Mon, 9 Feb 2009, Dusko Pavlovic wrote:
>
> QUESTION 1: re peter johnstone's
>>
>> > > In the topos of sheaves on the real line,
>>> > > every function from [0,1) to N is constant,
>>> > > yet there are obviously many other functions from N^N to N.
>>> > > Thus N^N and [0,1) are not constructively isomorphic as sets,
>>> > > so there is no way to give N^N the order type of [0,1)
>>> > > constructively.
>>>
>>
>> are you claiming that this statement is true with respect to every base
>> topos
>> and every real line in it? (the discussion seems to have touched upon the
>> various constructions of the various real lines. it would be nice to know
>> where is the one, over which you build the topos, is coming from.)
>>
>> That's actually a quote from Toby Bartels, not from me.
> It's a statement about a topos built over the classical topos of sets;
> the argument is a rather ad hoc one, and I'm not sure to what extent
> it's possible to make it constructive. However, as I said elsewhere, I
> prefer to work with the gros topos of spaces (i.e. sheaves on a suitable
> full subcategory of spaces for the coverage consisting of jointly-
> surjective families of open inclusions) and there it's quite clear
> what you need: namely, Heine--Borel (equivalently, exponentiability
> of R in your category of spaces). That's not true in all toposes;
> you could try to get round it by basing your gros topos on locales
> rather than spaces (the locale of formal reals being constructively
> locally compact), but it's not clear (to me, at least) what the
> result would actually mean if you based yourself on a topos where
> the formal reals aren't spatial.
>
> QUESTION 2: is there a branch of constructivism that would reject as
>> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as
>> the
>> coefficients of continued fractions?
>>
>> I don't think there is any doubt that the map exists. The problem is
> that,
> for most if not all schools of constructivism, it's wildly non-surjective.
>
> Peter Johnstone
>
>
>
>
--
L.G. Meredith
Managing Partner
Biosimilarity LLC
806 55th St NE
Seattle, WA 98105
+1 206.650.3740
http://biosimilarity.blogspot.com
From rrosebru@mta.ca Wed Feb 11 09:41:43 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 09:41:43 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXFLP-0003A9-Qf
for categories-list@mta.ca; Wed, 11 Feb 2009 09:41:39 -0400
Date: Tue, 10 Feb 2009 22:18:41 +0000 (GMT)
From: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
To: Greg Meredith <lgreg.meredith@biosimilarity.com>, categories@mta.ca
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
Message-Id: <E1LXFLP-0003A9-Qf@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 31
On Tue, 10 Feb 2009, Greg Meredith wrote:
> Categorically minded,
>
> Many thanks for an interesting thread! Just out of curiousity, is the Conway
> construction clearly identified with the Dedekind reals? How does the
> construction fit into the constructivist debate?
>
> Best wishes,
>
> --greg
>
The trouble with the Conway construction is not that it's non-
constructive, but that it isn't (in any reasonable sense) a
construction of the reals. If you stop it at the point when it
finally constructs the real numbers 1/3, \sqrt{2}, \pi and so
on, then it has also succeeded in constructing lots of non-real
numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how
do you distinguish the numbers you want from the ones you don't?
I did, in both my first Topos Theory book and the Elephant, borrow
Conway's recursive definition of multiplication to give a
constructively valid definition of multiplication for Dedekind reals.
I'm not aware of anyone else who has done that; but it seems to
me the only intellectually respectable way to do it.
Peter Johnstone
From rrosebru@mta.ca Wed Feb 11 09:42:23 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 09:42:23 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXFM2-0003FA-RV
for categories-list@mta.ca; Wed, 11 Feb 2009 09:42:18 -0400
Date: Tue, 10 Feb 2009 16:13:51 -0800
From: Toby Bartels <toby+categories@ugcs.caltech.edu>
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Toby Bartels <toby+categories@ugcs.caltech.edu>
Message-Id: <E1LXFM2-0003FA-RV@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 32
Steve Stevenson wrote in part:
>Toby Bartels wrote:
>>Floating-point reals have terrible theoretical properties;
>>they're not even a ring (not even classically).
>>This is why even after all of Kahan's good work on algorithms,
>>rounding errors are unavoidable (the "Table-Maker's Dilemma").
>Being left-handed and old, I'll propose in my dotage that we may be
>asking the wrong question. In a rewording, what constructive real
>numbers are there for the purpose of
>1. Being a model of an axiomatic characterization of the reals.
>2 Being usable in supercomputing to compute values needed for modeling
>and simulation.
I would distinguish two slightly different purposes:
1. Being usable in principle to compute values
2. Being usable in practice to compute values needed for modeling, etc.
And I'd say that constructive mathematics is inherently about (1),
although often (and like even classical mathematics, usually best when)
with an eye towards (2). But (2) itself is something different
(applied mathematics, to give it a name; numerical analysis straddles these.)
Although I've redefined them, I think that this remains true:
>Number 1 requires that we have nice theoretical properties. Number 2
>requires something that is bounded only the dollars and life span. Those
>interested in either purpose have (presumedly) a solution for
>themselves.
Interval arithmetic, despite being more complicated than arithemetic
with either floating-point reals or Dedekind/Cauchy/whatever reals,
is an interesting subject that promises to satisfy both (1)&(2).
This is good for both: good for (1) on the general grounds
that applied mathematics usually leads to good pure mathematics
(especially, but not only, when that mathematics is constructive);
and good for (2) since you'll have theorems that you can be sure of.
>I'm willing to
>live with a demonstrably correct approximation given that we are in an
>uncertain world.
Right, and interval arithmetic promises to get us such approximations.
There's still the question of whether demonstrably correct ones
are actually calculable in practice; that depends on the application.
At some point, you have to go beyond even interval arithmetic
and start dealing with probability distributions as your values,
which is yet more complicated theoretically but matches yet more closely
what one actually has in applications.
I'm not sure how much this has to do with category theory anymore,
but as interval arithmetic is already stretching my expertise,
I don't think that I have much more to say anyway.
--Toby
From rrosebru@mta.ca Wed Feb 11 09:43:04 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 09:43:04 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXFMg-0003Je-65
for categories-list@mta.ca; Wed, 11 Feb 2009 09:42:58 -0400
Date: Tue, 10 Feb 2009 21:49:35 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LXFMg-0003Je-65@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 33
Apropos of my
> PS. [...] That said, I would
> still like to know whether our final coalgebra, for FX = N x X where x
> is "lexicographic product" suitably defined for an NNO N in a topos, is
> or is not equally real in these toposes. If it is then this would be a
> situation where apartness is not needed to produce the reals
> constructively, presumably contradicting Brouwer.
I returned to this question after a pleasant dinner this evening with
Sol Feferman, Paul Eklof, and Grisha Mints, and it occurred to me almost
immediately (my subconscious must have been working on it without my
permission) that in a topos over any sufficient category of topological
spaces (not that I have the faintest idea how to make that rigorous), it
must be the case that the final coalgebra for the functor F described
above is the "real reals."
The intuitition behind this is that N together with an upper bound
thereon (call it oo) has only two possible T0 topologies whose
specialization order is the standard linear one, namely the Alexandroff
and Scott topologies. These differ by a single open set, which is
present in the former and absent from the latter. In the former it
isolates oo from N, in the latter its absence allows oo to link up with
N in the sense that every ultimately constant function on N must map
oo to the limiting value of that function.
There is a unique map from the Alexandroff to the Scott topology on this
set preserving the NNO structure, and no map back (where would you send
the Alexandroff open witnessing the solitude of oo?). So in any
competition for a final coalgebra Scott is going to beat Alexandroff.
Now in N^N as a representation of the isomorphism [0,oo) ~
[0,1)[1,2)[2,3)..., the objection that will naturally be raised to any
claim that this could be the continuum is that, even though [0,1)[1,2)
*looks* like it should glue together seamlessly, its implementation in
terms of continued fractions will create a gap between [0,1) and [1,2)
that is not found in the "real reals". While this gap cannot be used in
the topos Set to distinguish N^N from the Freyd coalgebra, where things
are so discrete that all realizations of the reals suffer from gaps, in
a more topologically sensitive topos it becomes possible to find open
sets willing to testify to these gaps in those cases where insufficient
care has been taken to bump off these witnesses, as surely happens when
one defines N^N naively as simply an exponential. Implementing the glue
of the Freyd coalgebra via apartness bumps off all such witnesses to the
disconnectedness of the Freyd continuum, making it thus far the sole
survivor in this competition to define the reals constructively. (If
there is another why isn't it in the Elephant?)
In any topos with sufficiently accommodating open sets as to permit this
Alexandroff-Scott distinction (surely not a tall order given that only
one open set need be removed to pass from Alexandroff to Scott), I claim
that the final coalgebra for the functor Dusko and I exhibited in our
CMCS'99 paper bumps off the Alexandroff open witnessing a gap between
[0,1) and [1,2), where the 1 in [1,2) plays the role of oo in my earlier
discussion of N and oo.
If the topos of sheaves on R, or on whichever essentially small version
of Top Peter Johnstone prefers over R itself, does not result in
removing this open set in a way that leaves no other witnesses to
disconnectedness then I will be bitterly disappointed.
If it does however then we have what as far as I'm aware must be the
first alternative since Brouwer to apartness in formulating the
continuum to the constructive standards set by toposophers. And
moreover using much older technology than the Freyd coalgebra, namely
good old continuous fractions (done right of course, none of this
antimonotone 1/(1+x) stuff totally disconnecting them).
(How old? Continued fractions are ancient, appearing in Euclid and no
doubt going back a lot further as with much of Euclidean mathematics.
They are a very natural and convenient way of representing reals, though
with subtleties to trip one up, just as with the Freyd coalgebra.)
Similar reasoning should also rehabilitate the constructivity of binary
fractions, where the final coalgebra surely deletes the open set
separating 0111... from 1000... Perhaps ASD has something to say about
this---Paul?
Vaughan Pratt
From rrosebru@mta.ca Wed Feb 11 09:43:47 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 09:43:47 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXFNN-0003O9-IK
for categories-list@mta.ca; Wed, 11 Feb 2009 09:43:41 -0400
Date: Wed, 11 Feb 2009 01:01:28 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LXFNN-0003O9-IK@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 34
Prof. Peter Johnstone wrote on Feb. 7 at 17:18 GMT:
> The reason is that you have to know in advance that a binary
> sequence isn't going to end in an infinite string of 1's; by excluding
> those sequences, you make the question "Is x < 1/2?" decidable,
> which is not constructively true of either the Cantor reals or the
> Dedekind reals.
I had always been somewhat dissatisfied intuitively by the idea of
excluding sequences of the form 01111.... It seemed more natural to
identify them with those of the form 10000.... However I just assumed
that these were equivalent approaches.
Your point about making x < 1/2 decidable is a good one. I'm now
convinced that it is better to identify than delete. Identification can
be accomplished spatially, but perhaps it is more elegant to do so
localically, namely by removing the open set that separates the two
halves to be glued together. In a T0 space, doing so will identify the
points anyway. However in the situation [0,1)[1,2) of my previous
messages where there is no point on the left adjacent to the point 1 on
the right, identification of points is not an option. The only
remaining concern then is whether there's an open set separating [0,1)
and [1,2). Finality should eliminate spurious open sets that have no
reason to stick around.
Vaughan
From rrosebru@mta.ca Wed Feb 11 09:45:18 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 09:45:18 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXFOr-0003bY-4r
for categories-list@mta.ca; Wed, 11 Feb 2009 09:45:13 -0400
Date: Wed, 11 Feb 2009 01:01:28 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LXFOr-0003bY-4r@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 35
Prof. Peter Johnstone wrote on Feb. 7 at 17:18 GMT:
> The reason is that you have to know in advance that a binary
> sequence isn't going to end in an infinite string of 1's; by excluding
> those sequences, you make the question "Is x < 1/2?" decidable,
> which is not constructively true of either the Cantor reals or the
> Dedekind reals.
I had always been somewhat dissatisfied intuitively by the idea of
excluding sequences of the form 01111.... It seemed more natural to
identify them with those of the form 10000.... However I just assumed
that these were equivalent approaches.
Your point about making x < 1/2 decidable is a good one. I'm now
convinced that it is better to identify than delete. Identification can
be accomplished spatially, but perhaps it is more elegant to do so
localically, namely by removing the open set that separates the two
halves to be glued together. In a T0 space, doing so will identify the
points anyway. However in the situation [0,1)[1,2) of my previous
messages where there is no point on the left adjacent to the point 1 on
the right, identification of points is not an option. The only
remaining concern then is whether there's an open set separating [0,1)
and [1,2). Finality should eliminate spurious open sets that have no
reason to stick around.
Vaughan
From rrosebru@mta.ca Wed Feb 11 09:45:51 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 09:45:51 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXFPP-0003gm-EN
for categories-list@mta.ca; Wed, 11 Feb 2009 09:45:47 -0400
Date: Wed, 11 Feb 2009 12:55:48 +0000
From: Alexander Kurz <kurz@mcs.le.ac.uk>
MIME-Version: 1.0
To: categories <categories@mta.ca>
Subject: categories: TACL 2009: Second Announcement and Call for Contributions
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Alexander Kurz <kurz@mcs.le.ac.uk>
Message-Id: <E1LXFPP-0003gm-EN@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 36
===============================================================================
TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2009)
===============================================================================
7-11 July 2009
Institute for Logic, Language and Computation
University of Amsterdam
the Netherlands
http://www.illc.uva.nl/tacl09/
Scope
-----
Studying logics via semantics is a well-established and very active
branch of mathematical logic, with many applications, in computer
science and elsewhere. The area is characterized by results, tools
and techniques stemming from various fields, including universal
algebra, topology, category theory, order, and model theory. The
program of the conference TACL 2009 will focus on three
interconnecting mathematical themes central to the semantical study
of logics and their applications: algebraic, categorical, and
topological methods. This is the fourth conference in the series
Topology, Algebra and Categories in Logic (TACL, formerly TANCL).
Earlier installments of this conference have been organized in
Tbilisi (2003), Barcelona (2005), and Oxford (2007).
Invited speakers
--------------------------
Martin Hyland, University of Cambridge, United Kingdom
Achim Jung, University of Birmingham, United Kingdom
Vincenzo Marra, University of Milano, Italy
Paul-Andre Mellies, University of Paris 7, France
Ieke Moerdijk, University of Utrecht, Netherlands
Ales Pultr, Charles University, Prague, Czech Republic
Lutz Schroeder, University of Bremen, Germany
Kazushige Terui, Kyoto University, Japan
Constantine Tsinakis, Vanderbilt University, USA
Featured topics
---------------
Contributed talks can deal with any topic falling under the scope of the
meeting. This includes, but is not limited to, the following areas:
* Algebraic logic
* Coalgebraic semantics
* Categorical methods in logic
* Domain theory
* Fuzzy and many-valued logics
* Lattices with operators
* Modal logics
* Non-classical logics
* Ordered topological spaces
* Ordered algebraic structures
* Pointfree topology
* Residuated structures
* Stone-type dualities
* Substructural logics
* Topological semantics of modal logic
Submissions
-----------
Contributed presentations will be of two types: 20 minutes long
presentations in parallel sessions and featured, 30 minutes long,
plenary presentations. The submission of an abstract of 1-4 pages is
required to be selected for a contributed presentation of either
kind. While preference will be given to new work, results that have
already been published or presented elsewhere will also be
considered. More information on the submission procedure is
available on the conference website.
Grants
-------------
TACL 2009 hopes to support junior and/or low budget participants whose
contributed talk proposal has been approved from the PC. This support
will take the form of fee waivers and of travel or accommodation grants.
For more information, please visit the conference website. The deadline
for grant application is April 22, 2009.
Important dates
---------------
March 15, 2009: Abstract submission deadline
April 15, 2009: Notification of authors
April 22, 2009: Grant application deadline
July 7-11, 2009: Conference
Program Committee
-----------------
Guram Bezhanishvili, New Mexico State University, USA
Nick Bezhanishvili, Imperial College London, United Kingdom
Nick Galatos, University of Denver, USA
Mai Gehrke, Radboud Universiteit, Nijmegen, Netherlands (Chair)
Rob Goldblatt, Victoria University, Wellington, New Zealand
Rosalie Iemhoff, University of Utrecht, Netherlands
Ramon Jansana, University of Barcelona, Spain
Alexander Kurz, University of Leicester, United Kingdom
Franco Montagna, University of Siena, Italy
Drew Moshier, Chapman University, USA
Hiroakira Ono, Japan Advanced Institute of Science and Technology, Japan
Yde Venema, Universiteit van Amsterdam, Netherlands
Steve Vickers, University of Birmingham, United Kingdom
Michael Zakharyaschev, Birkbeck, Universty of London, United Kingdom
More Information
----------------
If you have any queries please send them to the conference email address:
tacl09@uva.nl
===============================================================================
From rrosebru@mta.ca Wed Feb 11 21:39:38 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 21:39:38 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXQWS-0004pf-Tj
for categories-list@mta.ca; Wed, 11 Feb 2009 21:37:48 -0400
Date: Wed, 11 Feb 2009 11:55:49 -0400 (AST)
From: Toby Kenney <tkenney@mathstat.dal.ca>
To: Vaughan Pratt <pratt@cs.stanford.edu>, <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Toby Kenney <tkenney@mathstat.dal.ca>
Message-Id: <E1LXQWS-0004pf-Tj@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 37
On Tue, 10 Feb 2009, Vaughan Pratt wrote:
> As a (surely constructive!) witness to the surjectivity, indeed
> bijectivity, of R, define the inverse S: [0,oo) --> N^N of R as
> follows. (R converts sequences to Reals, which S turns back into
> Sequences.)
>
> S(x)(0) = floor(x)
> S(x)(n+1) = S(g(x mod 1))(n)
>
> where x mod 1 = x - floor(x) and g(x) = x/(1-x) : [0,1) --> [0,oo) is
> the inverse of f(x) = x/(1+x) : [0,oo) --> [0,1) used in the definition
> of R.
>
The trouble with this is that the floor function isn't constructive - the
question "is x<2" is undecidable in the reals, but decidable in the
natural numbers.
The problem with the obvious definition:
"Take the set of natural numbers below x, and take the join of this set."
is that the natural numbers don't have K~-finite joins, only K-finite
ones.
Incidentally, has anyone looked at semilattices with K~-finite joins? (Or
whatever your favourite notion of finiteness is.) Is there any use for
something like the completion of N under K~-finite joins, other than
allowing us to define the floor function?
Toby
From rrosebru@mta.ca Wed Feb 11 21:48:58 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 21:48:58 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXQh2-0005TW-QP
for categories-list@mta.ca; Wed, 11 Feb 2009 21:48:44 -0400
MIME-Version: 1.0
Date: Wed, 11 Feb 2009 10:11:44 -0600
Subject: categories: Re: "Kantor dust"
From: Michael Shulman <shulman@uchicago.edu>
To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>, categories@mta.ca
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Michael Shulman <shulman@uchicago.edu>
Message-Id: <E1LXQh2-0005TW-QP@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 38
On Tue, Feb 10, 2009 at 4:18 PM, Prof. Peter Johnstone
<P.T.Johnstone@dpmms.cam.ac.uk> wrote:
>> Many thanks for an interesting thread! Just out of curiousity, is
>> the Conway construction clearly identified with the Dedekind reals?
>> How does the construction fit into the constructivist debate?
>
> The trouble with the Conway construction is not that it's non-
> constructive, but that it isn't (in any reasonable sense) a
> construction of the reals. If you stop it at the point when it
> finally constructs the real numbers 1/3, \sqrt{2}, \pi and so
> on, then it has also succeeded in constructing lots of non-real
> numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how
> do you distinguish the numbers you want from the ones you don't?
And it isn't just "infinite" and "infinitesimal" numbers like \omega and
1/\omega that come along for the ride, either. Classically, the copy of
the natural numbers sitting inside the surreal numbers is actually the
*finite ordinal numbers*, and constructively there are many more ordinal
numbers below \omega than there are natural numbers. For instance,
{ 0 | P }
where P is an undecidable statement, is a perfectly good ordinal
number that lies "somewhere between 0 and 1."
Mike
From rrosebru@mta.ca Wed Feb 11 21:49:37 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 21:49:37 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXQhn-0005WM-0K
for categories-list@mta.ca; Wed, 11 Feb 2009 21:49:31 -0400
Date: Wed, 11 Feb 2009 17:33:59 +0000 (GMT)
From: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
To: Vaughan Pratt <pratt@cs.stanford.edu>, <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
Message-Id: <E1LXQhn-0005WM-0K@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 39
On Tue, 10 Feb 2009, Vaughan Pratt wrote:
> Apropos of my
>
>> PS. [...] That said, I would
>> still like to know whether our final coalgebra, for FX = N x X where x
>> is "lexicographic product" suitably defined for an NNO N in a topos, is
>> or is not equally real in these toposes. If it is then this would be a
>> situation where apartness is not needed to produce the reals
>> constructively, presumably contradicting Brouwer.
>
> I returned to this question after a pleasant dinner this evening with
> Sol Feferman, Paul Eklof, and Grisha Mints, and it occurred to me almost
> immediately (my subconscious must have been working on it without my
> permission) that in a topos over any sufficient category of topological
> spaces (not that I have the faintest idea how to make that rigorous), it
> must be the case that the final coalgebra for the functor F described
> above is the "real reals."
>
Whoa! This simply can't work. Whatever the final coalgebra for N x (-)
looks like, it must (thanks to Lambek) be isomorphic to N x itself,
and therefore (since equality for N is decidable) must have lots of
complemented subobjects {0} x itself, {1} x itself, ... The point of
the continuity theorem for functions R --> R is that there are toposes
in which R has *no* nontrivial complemented subobjects -- indeed, in
which the sentence
(\forall S : PR)((\forall x : R)((x \in S) \vee \neg(x\in S))
\implies ((S = R)\vee (S = \emptyset)))
is valid. This is purely a matter of logic: it has nothing to do with
the order, topological or any other sort of structure carried by
the final coalgebra. So invoking Alexandroff and Scott isn't going to
help at all. The only way to get round it (apart from using glue)
is to replace N by some "nonstandard natural number object" having no
nontrivial complemented subobjects -- but where you get that from, I
don't know.
Peter
From rrosebru@mta.ca Wed Feb 11 21:50:16 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 21:50:16 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXQiR-0005ZQ-Ux
for categories-list@mta.ca; Wed, 11 Feb 2009 21:50:11 -0400
Date: Wed, 11 Feb 2009 09:53:44 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LXQiR-0005ZQ-Ux@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 40
Vaughan Pratt wrote:
> Similar reasoning should also rehabilitate the constructivity of binary
> fractions, where the final coalgebra surely deletes the open set
> separating 0111... from 1000... Perhaps ASD has something to say about
> this---Paul?
Unfortunately the reasoning is not similar enough to make this work.
The crucial difference is that in the representation of [0,oo) ~
[0,1)[1,2)[2,3)... as N^N, there is no largest element of [0,1) whence
the Scott topology omits the open set separating [0,1) from [1,0). With
binary fractions however we have two points 0111... and 1000... with
nothing between them and the inequality 0111... < 1000..., which the
Scott topology must respect by preserving the open set separating them.
There is (as far as I'm aware) no such localic alternative of the kind I
was envisaging to either omitting 0111... or identifying it with
1000..., both of which are intrinsically spatial solutions to the
problem of converting Cantor space 2^N to the continuum. In contrast
the Alexandroff-to-Scott conversion of N^N to the continuum is localic
in character, in that it operates on open sets instead of points.
The crucial difference between classical and sheaf-theoretic toposes is
that localic procedures are meaningless in the former. The latter
permit the finer distinctions to be drawn that are needed to explicate
constructivity, starting with the distinction between not-not and identity.
(Unlike some other buggy posts of mine that I've been able to retract
before Bob forwarded them to the list, this one went through too
promptly for me to catch it in time. I made this mistake by incorrectly
visualizing the gap between 0111... and 1000... as though it were the
gap between
.0 < .01 < .011 < .0111 < ... and ... < .1000 < .100 < .10 < .1
This makes no sense (a) because the finite sequences on the right should
all be identified and (b) there are no finite sequences to begin with,
the binary fractions are properly understood as infinite sequences,
namely maps N --> 2. The paragraph was an afterthought I tacked on with
insufficient consideration before posting.)
Vaughan Pratt
From rrosebru@mta.ca Wed Feb 11 21:51:46 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 21:51:46 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXQju-0005g3-B0
for categories-list@mta.ca; Wed, 11 Feb 2009 21:51:42 -0400
MIME-Version: 1.0
Date: Wed, 11 Feb 2009 11:56:40 -0800
Subject: categories: Re: "Kantor dust"
From: Greg Meredith <lgreg.meredith@biosimilarity.com>
To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>, categories@mta.ca
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Greg Meredith <lgreg.meredith@biosimilarity.com>
Message-Id: <E1LXQju-0005g3-B0@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 41
Dr Johnstone,
Many thanks for the response. A couple of years ago, i did come up with a
scheme for sifting through the widgets generated by the Conway construction.
There's a one-liner translation of the Conway construction into a reflective
process calculus
<http://www.springerlink.com/index/f5547884k02u112q.pdf>[1]. Then,
using the
type schemes devised by Luis
Caires<http://ctp.di.fct.unl.pt/~lcaires/papers/CALCO-Caires-1.0.pdf>
,
you can use behavioral types -- in principle -- to sort through the gadgets
the Conway construction generates.
This idea shares much of the spirit of the work done by Mads Dam on proof
systems for the pi-calculus <http://www.csc.kth.se/~mfd/Papers/pspcl.pdf> in
his examples of logical specifications of process models of the naturals --
though to the best of my knowledge he never applied his ideas to the Conway
construction. i cooked up this hair-brained idea in search of a more natural
typing of a notion of quantity that is grounded in a conception of computing
that i know how to reduce to practice.
Best wishes,
--greg
[1] i'm ignoring a bunch of issues about which domain you use to solve the
domain equations that present the reflective process calculus -- which
impact how wide your summations and parallel compositions can be, which
impact how wide the left and right side of the Conway games can be. But,
therein lies at least on connection to category theory. Be that as i may,
here is the 1-liner translation
[| G |] =
\Sigma_{G^L} @ [| G^L |] ?(x)(*x | [| G^L |]) | \Sigma_{G^R} @ [| G^R |]!(
[| G^L |] )
The syntax of the reflective calculus that is the target of this translation
is given below
P,Q ::= 0 | x?A | x!C | *x | P+Q
A ::= (y1,...,yN)P, C ::= (P1,...,PN)
x,y ::= @P
See the link above for a brief account of the calculus and a corresponding
logic.
i should note that the translation is horrifically inefficient and it was
wading through the different optimizations -- while preserving nice
compositional properties of the translation so that the definitions and
proofs given by Conway easily port over through the translation to natural
operations on the process models -- that sapped my motivation.
On Tue, Feb 10, 2009 at 2:18 PM, Prof. Peter Johnstone <
P.T.Johnstone@dpmms.cam.ac.uk> wrote:
> On Tue, 10 Feb 2009, Greg Meredith wrote:
>
> Categorically minded,
>>
>> Many thanks for an interesting thread! Just out of curiousity, is the
>> Conway
>> construction clearly identified with the Dedekind reals? How does the
>> construction fit into the constructivist debate?
>>
>> Best wishes,
>>
>> --greg
>>
>> The trouble with the Conway construction is not that it's non-
> constructive, but that it isn't (in any reasonable sense) a
> construction of the reals. If you stop it at the point when it
> finally constructs the real numbers 1/3, \sqrt{2}, \pi and so
> on, then it has also succeeded in constructing lots of non-real
> numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how
> do you distinguish the numbers you want from the ones you don't?
>
> I did, in both my first Topos Theory book and the Elephant, borrow
> Conway's recursive definition of multiplication to give a
> constructively valid definition of multiplication for Dedekind reals.
> I'm not aware of anyone else who has done that; but it seems to
> me the only intellectually respectable way to do it.
>
> Peter Johnstone
>
From rrosebru@mta.ca Wed Feb 11 21:52:38 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 21:52:38 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXQkl-0005ko-Dn
for categories-list@mta.ca; Wed, 11 Feb 2009 21:52:35 -0400
From: "Bhupinder Singh Anand" <re@alixcomsi.com>
To: "'Paul Taylor'" <pt09@PaulTaylor.EU>, <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Date: Thu, 12 Feb 2009 03:46:00 +0530
MIME-Version: 1.0
Content-Type: text/plain;charset="US-ASCII"
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Bhupinder Singh Anand" <re@alixcomsi.com>
Message-Id: <E1LXQkl-0005ko-Dn@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 42
On Sunday, February 08, 2009 8:33 PM, Paul Taylor wrote in Categories:
" ... people should be clear about WHICH OF MANY "CONSTRUCTIVE" THEORIES OF
MATHEMATICS they mean as the context of their comments. ... If you want to
construct Cantor space from the reals by the "missing third" construction, I
would think that it makes little difference whether you start from Cauchy or
Dedekind."
Actually, there seem to be two issues involved here.
The minor of the two: that the "missing third" construction yields a
'limit', namely the "Kantor dust";
The other: whether we can agree on any 'constructive' concept at all, such
as, say, the standard interpretation of first-order Peano Arithmetic.
As to the first: Consider an equilateral triangle ABC of height h and side
s. Divide the base AC in half and construct two isosceles triangles of
height h.d and base s/2, where 1>d>0. Iterate the construction on each
constructed triangle ad infinitum.
If the "Kantor dust" is a legitimate (fractal) set, then this construction,
too, should yield a limiting configuration.
Since the height of the constructed triangles at the n'th construction is
h(d^n), and 1>d>0, it would seem that the base AC of the original
equilateral triangle will always be the limiting configuration of the
opposing sides.
This is indeed so if 1/2>d>0, since the total length of the opposing sides
is a Cauchy sequence whose limiting value is, indeed, the length s of the
base AC.
However, if d=1/2, the total length of all the sides opposing their base on
AC is always 2s!
Moreover, if d>1/2, the total length of all the sides opposing their base on
AC is a monotonically increasing value.
(To give it a practical flavour, let s be one light-year, and consider how
long it would take a light signal to travel from A to C along the sides
opposing the base in each of the above cases; and whether it makes any sense
to assert that all the cases must have a limiting configuration.)
So, whatever it is that the "missing third" construction is supposed to
yield, it certainly cannot have any relation to the terms "third",
"construction", "limit" and "set" under any interpretation of these terms
that we normally conceive of in mathematics.
The issue - as Thoralf Skolem emphasised in "Some remarks on axiomatized set
theory", delivered in an address before the Fifth Congress of Scandinavian
Mathematicians in Helsinki, 4-7 August 1922, with respect to the the Axiom
of Choice - is that set-theory admits statements that are essentially
non-verifiable under any conceivable interpretation; statements, moreover,
which do not express any definable content and cannot, therefore, be
expected to communicate any meaningful information unambiguously under
interpretation:
"So long as we are on purely axiomatic ground there is, of course, nothing
special to be remarked concerning the principle of choice (though, as a
matter of fact, new sets are not generated univocally by applications of
this axiom); but if many mathematicians---indeed, I believe, most of
them---do not want to accept the principle of choice, it is because they do
not have an axiomatic conception of set theory at all. They think of sets as
given by specification of arbitrary collections; but then they also demand
that every set be definable. We can, after all, ask: What does it mean for a
set to exist if it can perhaps never be defined? It seems clear that this
existence can be only a manner of speaking, which can lead only to purely
formal propositions---perhaps made up of very beautiful words---about
objects called sets. But most mathematicians want mathematics to deal,
ultimately, with performable computing operations and not to consist of
formal propositions about objects called this or that."
That the problem lies deeper - in fact at the very core of our fundamental
assumptions - is seen if we note that our logical thinking is universally
founded upon the validity of Aristotle's particularisation.
This holds that an assertion such as, 'There exists an x such that F(x)
holds'---usually denoted symbolically by '(Ex)F(x)'---can be validly
inferred in the classical logic of predicates from the assertion, 'It is not
the case that, for any given x, F(x) does not hold'---usually denoted
symbolically by '~(Ax)~F(x)'.
Now, in his 1927 address, Hilbert reviewed in detail his axiomatisation of
classical Aristotlean predicate logic as a formal first-order
epsilon-predicate calculus, in which he used a primitive choice-function
symbol, 'epsilon', for defining the quantifiers 'for all' and 'exists'.
In an earlier address "On The Infinite", delivered in Munster on 4th June
1925 at a meeting of the Westphalian Mathematical Society, Hilbert had shown
that the formalisation proposed by him would adequately express Aristotle's
logic of predicates if the epsilon-function was interpreted to yield
Aristotlean particularisation.
This, as Hilbert remarked in his 1927 address, was what he had set out to
achieve as part of his 'proof theory':
"... The fundamental idea of my proof theory is none other than than to
describe the activity of our understanding, to make a protocol of the rules
according to which our thinking actually proceeds."
What came to be known later as Hilbert's Program---which was built upon
Hilbert's 'proof theory'---can be viewed as, essentially, the subsequent
attempt to show that the formalisation was also necessary for communicating
Aristotle's logic of predicates effectively and unambiguously under any
interpretation of the formalisation.
This goal is implicit in Hilbert's remarks:
"Mathematics in a certain sense develops into a tribunal of arbitration, a
supreme court that will decide questions of principle---and on such a
concrete basis that universal agreement must be attainable and all
assertions can be verified."
"... a theory by its very nature is such that we do not need to fall back
upon intuition or meaning in the midst of some argument."
The difficulty in attaining this goal constructively along the lines desired
by Hilbert---in the sense of the above quotes---lies in the fact that, as
Rudolf Carnap emphasised in a 1962 paper, "On the use of Hilbert's
epsilon-operator in scientific theories", the Axiom of Choice is formally
derivable as a theorem in a set theory ZF_epsilon, which is, essentially,
Zermelo-Fraenkel set theory where the quantifiers are defined in terms of
Hilbert's epsilon-function.
The significance of this lies in the accepted interpretation of Paul Cohen's
argument in his 1963-64 papers; they are primarily taken as definitively
establishing that the Axiom of Choice is independent of a set theory such as
ZF.
Now, Cohen's argument---in common with the arguments of many important
theorems in standard texts on the foundations of mathematics and
logic---appeals to Aristotle's particularisation when interpreting the
existential axioms of ZF (or statements about ZF ordinals) in the
application of the seemingly paradoxical (downwards) Lowenheim-Skolem
Theorem for legitimising putative models of a language (such as the standard
model 'M' of ZF, and its forced derivative 'N', in Cohen's argument).
Thus, Cohen's argument should really be taken to establish that, not only is
Aristotle's particularisation 'stronger' than the Axiom of Choice, but that
there is no sound interpretation of ZF that can appeal to Aristotle's
particularisation.
Moreover, the larger significance of Hilbert's formalisation of Aristotle's
particularisation is that---in formal languages that prefer the more
familiar '[A]' - as in '[(Ax)]' - as a primitive symbol to Hilbert's more
logical choice function 'epsilon'---it implicitly gives formal legitimacy to
Alfred Tarski's standard definitions of the satisfaction, and truth, of the
formulas of a formal language under an interpretation, since these
definitions faithfully mirror the particular interpretation of Hilbert's
formalisation that appeals to Aristotle's particularisation.
The reason: Under Tarski's definitions, the formally defined logical
constant '[E]' in an occurrence such as '[(Ex)]'---which is formally defined
in terms of the primitive (undefined) logical constant '[Ax]' as '[~(Ax)~
...]'---always appeals to an interpretation such as 'There is some x such
that ...' in any formal first-order mathematical language.
In other words, Tarski's definitions ensure that, if the first-order
predicate calculus of a first-order mathematical language admits
quantification, then any putative model of the language must interpret
existential quantification as Aristotle's particularisation.
Selecting such a strong interpretation---i.e., one which favours Aristotle's
particularisation---for the standard interpretation, say S, of the formal
Peano Arithmetic PA has significant consequences.
For instance, if we accept the logical validity of such interpretation, then
S is sound (i.e., every PA-theorem interprets as true under S.
Further, if S is sound, then PA is omega-consistent (i.e., we cannot have a
PA-formula [F(x)] such that [F(n)] is PA-provable for any given PA-numeral
[n], and [~(Ax)F(x)] is also PA-provable).
Now, in his seminal 1931 paper, Godel showed that if a Peano Arithmetic such
as his formal system P is omega-consistent, then it is incomplete, in the
sense that he could constructively define a P-formula [R(x)] such that
neither [(Ax)R(x)] nor [~(Ax)R(x)] are P-provable.
However, he also showed in this paper that if P is consistent and [(Ax)R(x)]
is assumed P-provable, then [~(Ax)R(x)] is P-provable.
By Godel's definition of P-provability, it follows that there is a finite
sequence [F_1], ..., [F_n] of P-formulas such that [F_1] is [Ax)R(x)], [F_n]
is [~(Ax)R(x)], and, for 2=< i =< n, [F_i] is either a P-axiom or a logical
consequence of the preceding formulas in the sequence by the rules of
inference of P.
Now, a proof sequence of P necessarily interprets as a sound deduction
sequence under any sound interpretation of P. It follows that we cannot have
a sound interpretation of P under which [(Ax)R(x)] interprets as true and
[~(Ax)R(x)] as false.
Since both [(Ax)R(x)] and [~(Ax)R(x)] are closed P-formulas, it follows that
the P-formula [(Ax)R(x) => ~(Ax)R(x)] interprets as true under every sound
interpretation of P.
By Godel's completeness theorem, [(Ax)R(x) => ~(Ax)R(x)] is, therefore,
P-provable; whence [~(Ax)R(x)] is P-provable.
Since Godel also showed that, if P is consistent, then [R(n)] is P-provable
for any given P-numeral [n], it follows that P is not omega-consistent.
Since Godel's argument holds in PA, we further have that the standard
interpretation S of PA is not sound; moreover, no sound interpretation of PA
can appeal to Aristotle's particularisation!
Thus the difficulty in agreeing upon the concept of a 'constructive' theory
is deep-rooted in our dependence on Aristotle's logic of predicates which,
whilst allowing us the luxury of expressing the most subjectively conceived
of our abstract concepts not only in languages of common discourse such as
English, but also in mathematical languages such as ZF, is inadequate for
ensuring that that which we express in the most basic of our mathmatical
languages, namely Peano Arithmetic, can be communicated effectively and
unambiguously.
That a sound interpretation of Peano Arithmetic exists - moreover, one that
allows us to communicate effectively and unambiguously - is indicated by the
fact that we unhesitatingly entrust our lives each moment of each day to
mechanical and electronic artefacts whose reliability is essentially founded
on the ability of PA to admit unambiguous and effective communication.
Accordingly, in a recently arXived paper (link below), I consider a
weakened, finitary, interpretation B (of an omega-inconsistent PA) which
avoids appealing to Aristotlean particularisation in the interpretation of
the existential quantifier, and which is actually implicit in Turing's 1936
analysis of computable functions.
This is the interpretation B of PA obtained if, in Tarski's inductive
definitions---of the satisfaction and truth of the formulas of PA under the
'standard' interpretation S of PA---we apply Occam's razor and weaken the
definition of subjective Tarskian satisfiability by replacing it with an
algorithmically verifiable definition of objective Turing-satisfiability.
Not only is the interpretation sound, but it implies that PA is categorical;
we can thus, in principle, communicate perfectly with technologically
advanced extra-terrestrial intelligences.
http://arxiv.org/PS_cache/arxiv/pdf/0902/0902.1064v3.pdf
Regards,
Bhup
From rrosebru@mta.ca Wed Feb 11 21:53:17 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 11 Feb 2009 21:53:17 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXQlN-0005oB-Eg
for categories-list@mta.ca; Wed, 11 Feb 2009 21:53:13 -0400
Date: Wed, 11 Feb 2009 15:51:06 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: Categories mailing list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LXQlN-0005oB-Eg@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 43
Prof. Peter Johnstone wrote:
> Whoa! This simply can't work. Whatever the final coalgebra for N x (-)
> looks like, it must (thanks to Lambek) be isomorphic to N x itself,
> and therefore (since equality for N is decidable) must have lots of
> complemented subobjects {0} x itself, {1} x itself, ... The point of
> the continuity theorem for functions R --> R is that there are toposes
> in which R has *no* nontrivial complemented subobjects [...]
> The only way to get round it (apart from using glue)
> is to replace N by some "nonstandard natural number object" having no
> nontrivial complemented subobjects -- but where you get that from, I
> don't know.
You're assuming product distributes over sums, which would be true for
ordinary product but I specified lexicographic product, with the left
argument as the "high order digit" (converse of the usual convention for
ordinal product in ordinal arithmetic). Why should {0} x N be a
complemented subobject of N x N when lexicographic product attaches the
"end" of it to {1} x {0} , which I would expect it will in a topos of
sheaves when participating in a final coalgebra for N x X.
Vaughan
From rrosebru@mta.ca Thu Feb 12 22:09:32 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 12 Feb 2009 22:09:32 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXnRU-0000GI-UJ
for categories-list@mta.ca; Thu, 12 Feb 2009 22:06:12 -0400
MIME-Version: 1.0
Subject: categories: Fields Workshop on Smooth Structures - Accommodation
Date: Wed, 11 Feb 2009 22:29:01 -0500
From: "Pieter Hofstra" <phofstra@uottawa.ca>
To: <categories@mta.ca>
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Pieter Hofstra" <phofstra@uottawa.ca>
Message-Id: <E1LXnRU-0000GI-UJ@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 44
Fields Workshop on Smooth Structures in Logic, Category Theory and =
Physics=20
May 1-3 2008, Ottawa
***
Since the weekend of the Workshop coincides with the annual Tulip =
Festival (which attracts many tourists) it will be difficult and =
expensive to find accommodation in town. We have therefore reserved =
rooms at two nearby hotels (at a discount rate) as well as a few units =
in the University Residence. We can hold these rooms until April 1st, so =
we recommend those who intend to attend the workshop to book as soon as =
possible in order to avoid disappointment. Information about these =
hotels can be found on the local web page:
http://aix1.uottawa.ca/~scpsg/Fields09/Fields09.smoothworkshop.html
Best regards,
R. Blute
P. Hofstra
P. Scott
M. Warren
From rrosebru@mta.ca Thu Feb 12 22:09:32 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 12 Feb 2009 22:09:32 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXnSB-0000Ix-5J
for categories-list@mta.ca; Thu, 12 Feb 2009 22:06:55 -0400
Date: Wed, 11 Feb 2009 20:05:50 -0800
From: Toby Bartels <toby+categories@ugcs.caltech.edu>
To: categories list <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Toby Bartels <toby+categories@ugcs.caltech.edu>
Message-Id: <E1LXnSB-0000Ix-5J@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 45
Vaughan Pratt wrote in part:
>Toby Bartels claims it's obvious, in which case there should be a short
>construction of a nonconstant function from N^N (as a final coalgebra)
>to 2 (or to N, the codomain Toby spoke of) in the topos of sheaves on R.
> Toby, what is it?
An element s of N^N as a final coalgebra of X |-> N x X
decomposes into an element s0 of N and an element s+ of N^N.
In this notation, the easiest of the desired functions is s |-> s0.
Other functions N^N -> N include s |-> s+0, s++0, ...; there are more.
This can be done in any topos (actually in more categories than that).
If any of these is constant, then N is a terminal object,
so if it's an NNO (as it should be to justify the notation N^N)
we are in the terminal category (the inconsistent topos).
--Toby Bartels
From rrosebru@mta.ca Thu Feb 12 22:09:32 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 12 Feb 2009 22:09:32 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXnTL-0000Nn-6h
for categories-list@mta.ca; Thu, 12 Feb 2009 22:08:07 -0400
Date: Wed, 11 Feb 2009 20:25:25 -0800
From: Toby Bartels <toby+categories@ugcs.caltech.edu>
To: categories@mta.ca
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Toby Bartels <toby+categories@ugcs.caltech.edu>
Message-Id: <E1LXnTL-0000Nn-6h@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 46
Dusko Pavlovic wrote in part:
[Prof. Johnstone responded to most of this, but I want to address one point.]
>there are
>many things that need to be computed with the reals, and no one
>representation fits for all purposes. so the statement
>>nobody uses the binary reals
>probably has more counterexamples than, say, the statement "nobody
>uses toposes". even if "the" binary reals were completely wrong.
What I meant is that no practising constructivist accepts
that the binary reals are the (or a) good notion of real number,
especially since no practising constructivist believes they form a ring.
I don't intend this as a dogamatic statement, and I'd be very interested
to here of any exceptions, but nevertheless I believe that it is true.
I certainly don't mean that nobody, not even a constructivist,
uses the binary reals as an approximation to real numbers
for the purposes of convenient calculations.
And of course, classical mathematicians do believe
that the binary reals are (all of) the reals.
As I suggested in a reply to Steve Stevenson,
constructive mathematics is about what can in principle be computed exactly.
What can in practice be computed closely enough is another question,
quite a useful one to ask but not at all the same thing.
(And what can in practice be computed exactly is another good question,
one that I'm interested in but don't know enough about.)
--Toby
From rrosebru@mta.ca Thu Feb 12 22:09:32 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 12 Feb 2009 22:09:32 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXnSi-0000Ku-Od
for categories-list@mta.ca; Thu, 12 Feb 2009 22:07:28 -0400
Date: Wed, 11 Feb 2009 20:10:47 -0800
From: Toby Bartels <toby+category@ugcs.caltech.edu>
To: categories@mta.ca
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Toby Bartels <toby+category@ugcs.caltech.edu>
Message-Id: <E1LXnSi-0000Ku-Od@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 47
Prof. Peter Johnstone wrote in part:
>The trouble with the Conway construction is not that it's non-
>constructive, but that it isn't (in any reasonable sense) a
>construction of the reals. If you stop it at the point when it
>finally constructs the real numbers 1/3, \sqrt{2}, \pi and so
>on, then it has also succeeded in constructing lots of non-real
>numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how
>do you distinguish the numbers you want from the ones you don't?
Can you get anywhere by imposing (at that stage) some Archimedean conditions?
We need to know first how to interpret natural numbers as Conway numbers,
then take the subset of those x such that -n < x < n for some n,
and identify x and y if -1 < (x-y)n < 1 for every n.
--Toby
From rrosebru@mta.ca Thu Feb 12 22:10:28 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 12 Feb 2009 22:10:28 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXnU8-0000Qq-4F
for categories-list@mta.ca; Thu, 12 Feb 2009 22:08:56 -0400
Date: Thu, 12 Feb 2009 09:00:58 +0000 (GMT)
From: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
To: Vaughan Pratt <pratt@cs.stanford.edu>, <categories@mta.ca>
Subject: categories: Re: "Kantor dust"
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
Message-Id: <E1LXnU8-0000Qq-4F@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 48
On Wed, 11 Feb 2009, Vaughan Pratt wrote:
> Prof. Peter Johnstone wrote:
>> Whoa! This simply can't work. Whatever the final coalgebra for N x (-)
>> looks like, it must (thanks to Lambek) be isomorphic to N x itself,
>> and therefore (since equality for N is decidable) must have lots of
>> complemented subobjects {0} x itself, {1} x itself, ... The point of
>> the continuity theorem for functions R --> R is that there are toposes
>> in which R has *no* nontrivial complemented subobjects [...]
>> The only way to get round it (apart from using glue)
>> is to replace N by some "nonstandard natural number object" having no
>> nontrivial complemented subobjects -- but where you get that from, I
>> don't know.
>
> You're assuming product distributes over sums, which would be true for
> ordinary product but I specified lexicographic product, with the left
> argument as the "high order digit" (converse of the usual convention for
> ordinal product in ordinal arithmetic).
For goodness' sake, Vaughan! How many times do I have to tell you that
I'm talking about *the underlying object* of the final coalgebra, and
not its order structure or its topology? If the underlying object of
the lexicographic product is the ordinary (cartesian) product -- and
if it's not, then I don't know what it is -- then it distributes over
sums because that's what products do in a topos.
> Why should {0} x N be a
> complemented subobject of N x N when lexicographic product attaches the
> "end" of it to {1} x {0} , which I would expect it will in a topos of
> sheaves when participating in a final coalgebra for N x X.
>
The order structure can't do any sort of "attaching" that negates the
complementedness of the underlying subobject, and neither can the
topology. The only thing that can do that is to make identifications
between endpoints -- i.e. to use "glue" a la Freyd.
Peter
From rrosebru@mta.ca Thu Feb 12 22:10:57 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 12 Feb 2009 22:10:57 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXnUu-0000Td-EH
for categories-list@mta.ca; Thu, 12 Feb 2009 22:09:44 -0400
From: Bas Spitters <spitters@cs.ru.nl>
To: "Galchin, Vasili" <vigalchin@gmail.com>
Subject: categories: Re: "Kantor dust"
Date: Thu, 12 Feb 2009 10:05:10 +0100
MIME-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Bas Spitters <spitters@cs.ru.nl>
Message-Id: <E1LXnUu-0000Td-EH@mailserv.mta.ca>
Status: RO
X-Status:
X-Keywords:
X-UID: 49
Let me use this as an excuse to advertise the work of Russell O'Connor, who is
about to complete a PhD in Nijmegen working with me.
O'Connor's project was to implement exact real numbers in type theory in a
machine verified way. His implementation is fairly efficient and completely
verified in the Coq proof assistant.
Real numbers are implemented using (a variant of) Cauchy sequences. He used
the completion monad on metric spaces to write a Haskell-style "effectful"
functional program in Coq (http://arxiv.org/abs/cs/0605058).
He combined the same monad with the list monad to obtain an implementation of
compact sets (pictures, graphs, i.e. Cantor set).
http://arxiv.org/abs/0806.3209
Together we implemented the Riemann integral by combining the step function
monad with the completion monad:
http://arxiv.org/abs/0809.1552
It was very pleasant to see how much category theory pops up naturally when
one tries to implement exact real numbers in a certified way.
To come back to your question: there is a *certified implementation* of
compact sets of the plane. Cantor set is an example of this.
O'Connor's paper includes much more discussion than what I would like to
repeat here. I recommend it.
Bas
On Friday 30 January 2009 08:18:39 Galchin, Vasili wrote:
> [Note from moderator: this may have been sent incorrectly earlier,
> apologies if you have received it twice.]
>
> Dear Category group,
>
> Here is a definition of Cantor dust ....
> http://en.wikipedia.org/wiki/Cantor_set.
>
> My question is from a constructivist viewpoint does this set really
> exist and if so, why?
>
> Very kind regards,
>
> Vasili
From rrosebru@mta.ca Thu Feb 12 22:12:39 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 12 Feb 2009 22:12:39 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXnWQ-0000bX-Fe
for categories-list@mta.ca; Thu, 12 Feb 2009 22:11:18 -0400
Mime-Version: 1.0 (Apple Message framework v624)
Content-Transfer-Encoding: 7bit
Content-Type: text/plain; charset=US-ASCII; format=flowed
To: Categories list <categories@mta.ca>
From: Paul Taylor <pt09@PaulTaylor.EU>
Subject: categories: Dedekind versus Cauchy reals
Date: Thu, 12 Feb 2009 12:54:07 +0000
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Paul Taylor <pt09@PaulTaylor.EU>
Message-Id: <E1LXnWQ-0000bX-Fe@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 50
I wanted to reply to what Toby Bartells and Thomas Streicher said
in response to my challenge to say why Cauchy sequences are often
preferred to Dedekind cuts as constructions of the real line.
However, I made the mistake of trying to read through the whole thread,
so I'm afraid this posting has ended up in a somewhat rambling state.
Also, I shall postpone the discussion of why DEDEKIND reals are
good for COMPUTATION to another posting.
NOTE TO ANYONE READING THIS IN AN ARCHIVE:
There have been numerous very interesting contributions to this thread
from Toby Bartels, Giovanni Curi, Peter Johnstone, Dusko Pavlovic,
Vaughan Pratt, Steve Stevenson and others, but many of them have been
posted under Subject: lines including the words
Kantor dust
This is an excellent thread, though unfortunately on the wrong mailing
list. But I know that Peter Schuster reads "categories", so maybe he
will chip in from the point of view of Bishop's constructive analysis.
Some quick answers to various people's questions first.
When I have spoken about "CONSTRUCTIONS" of the real line or of Cantor
space, I mean the word in the usual non-formal mathematical sense, not
according to any doctrine of constructivity.
Even in a particular system, I don't think it makes sense to say
whether the "construction" of a SPACE takes finite time. We can ask
such questions (and, in more detail, about "complexity") for
computations of INTEGERS FROM INTEGERS. Some people, in particular
some of those who take part in "Computability and Complexity in
Analysis", claim that this question is meaningful for REAL NUMBERS.
But for OBJECTS, I don't see that it has any clear meaning.
Toby Bartels said that the "UNDERLYING-SET AXIOM" in ASD is
impredicative.
This is correct, but I introduced this axiom as a "straw man".
First, in order to say exactly what is needed to make ASD equivalent
to (locally compact locales over) an elementary topos.
Second, to make the point that a great deal of mainstream mathematics
is computable and does NOT require underlying sets. I see the main
thread of ASD as being about a computable theory.
Toby has also said a lot of interesting things about many different
systems. These illustrate my point that it is essential to state
which system, or which notion of "constructivity" you intend.
He has said, for example
* The Dedekind reals can also be constructed in CZF (Peter Aczel's
predicative constructive set theory) even if you remove countable
choice, using subset collection aka fullness.
* Similarly, if you remove identity types from intensional type theory
(so breaking the justification of countable choice), you can still
justify the fullness axiom and so construct the Dedekind reals
(albeit not literally as sets of rational numbers).
* The Cauchy reals exist an a Pi-W-pretopos (equivalently, in a
constructive set or type theory with exponentiation but no power
sets or even fullness and with infinity but no countable choice).
* But the Dedekind reals, as far as [he] can tell, do not; excluded
middle, power sets, fullness, or countable choice would each do the
job, but you need ~something~.
I would challenge someone to consider the last of these questions
seriously, maybe taking a hint from the second. ASD provides another,
as it uses lambda term over a special object instead of talking about
"sets" of rational numbers.
Peter Johnstone, on the other hand, has referred to the fact that both
constructions exist in the topos-theoretic context, and are in general
different. I don't want to put words into Peter's mouth, but a lot of
evidence from "ordinary mathematics" says that the Dedekind reals are
preferable.
Giovanni Curi has also described the situation in several settings,
apparently coming down on the side of Dedekind. (I am citing other
people's postings primarily in order to encourage readers to read
throught the thread.)
The reason why we need to be clear about the different systems is that
the mathematical results are DIFFERENT in them, in INTERESTING ways.
It is very easy to adopt the habit of taking a particular system as
given, and then asserting or denying that some theorem is
"constructive", as a judgement about the THEOREM. However, they are
typically headline results from mainstream mathematics, so it is the
SYSTEM and not the theorem that is under scrutiny.
In particular, I would like to turn the tables on the predicativists.
A lot of excellent mathematics has been done in Martin-Lof type theory.
More recently, certain categorists have been inspired by this to study
"Pi-W-pretoposes" (which surely deserve a better name).
But these theories pick a few items from the (by Godel's theorem,
inexhaustible) collection of possible type-forming operations.
Two questions naturally arise:
* Why do you consider that the axioms that you have chosen are
legitimate?
* Why stop with them?
For example, the recent debate amongst various constructive
disciplines has shown that it is valuable to set down explicit rules
about WHICH JOINS one may legitimately form in the lattice of open
subspaces of a space:
* In locale theory, one can form "all" of them, or, from a more
constructive point of view, "enough" of them to obtain right adjoints
such as Heyting implication and the direct image f_*.
* In ASD, the indexing objects of legitimate joins are called OVERT.
You can take this as a tautologous definition, in which case the
notion of "overtness" is variable and might, for example, be extended
by introducing ORACLES.
* In Formal Topology, the ability to form unions is governed by
Martin-Lof Type Theory, wherein the "sets" (over which we may
form unions) are closed under implication. (At least, I believe
that this is the case - no doubt someone will correct me if not.)
From a computational point of view, this is a questionable thing to
do (hence my first question).
* Algebraic Set Theory has an axiomatisation based on the properties
of OPEN MAPS. The latter are the same as families of overt spaces,
in the same way that proper maps are families of compact spaces.
Various workers on AST have augmented these axioms, explicitly
with the purpose of including different LOGICAL connectives.
So why not consider the TYPE OF DEDEKIND REALS too?
This is a perfectly serious suggestion, and indeed it is precisely
what Andrej Bauer and I have been doing. Dedekind completeness is
a rule for INTRODUCING real numbers, given pairs of predicates,
whilst the Heine--Borel theorem introduces quantified predicates.
See
www.PaulTaylor.EU/ASD/analysis.html
for a summary of this SYNTACTIC theory, along with the papers that
develop it.
I intend to answer Thomas Streicher's "pragmatic" reasons for
computing with Cauchy sequences in a separate posting, but I'd
like to pick out the "foundational" part here:
> AC_N of course allows you to magically find a modulus of convergence
> for every Cauchy sequence. But like Church's Thesis or Brouwer's
> Theorem this is sort of a Deus ex machina (actually those are 2
> contradictory dei ex machina!) and thus of moderate help for exact
> computation on the reals.
(Do you see what I mean by "heresy"?)
The alleged conflict between Church's Thesis and Brouwer's Theorem
(I would prefer to say the Heine--Borel theorem) is in fact exactly the
point at which Andrej Bauer and I began our collaboration, in November
2004. He asked me whether I believed both of these things, which I
said I did, and he progressively took me through the construction of
the Kleene Tree -- to the point of contradiction.
Of course, I wasn't going to accept that, so we back-tracked, and
in particular I set out what I meant by Church's thesis. I think
this formulation is in Pino Rosolini's thesis, and it is proved
for ASD in "Scott domains in ASD" (rejected by CTCS 2002).
There is a map p:N->Sigma^N that is "universal" in the (weak) sense
that, for any map f:N->Sigma^N, there is some (not necessarily unique)
fill-in q:N->N with f=p.q:
> N
. |
. |p
q. |
. |
. V
. f V
N---------> Sigma^N
I forget how the conversation with Andrej went on from that point,
but shortly afterwards he wrote down the Dedekind cut for the supremum
of a non-empty compact overt subspace of R. Our construction of R took
off from there.
This "conflict between Church's Thesis and Brouwer's Theorem"
illustrates another important principle about the methodology of
mathematics:
COUNTEREXAMPLES CLOSE MINDS
When someone demonstrates a counterexample, what they legitimately
prove is typically
D, E, F |- not G.
Then they assert "not E", after which an entire discipline gets built
on the failure of E. Cantor's theorem about the non-isomorphism of
a set with its powerset is perhaps the dominant example of this.
This is an "argument by authority", one of the principal fallacies of
logic.
For one thing, D, E, F and G play symmetrical roles in the argument,
so why pick on E as the erroneous assumption?
Eventually, some heretic comes along and points out that this proof
makes other assumptions A, B and C. By substituting different ideas,
A', B' and C', they manage to show that these and D, E, F and G can
validly co-exist. However, because of the pernicious influence of the
counterexample on other people's minds, it is very difficult for the
new ideas to get a hearing.
Finally, a footnote about CONWAY'S NUMBERS.
As Peter Johnstone has already pointed out, these include the ordinals.
However, the traditional theory of the ordinals depends VERY HEAVILY
on excluded middle. The intuitionistic theory is therefore rather
complicated and, in particular, there are several different kinds of
intuitionistic ordinals, for which see
"Intuitionistic Sets and Ordinals" by Paul Taylor, JSL 61 (1996).
"Algebraic Set Theory" by Andre Joyal and Ieke Moerdijk, CUP 1996?
and my web page www.PaulTaylor.EU/ordinals/.
This means that the intuitionistic version of Conway numbers would be
even more complicated, although Frank Rosemeier made a start in
"A Constructive Approach to Conway's Theory of Games" in
"Reuniting the Antipodes: Constructive and Nonstandard Views
of the Continuum}, Peter Schuster, Ulrich Berger and Horst Osswald
(eds), Springer-Verlag, 2001.
There are further remarks on the interaction amongst Dedekind
completeness,
the Archimedean property and Conway's numbers at the end of section 12
of "The Dedekind reals in ASD".
Paul Taylor
From rrosebru@mta.ca Thu Feb 12 22:12:55 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 12 Feb 2009 22:12:55 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LXnX2-0000fe-Lh
for categories-list@mta.ca; Thu, 12 Feb 2009 22:11:56 -0400
MIME-Version: 1.0
Date: Fri, 13 Feb 2009 01:07:08 +0100
Subject: categories: Re: Dedekind versus Cauchy reals
From: Andrej Bauer <andrej.bauer@andrej.com>
To: categories@mta.ca, Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Andrej Bauer <andrej.bauer@andrej.com>
Message-Id: <E1LXnX2-0000fe-Lh@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 51
This is a reply to Thomas's post about "Dedekind vs. Cauchy". I am too
young to know why Cauchy reals were preferred by the early
constructivists, so I will reply only to remarks that regard
real-number computation, of which I have more experience.
Thomas gives pragmatic reasons for preferring Cauchy sequences,
actually the rapid ones, with rate of convergence 2^-n. Given a rapid
Cauchy sequence we can easily get an approximation to any desired
degree. On the other hand, Thomas says, a Dedekind real is implemented
as a semidecision procedure, which forces us to _guess_ approximations
to the real. And he says this must be done in parallel, which just
makes things worse.
Firstly, I think arguments which are based too heavily on efficiency
are on a shaky ground. C is faster than Haskell, therefore everyone
should use C. Perhaps nobody has rally tried to implement efficient
Dedekind reals so how can we tell? In fact, as far as I know, nobody
has until last year. By the way, Cauchy sequences with a fixed rate of
convergence are a bad idea if you worry about efficiency. As Norbert
Mueller has demonstrated over the years, it is better to allow Cauchy
sequences (actually sequences of eventually shrinking intervals)
_without_ a priori conditions on the rate of convergence. Somewhat
paradoxically, by allowing arbitrarily slow rate of convergence we are
able to write _faster_ real arithmetic. This is a non-obvious fact
which the practitioners have been trying to get across, but it's not
sticking with the theorists for some reason. Thomas's argument about
AC_N being of only moderate help is true, but in a twisted way: in
practice AC_N is just never used explicitly, and moduli of continuity,
even fixed ones like 2^-n, are avoided at all cost.
Secondly, there are other criteria by which we should judge an
implementation. One of them is expressivity and the level of
abstraction. With the Dedekind reals certain concepts are more easily
expressed. For example, if one wants to talk constructively about
compactness of the closed interval, Cauchy reals will not be of much
help (unless you essentially declare [0,1] to be compact), whereas
locale-theoretic constructions in the style of Dedekind will work
better.
Lastly, since my computer believes in number choice, there really is
no dilemma. The Cauchy and Dedekind reals _must_ be equivalent to the
computer. Paul Taylor and I have devised algorithms for efficient,
sequential computation with Dedekind reals which use the equivalence
with Cauchy reals under the hood (at least I think that's what is
going on, but I do not fully understand the whole thing yet). There is
no need to think of a Dedekind real as a clumsy semidecision
procedure. Instead, the left and the right cut may be seen as
instructions for calculating better approximations from existing ones.
This can be done quite efficiently with Newton's method (the variant
for interval arithmetic). The computation that comes out then behaves
very much like an iterative procedure for computing a Cauchy sequence.
Best regards,
Andrej
From rrosebru@mta.ca Fri Feb 13 13:47:07 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 13 Feb 2009 13:47:07 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LY27G-0000nb-LW
for categories-list@mta.ca; Fri, 13 Feb 2009 13:46:18 -0400
Date: Thu, 12 Feb 2009 21:40:48 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: Re: "Kantor dust"
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LY27G-0000nb-LW@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 52
Toby Bartels wrote:
> Prof. Peter Johnstone wrote in part:
>
>> The trouble with the Conway construction is not that it's non-
>> constructive, but that it isn't (in any reasonable sense) a
>> construction of the reals. If you stop it at the point when it
>> finally constructs the real numbers 1/3, \sqrt{2}, \pi and so
>> on, then it has also succeeded in constructing lots of non-real
>> numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how
>> do you distinguish the numbers you want from the ones you don't?
>
> Can you get anywhere by imposing (at that stage) some Archimedean conditions?
> We need to know first how to interpret natural numbers as Conway numbers,
> then take the subset of those x such that -n < x < n for some n,
> and identify x and y if -1 < (x-y)n < 1 for every n.
Pretty much. Peter was speaking of day \omega. With your
identification applied to that day, the only other step needed is to
remove \omega and -\omega and then you have exactly the field R.
A more uniform way of arriving at R is to take the subset consisting of
those numbers expressible as a nonempty proper sup or nonempty proper
inf in an even number of ways. This is because at day \omega you have
\omega, -\omega, D \cdot 3 in the sense of ordinal product, where D is
the set of dyadic rationals and 3 = {-1/omega < 0 < 1/omega} (the range
of adjustments to each dyadic rational), and the dyadic irrationals.
\omega is a proper sup of the integers but not a nonempty inf (though it
is the empty inf), and dually for -\omega. The dyadic rationals are not
a proper sup or inf of anything (their increments on either side prevent
this) but the increment on the left is a proper sup but not a proper
inf, and dually on the right. The dyadic irrationals are both a proper
sup of what's below them and a proper inf of what's above them.
Puzzle. Bearing in mind that on all days prior to day \omega, every
number satisfies this criterion, on what other days besides day \omega
does this criterion produce a field?
Vaughan
From rrosebru@mta.ca Fri Feb 13 13:47:08 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 13 Feb 2009 13:47:08 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LY26c-0000jG-Fs
for categories-list@mta.ca; Fri, 13 Feb 2009 13:45:38 -0400
Date: Thu, 12 Feb 2009 20:39:03 -0800
From: Toby Bartels <toby+categories@ugcs.caltech.edu>
To: Categories list <categories@mta.ca>
Subject: categories: Re: Dedekind versus Cauchy reals
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Toby Bartels <toby+categories@ugcs.caltech.edu>
Message-Id: <E1LY26c-0000jG-Fs@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 53
Paul Taylor wrote in part:
>Toby Bartels said that the "UNDERLYING-SET AXIOM" in ASD is impredicativ=
e.
>This is correct, but I introduced this axiom as a "straw man".
>First, in order to say exactly what is needed to make ASD equivalent
>to (locally compact locales over) an elementary topos.
OK, that's pretty much what I thought.
>Second, to make the point that a great deal of mainstream mathematics
>is computable and does NOT require underlying sets. I see the main
>thread of ASD as being about a computable theory.
I hope you won't mind if I take this opportunity to ask something
that I've been idly wondering about ASD lately,
and which is related to this thread (even the Cantor set).
That is: 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 throug=
h.
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?
>[Toby] has said, for example
>* [...]
>* Similarly, if you remove identity types from intensional type theory
> (so breaking the justification of countable choice), you can still
> justify the fullness axiom and so construct the Dedekind reals
> (albeit not literally as sets of rational numbers).
>* [...]
>* But the Dedekind reals, as far as [he] can tell, do not; excluded
> middle, power sets, fullness, or countable choice would each do the
> job, but you need ~something~.
>I would challenge someone to consider the last of these questions
>seriously, maybe taking a hint from the second.
I'd be interested to hear if anybody has done ~any~ work on the second:
intensional type theory without identity types.
It seems to me to work if done in the style of Thierry Coquand
(with inductive types and dependent products as the main constructions)
but not if done in the style of Per Martin-L=C3=B6f
(with W-types and dependent and finitary products and sums).
I should probably say something about what categories
would serve as syntactic models of such a type theory,
but I never fully worked that out.
--Toby
From rrosebru@mta.ca Fri Feb 13 13:47:10 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 13 Feb 2009 13:47:10 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LY282-0000su-Lr
for categories-list@mta.ca; Fri, 13 Feb 2009 13:47:06 -0400
From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
Date: Fri, 13 Feb 2009 13:28:54 +0100
To: Andrej Bauer <andrej.bauer@andrej.com>, categories@mta.ca
Subject: categories: Re: Dedekind versus Cauchy reals
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
Message-Id: <E1LY282-0000su-Lr@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 54
Dear Andrej,
wasn't aware of the fact that insisting on fixed rate of convergence can make
things slower. My argument BTW was not about speed but rather about the ability
to read off the desired result. In case of Cauchy sequences I need the modulus
of convergence to know when I am close enough. In case of Dedekind reals that's
not needed PROVIDED the left and the right set are given by enumerations of
rationals. I "just" have to wait till close enough approximations from left
and right have been enumerated.
But is it right that in your implementation the left and right cuts are given
by ENUMERATIONS of its elements and now via semidecision procedures?
I guess so.
Well, but when considering Dedekind cuts this way it essentially boils down
to introducing reals as interval nestings (as done in High School sometimes).
So really the question is whether Cauchy sequences or interval nestings are
better. The way I interpret your remarks is that interval nesting is better
since it allows one to avoid moduli of continuity which is good since fixed
rate of convergence is a source of inefficiency.
I think even constructivists refuting impredicativity have no problem to
embrace representations by interval nestings. If I am not mistaken one finds
this also in Martin-Loef's 1970 book.
Thomas
From rrosebru@mta.ca Fri Feb 13 13:47:42 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 13 Feb 2009 13:47:42 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LY28Z-0000xX-FY
for categories-list@mta.ca; Fri, 13 Feb 2009 13:47:39 -0400
MIME-Version: 1.0
Date: Fri, 13 Feb 2009 14:47:57 +0100
Subject: categories: enriched Kan-extensions
From: Tony Meman <tonymeman1@googlemail.com>
To: categories <categories@mta.ca>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Tony Meman <tonymeman1@googlemail.com>
Message-Id: <E1LY28Z-0000xX-FY@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 55
Dear category theorists,
I have a question concerning enriched left Kan-extensions.
My situation is the following:
V is a complete and cocomplete symmetric monoidal closed category, A and B
two small V categories and F:A-->B a V-functor. Via the V-left-Kan extension
one gets a V-adjunction
Lan_F: V-Fun(A,V)<-->V-Fun(B,V):F*
where F* denotes the precomposition with F.
Moreover, the V-category V-Fun(A,V) and the V-category V-Fun(B,V) are
equipped with a symmetric V-monoidal structure respectively. Is it known,
under which conditions the adjunction (Lan_F,F*) is actually a monoidal
adjunction? Surely, it must have something to do with F: I suppose that F
have to be a symmetric monoidal functor with respect to a symmetric
V-monoidal structure on and A and B. The V-monoidal structures on A and B
also should have something to do with the V-monoidal structure on V-Fun(A,V)
and V-Fun(B,V).
Does anyone know a reference for this situation?
Thank you in advance for any help.
Tony
From rrosebru@mta.ca Fri Feb 13 13:48:21 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 13 Feb 2009 13:48:21 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LY29C-00012A-2C
for categories-list@mta.ca; Fri, 13 Feb 2009 13:48:18 -0400
Date: Fri, 13 Feb 2009 16:05:14 +0100
From: gcuri@math.unipd.it
To: categories@mta.ca
Subject: categories: Re: Dedekind versus Cauchy reals
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: gcuri@math.unipd.it
Message-Id: <E1LY29C-00012A-2C@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 56
Quoting Paul Taylor <pt09@PaulTaylor.EU>:
>
>
> Toby has also said a lot of interesting things about many different
> systems. These illustrate my point that it is essential to state
> which system, or which notion of "constructivity" you intend.
>
> He has said, for example
> * The Dedekind reals can also be constructed in CZF (Peter Aczel's
> predicative constructive set theory) even if you remove countable
> choice, using subset collection aka fullness.
> * Similarly, if you remove identity types from intensional type theory
> (so breaking the justification of countable choice), you can still
> justify the fullness axiom and so construct the Dedekind reals
> (albeit not literally as sets of rational numbers).
> * The Cauchy reals exist an a Pi-W-pretopos (equivalently, in a
> constructive set or type theory with exponentiation but no power
> sets or even fullness and with infinity but no countable choice).
> * But the Dedekind reals, as far as [he] can tell, do not; excluded
> middle, power sets, fullness, or countable choice would each do the
> job, but you need ~something~.
>
> I would challenge someone to consider the last of these questions
> seriously, maybe taking a hint from the second. ASD provides another,
> as it uses lambda term over a special object instead of talking about
> "sets" of rational numbers.
A note concerning the possibility of constructing the Dedekind reals with=
out
fullness, etc:
the Dedekind reals can be defined in constructive set theory even withou=
t
excluded middle, power sets, fullness, or countable choice. The point is =
that
they then form a class and not a set.
Class-sized objects are however the norm in a constructive predicative se=
tting.
For instance, a (non-trivial) locale is carried by a class that is never =
a set;
in general a formal space or formal topology is a large object too, so th=
at one
often deals with superlarge "categories" with large homsets.
Giovanni Curi
Dipartimento di Matematica Pura ed Applicata
Universita' degli Studi di Padova
www.math.unipd.it
From rrosebru@mta.ca Sun Feb 15 19:12:44 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 15 Feb 2009 19:12:44 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LYq8y-0003pF-Iy
for categories-list@mta.ca; Sun, 15 Feb 2009 19:11:24 -0400
From: "Ronnie Brown" <ronnie.profbrown@btinternet.com>
To: "Categories list" <categories@mta.ca>
Subject: categories: Re: Dedekind versus Cauchy reals
Date: Sun, 15 Feb 2009 07:43:31 -0000
MIME-Version: 1.0
Content-Type: text/plain;format=flowed;charset="iso-8859-1";reply-type=original
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Ronnie Brown" <ronnie.profbrown@btinternet.com>
Message-Id: <E1LYq8y-0003pF-Iy@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 57
I have enjoyed, without entirely following, the debate on this theme and
would like to ask some naive questions.
Rather practical toposes are presheaf toposes. Do the Dedekind and Cauchy
reals differ in some of those?
To be more practical again, one use of the reals is to analyse motion, as
Lawvere has said. Motion includes change of data, which is analysed by
statistics. But suppose the data to be analysed has structure, such as a
directed graph. Then perhaps we need the reals in the topos of directed
graphs? I.e. insert the required structure at the very beginning of the
study, instead of post facto. Is the law of large numbers valid in the (??)
probablity theory based on those reals? And which reals?
Idle curiosity I fear!
Ronnie
From rrosebru@mta.ca Sun Feb 15 19:12:44 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 15 Feb 2009 19:12:44 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LYq89-0003mW-QP
for categories-list@mta.ca; Sun, 15 Feb 2009 19:10:33 -0400
Date: Sat, 14 Feb 2009 22:50:12 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories list <categories@mta.ca>
Subject: categories: Re: Dedekind versus Cauchy reals
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LYq89-0003mW-QP@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 58
Andrej Bauer wrote:
> There is
> no need to think of a Dedekind real as a clumsy semidecision
> procedure. Instead, the left and the right cut may be seen as
> instructions for calculating better approximations from existing ones.
> This can be done quite efficiently with Newton's method (the variant
> for interval arithmetic). The computation that comes out then behaves
> very much like an iterative procedure for computing a Cauchy sequence.
If everything can be related to interval arithmetic in one way or
another, why not take interval arithmetic itself as the gold standard
for the constructive reals? The Edalat-Escardo-Potter domain-theoretic
analysis of interval arithmetic struck me as sufficiently canonical that
I don't understand why all the alternatives aren't being evaluated
relative to that one. Are there alternatives that compensate for some
shortcoming of interval arithmetic as understood through the lens of
domain theory?
Vaughan Pratt
From rrosebru@mta.ca Sun Feb 15 19:12:44 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 15 Feb 2009 19:12:44 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LYq9t-0003s4-2N
for categories-list@mta.ca; Sun, 15 Feb 2009 19:12:21 -0400
Date: Mon, 16 Feb 2009 09:31:43 +1100
Subject: categories: Re: enriched Kan-extensions
From: Steve Lack <s.lack@uws.edu.au>
To: Tony Meman <tonymeman1@googlemail.com>,categories <categories@mta.ca>
Mime-version: 1.0
Content-type: text/plain; charset="US-ASCII"
Content-transfer-encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Steve Lack <s.lack@uws.edu.au>
Message-Id: <E1LYq9t-0003s4-2N@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 59
Dear Tony,
As you say, this depends on how the monoidal structures on the functor
categories are defined. The only sensible way I know of which uses the given
structures on A and B is by Day convolution, and then your result will hold
if F itself is strong monoidal.
See the Day-Street paper "Kan extensions along promonoidal functors" in
volume 1 of TAC.
Regards,
Steve Lack.
On 14/02/09 12:47 AM, "Tony Meman" <tonymeman1@googlemail.com> wrote:
> Dear category theorists,
> I have a question concerning enriched left Kan-extensions.
>
> My situation is the following:
> V is a complete and cocomplete symmetric monoidal closed category, A and B
> two small V categories and F:A-->B a V-functor. Via the V-left-Kan extension
> one gets a V-adjunction
> Lan_F: V-Fun(A,V)<-->V-Fun(B,V):F*
> where F* denotes the precomposition with F.
>
> Moreover, the V-category V-Fun(A,V) and the V-category V-Fun(B,V) are
> equipped with a symmetric V-monoidal structure respectively. Is it known,
> under which conditions the adjunction (Lan_F,F*) is actually a monoidal
> adjunction? Surely, it must have something to do with F: I suppose that F
> have to be a symmetric monoidal functor with respect to a symmetric
> V-monoidal structure on and A and B. The V-monoidal structures on A and B
> also should have something to do with the V-monoidal structure on V-Fun(A,V)
> and V-Fun(B,V).
>
> Does anyone know a reference for this situation?
>
> Thank you in advance for any help.
> Tony
>
>
From rrosebru@mta.ca Wed Feb 18 03:23:17 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 18 Feb 2009 03:23:17 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LZgl4-0003BT-BE
for categories-list@mta.ca; Wed, 18 Feb 2009 03:22:14 -0400
Date: Mon, 16 Feb 2009 15:41:08 +0000
From: "Roy L. Crole" <rlc3@mcs.le.ac.uk>
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: 2nd Call for Participation - Midlands Graduate School in the Foundations of Computing Science 2009
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Roy L. Crole" <rlc3@mcs.le.ac.uk>
Message-Id: <E1LZgl4-0003BT-BE@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 60
Dear Colleagues,
We still have a small number of places remaining at MGS2009, available
at the full rate of =A3380. If you would like to attend, please complete =
the
registration form provided on the web page.
****************************************************************
Midlands Graduate School in the Foundations of Computing Science
****************************************************************
=20
30th March - 3rd April 2009
University of Leicester, UK
http://www.cs.le.ac.uk/events/mgs2009
The 10th Midlands Graduate School (MGS) is taking place!
WHAT IS MGS 2009?
The MGS is an intensive course of lectures on the Foundations
of Computing. It is very well established, with this being our 10th
anniversary, and has always proved a very popular and successful
event. This year we have Professor Peter Dybjer, Chalmers, Sweden, as
guest lecturer.
The lectures are aimed at graduate students, typically in their first
or second year of study for a PhD. However, the school is open to
anyone who is interested in learning more about mathematical computing
foundations. We very much welcome international applications as well
as from those from the UK.
COURSES
- Foundations
Thorsten Altenkirch Category Theory =20
Paul Levy The Lambda Calculus =20
Henrik Nilsson Functional Programming =20
- Advanced
Peter Dybjer Normalization by Evaluation =20
Martin Escardo Semantics =20
Nicola Gambino Dependent Types
Alexander Kurz Coalgebra
Uday Reddy Separation Logic
Georg Struth Automated Theorem Proving
WHERE IS MGS 2009?
MGS 2009 will take place at John Foster Hall, University of Leicester,
UK, with accommodation and lectures all on one site. Breakfasts,
lunches and four course dinners will be provided.
For further details and registration visit
http://www.cs.le.ac.uk/events/mgs2009
Roy Crole and Daniela Petrisan.
From rrosebru@mta.ca Wed Feb 18 03:23:17 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 18 Feb 2009 03:23:17 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LZgjJ-00039g-6R
for categories-list@mta.ca; Wed, 18 Feb 2009 03:20:25 -0400
MIME-Version: 1.0
Date: Mon, 16 Feb 2009 08:01:05 +0100
Subject: categories: Re: Dedekind versus Cauchy reals
From: Andrej Bauer <andrej.bauer@andrej.com>
To: Vaughan Pratt <pratt@cs.stanford.edu>, <categories@mta.ca>
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Andrej Bauer <andrej.bauer@andrej.com>
Message-Id: <E1LZgjJ-00039g-6R@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 61
On Sun, Feb 15, 2009 at 7:50 AM, Vaughan Pratt <pratt@cs.stanford.edu> wrote:
> If everything can be related to interval arithmetic in one way or
> another, why not take interval arithmetic itself as the gold standard
> for the constructive reals? The Edalat-Escardo-Potter domain-theoretic
> analysis of interval arithmetic struck me as sufficiently canonical that
> I don't understand why all the alternatives aren't being evaluated
> relative to that one. Are there alternatives that compensate for some
> shortcoming of interval arithmetic as understood through the lens of
> domain theory?
I essentially agree with you, namely that interval arithmetic
(actually, the interval domain) plays a fundamental role in the
construction of reals, as well as in practical computation (the
fastest implementations use interval arithmetic on top of
multiple-precision floating point).
A result of Vasco Brattka says that any two implementations of the
structure of reals (arithmetic, abs, semidecidable <, limit operator
for rapid sequences) are computably isomorphic. This can be
interpreted as saying that the domain-theoretic reals are as good as
any other version.
One reason why this is not the end of the story is that we do not
understand what happens at higher types. Vasco tells us that given two
versions of reals, R1 and R2, they are computably isomorphic. But how
about functions R1 -> R1, functionals (R1 -> R1) -> R1 and other
higher types?
For example, if R1 is the domain-theoretic reals (constructed as the
maximal elements of the interval domain) and R2 is the "Cauchy reals"
(represented as streams of digits, including negative digits), then we
know that the hierachies
R1, R1 -> R1, (R1 -> R1) -> R1, ...
and
R2, R2 -> R2, (R2 -> R2) -> R2, ...
agree in the first three terms, but do not know what happens after
that. This was established by Alex Simpson, Martin Escardo and myself.
Dag Normann has also investigated the two hierarchies.
For the familiar case of natural numbers John Longley has shown that
"in nature" there are only three versions of the hierachy
N, N -> N, (N -> N) -> N, ...
These are the hereditarily effective operators, the Kleene-Kreisel
continuous functionals, and a "mixed" version (the computable
Kleene-Kreisel continuous functionals). We would like to have a result
like that for reals, but we're stuck with the continuous version of
the hierarchy at rank 3.
In terms of implementation, the question is the following: does it
matter whether the reals are implemented transparently (the programmer
has access to their internal representation) or opaquely (reals are
values of an abstract data type whose internal workings cannot be
inspected)? We know that up to types of rank 2 it does not matter.
Until such questions are answered, settling with a single construction
or theory of real number computation is premature.
By the way, can you give a single interesting _total_ functional of
type ((R -> R) -> R) -> R? (Please don't ask me to define
"interesting".)
Andrej
From rrosebru@mta.ca Wed Feb 18 03:23:30 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 18 Feb 2009 03:23:30 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LZgmE-0003DQ-Rn
for categories-list@mta.ca; Wed, 18 Feb 2009 03:23:26 -0400
Mime-Version: 1.0 (Apple Message framework v624)
Content-Type: text/plain; charset=US-ASCII; format=flowed
Content-Transfer-Encoding: 7bit
From: Paul Taylor <pt09@PaulTaylor.EU>
Subject: categories: Dedekind versus Cauchy reals
Date: Mon, 16 Feb 2009 22:09:21 +0000
To: Categories list <categories@mta.ca>
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Paul Taylor <pt09@PaulTaylor.EU>
Message-Id: <E1LZgmE-0003DQ-Rn@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 62
Thomas Streicher said, in response to Andrej Bauer,
> In case of Cauchy sequences I need the modulus of convergence to know
> when I am close enough. In case of Dedekind reals that's not needed
> PROVIDED the left and the right set are given by enumerations of
> rationals.
You still need a condition with the same objective. It is given
by LOCATEDNESS:
for any d<u, either d is in the lower cut, or u is in the upper cut
This means that, if you so far know that the number is between d0 and
u0,
ie that d0 is in the lower cut and u0 in the upper one, and want another
three decimal (ten binary) places, you need to bisect [d0,u0] 11 times.
> I "just" have to wait till close enough approximations from left
> and right have been enumerated. But is it right that in your
> implementation the left and right cuts are given by ENUMERATIONS
> of its elements and now via semidecision procedures? I guess so.
> Well, but when considering Dedekind cuts this way it essentially
> boils down to introducing reals as interval nestings (as done in
> High School sometimes).
No -- you're trying to force Dedekind cuts (and real computation in
general) into the straitjacket of Cauchy sequences. This is part
of the longstanding prejudice in favour of numbers and against logic.
If you GENUINELY take Dedekind cuts on board, you can start thinking
of computation using GEOMETRY and other disciplines.
The fragment of the ASD calculus for R has a syntax with
- types N, R, Sigma and Sigma^R
- arithmetic operations + - *
- arithmetic relations < > !=
- the usual stuff on N too
- logical operations T F /\ \/
- existential quantifiers over N, R, open intervals, closed intervals
(with real endpoints), ie with types Sigma^N-->Sigma etc
- universal quantifiers over closed bounded intervals
- definition by description for N
- Dedekind cuts for R
- primitive recursion over N at all types.
The primitive calculation is therefore a LOGICAL question,
- existentially or universally quantified over some ranges
of the variables
- of an arithmetic comparison ( > OR < )
- of two polynomials.
This suggests using SEMI-ALGEBRAIC GEOMETRY, although I do not know
enough about this subject to see how to use it.
A quick way that answers a universally quantified question
surprisingly often is just to evaluate the polynomials using
interval (Moore) arithmetic.
Another technique is to split the range of one of the variables.
A much more powerful technique uses the INTERVAL Newton algorithm.
The "classical" Newton algorithm DOUBLES THE NUMBER OF BITS OF
PRECISION at each iteration -- once you have got below the "typical
length" of the problem. Above this, it behaves chaotically.
The interval Newton algorithm "knows" how to behave -- like
interval halving when the problem is essentially combinatorial,
and like the classical algorithm when we're below the typical length.
Whereas UNIVERSALLY quantified questions can often be answered
using "ordinary" (Moore) interval arithmetic, EXISTENTIAL ones
are handled in a similar way, but using "back-to-front" intervals,
whose arithmetic was originally formulaed by Edgar Kaucher.
Andrej's program uses forward and backward intervals to evaluate
Dedekind cuts, but does not at the moment use the interval Newton
algorithm,
Vaughan Pratt said, again in response to Andrej,
> If everything can be related to interval arithmetic in one way or
> another, why not take interval arithmetic itself as the gold standard
> for the constructive reals? The Edalat-Escardo-Potter domain-theoretic
> analysis of interval arithmetic struck me as sufficiently canonical
> that
> I don't understand why all the alternatives aren't being evaluated
> relative to that one. Are there alternatives that compensate for some
> shortcoming of interval arithmetic as understood through the lens of
> domain theory?
In previous ages, mathematicians of the day "standardised" on unit
fractions or Roman numerals. At one conference that I attended,
a whole afternoon was given over to a team of interval analysts who
wanted to "standardise" their subject, in the bureaucratic sense of
getting some document accepted by the ISO. One of the speakers did
some dreadful mathematics that depended heavily on decidable choices,
another presented some "software engineering" that was -- even for
that subject -- dogmatic and outdated, whilst the third gave a (good)
political speech.
If you read what most interval analysts write, it is ad hoc and
wrong-headed. There is, in particular, a fundamental error in
regarding the interval [d,u] as the closed set of numbers BETWEEN
d and u. Amongst other things, this makes it impossible to understand
Kaucher arithmetic (back-to-front intervals). Another widespread
belief is that interval arithmetic is some wonderful new algebraic
system in the tradition of the complex numbers and quaternions.
A much simpler way of understanding the interval [d,u], which is
both constructive and compatible with Kaucher arithmetic, is as
a DEDEKIND PSEUDO-CUT. The two halves consist of the numbers that
are SO FAR KNOWN to be respectively less and greater than the number
being calculated. This representation is much more natural, in
that advancing calculation and the Scott topology are in the same
sense as increasing the sets D and U, whereas the closed set [d,u]
becomes smaller. Essentially, the two parts D and U then lead
their own separate lives, each belonging to an "extended line"
with the Scott topology. It's actually very simple.
Paul Taylor
PS. I have flagged Toby Bartels' question,
> to what extent does ASD have inductive and coinductive objects,
to answer after the current thread about the reals, Cantor space,
the Conway numbers, constructivity and toposes has died down.
PPS. My website has now gone live on a new server at www.PaulTaylor.EU
whilst the old one is still at www.monad.me.uk. Please tell me
about missing links and server errors. The "monad" address will
become a redirection in a couple of weeks' time, and will be
discontinued next year.
From rrosebru@mta.ca Wed Feb 18 21:04:17 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 18 Feb 2009 21:04:17 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LZxHo-0006bC-Lp
for categories-list@mta.ca; Wed, 18 Feb 2009 21:01:08 -0400
Date: Wed, 18 Feb 2009 22:23:14 +0600 (NOVT)
From: "Serge P. Kovalyov" <kovalyov@nsc.ru>
To: categories@mta.ca
Subject: categories: Question on E-coreflective subcategories
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Serge P. Kovalyov" <kovalyov@nsc.ru>
Message-Id: <E1LZxHo-0006bC-Lp@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 63
Dear Category Theory gurus,
In my reserach I have encountered the following problem.
Let A be a full isomorphism-closed coreflective subcategory of a category
C, G : C -> A be a coreflection. Let (E, M) be a factorization system for
C-morphisms, such that class G(E) contains class of all A-isomorphisms and
is contained in class of all A-retractions.
Is any of the following statements correct:
1. If functor G preserves M, then it preserves E.
2. If any M-morphism is mono, then an M-morphism belongs to Mor(A)
provided that its codomain belongs to Ob(A).
Examples known to me satisfy both statements, but I fail to prove any.
Thanks,
Serge.
From rrosebru@mta.ca Wed Feb 18 21:04:17 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 18 Feb 2009 21:04:17 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LZxIj-0006eM-Le
for categories-list@mta.ca; Wed, 18 Feb 2009 21:02:05 -0400
From: Richard Moot <richard.moot@labri.fr>
To: Richard Moot <Richard.Moot@labri.fr>
Content-Type: text/plain; charset=US-ASCII; format=flowed
Content-Transfer-Encoding: 7bit
Subject: categories: ESSLLI 2009 Call for Participation
Date: Wed, 18 Feb 2009 18:26:26 +0100
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Richard Moot <richard.moot@labri.fr>
Message-Id: <E1LZxIj-0006eM-Le@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 64
======================================================================
= =
= CALL FOR PARTICIPATION =
= =
= 21st EUROPEAN SUMMER SCHOOL IN LOGIC, LANGUAGE AND INFORMATION =
= ESSLLI 2009 =
= =
= Bordeaux, July 20-31 2009 =
= =
======================================================================
http://esslli2009.labri.fr/
The European Summer School in Logic, Language and Information (ESSLLI)
is organized every year by the Association for Logic, Language and
Information (FoLLI) in different sites around Europe. The main focus
of ESSLLI is on the interface between linguistics, logic and
computation.
The 21st edition of ESSLLI will be held in Bordeaux, recently
selected as a Unesco World Heritage site.
* Course Program *
ESSLLI offers a total of 48 courses and workshops, divided among
foundational, introductory and advanced courses, and including a total
of 7 workshops. The courses and workshops cover a wide variety of
topics within the three areas of interest: Language and Computation,
Language and Logic, and Logic and Computation.
http://esslli2009.labri.fr/programme.php
* Registration *
Registration for ESSLLI is open. Early registration rates are 225 euros
for students and 350 euros for others.
Early registration deadline: 1st of May 2009.
http://esslli2009.labri.fr/reg.php
Richard Moot
ESSLLI Organizing Committee
From rrosebru@mta.ca Fri Feb 20 19:03:25 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 20 Feb 2009 19:03:25 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LaeM4-0004hy-TB
for categories-list@mta.ca; Fri, 20 Feb 2009 19:00:25 -0400
Date: Thu, 19 Feb 2009 23:57:18 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: Fixing the constructive continued-fraction definition of the reals: proofs and refutations
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1LaeM4-0004hy-TB@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 65
Prof. Peter Johnstone wrote:
> On Wed, 11 Feb 2009, Vaughan Pratt wrote:
>
>> Prof. Peter Johnstone wrote:
>>> Whoa! This simply can't work. Whatever the final coalgebra for N x (-)
>>> looks like, it must (thanks to Lambek) be isomorphic to N x itself,
>>> and therefore (since equality for N is decidable) must have lots of
>>> complemented subobjects {0} x itself, {1} x itself, ... The point of
>>> the continuity theorem for functions R --> R is that there are toposes
>>> in which R has *no* nontrivial complemented subobjects [...]
>>> The only way to get round it (apart from using glue)
>>> is to replace N by some "nonstandard natural number object" having no
>>> nontrivial complemented subobjects -- but where you get that from, I
>>> don't know.
>>
>> You're assuming product distributes over sums, which would be true for
>> ordinary product but I specified lexicographic product, with the left
>> argument as the "high order digit" (converse of the usual convention for
>> ordinal product in ordinal arithmetic).
>
> For goodness' sake, Vaughan! How many times do I have to tell you that
> I'm talking about *the underlying object* of the final coalgebra, and
> not its order structure or its topology? If the underlying object of
> the lexicographic product is the ordinary (cartesian) product -- and
> if it's not, then I don't know what it is -- then it distributes over
> sums because that's what products do in a topos.
Peter, if you don't mind my answering a question with a question, did
either of us mention underlying objects before? (I could have
overlooked an earlier message.)
When you speak out of the blue about "the underlying object of the final
coalgebra," what exactly is underlying what? I feel like I've abruptly
stepped through a mirror into some strange part of topos theory that
will be covered in Volume 3 of the Elephant.
One notion of underlying object that makes sense for me in the context
so far is the set E(1,X) of elements of an object X in a topos E. With
this notion I have a prayer of making sense of your claim in the context
of the following four objects of a topos E with NNO N (and whatever else
if anything is needed to ensure that objects 2-4 exist in E).
1. N^2.
2. The initial object among all objects X with an element 0: 1 --> X
and maps s,t: X --> X satisfying st = ts.
3. As for 2 with ts = t in place of st = ts.
4. As for 3 with st = s in place of ts = t.
If I've grasped this slippery topos concept, all four objects X of E
have, as their underlying set E(1,X), the set of all pairs (m,n) of
natural numbers (up to isomorphism of course). In 2 the elements take
the form of terms (s^m||t^n)(0) meaning m s's and n t's applied in any
order to 0. In 3 the elements take the form of maps s^m(t^n(0)) meaning
n applications of t (coarse tuning) followed by m applications of s
(fine tuning), while in 4 they take the form of maps t^m(s^n(0)) (3 with
s and t interchanged).
I could well imagine 1 and 2 turning out to be isomorphic, but I feel I
would get a lot from seeing the proof of whichever way that goes.
I presume that 3 and 4 are isomorphic on the ground that s and t can be
mapped to any two endomorphisms whence there must exist an isomorphism
exchanging s and t. I imagine I would get less out of a rigorous proof
of that unless there's a bug in the previous sentence. If there's no
bug then this would seem to constitute a subtle difference from algebra,
where the signature labels the operations in a way that prevents such an
interchange and puts 3 and 4 in distinct albeit equivalent varieties.
Whether or not 1 and 2 are isomorphic, they are in some sense both
representations of the ordinary product of N with itself.
Where I have greater difficulty is imagining an isomorphism between 2
and 3 merely on the ground that they have the same underlying object.
I'm really not following your logic here. 2 implements product
concurrently whereas 3 and 4 implement it sequentially. How could they
be isomorphic in every topos? (I can see that they'd have to be
isomorphic in Set, and presumably certain other toposes which however I
have no idea how to characterize.) I regard 3 and 4 as equivalent
definitions of the ordinal w^2 (w = \omega) in a topos.
What are the necessary subobjects of 3, and which of those are
necessarily complemented? I can think of the singletons {(m,n)}, the
set of successor elements (since s: X --> X is a monic), and the
*uniform* tails s^m: X --> X of the successor elements, but not the set
of limit ordinals in w^2 since t: X --> X is not a monic, and hence not
anything involving t. Are there other subobjects of 3, and can you
characterize them all in some neat way?
If as you seem to be implying, 1-4 are isomorphic, then I would have to
agree with your "for goodness' sake" (yes it was really stupid of me not
to see that) and resign myself to the absence (thus far) of any
alternative to apartness for representing the reals.
If however you agree with me that they can't be isomorphic (via
something more reliable than my proof by agitated gesticulation born of
summary dismissal) then we can move on with the rest of my envisaged
program to define the continuum [0,x) in a topos without appealing to
apartness. This too may or may not have bugs, whence the "proofs and
refutations" qualification in the new subject line. (If this were darts
there'd be a sequential scoreboard, concurrently with beer.)
Vaughan
From rrosebru@mta.ca Sun Feb 22 02:23:18 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 22 Feb 2009 02:23:18 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1Lb7hq-0005zo-Mq
for categories-list@mta.ca; Sun, 22 Feb 2009 02:20:50 -0400
Date: Sat, 21 Feb 2009 12:29:48 -0400 (AST)
Subject: categories: Re: Fixing the constructive continued-fraction definition of the reals: proofs and refutations
From: "Toby Kenney" <tkenney@mathstat.dal.ca>
To: "Vaughan Pratt" <pratt@cs.stanford.edu>, categories@mta.ca
MIME-Version: 1.0
Content-Type: text/plain;charset=iso-8859-1
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Toby Kenney" <tkenney@mathstat.dal.ca>
Message-Id: <E1Lb7hq-0005zo-Mq@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 66
Vaughan Pratt wrote in part:
...
>
> One notion of underlying object that makes sense for me in the context
> so far is the set E(1,X) of elements of an object X in a topos E. With
> this notion I have a prayer of making sense of your claim in the contex=
t
> of the following four objects of a topos E with NNO N (and whatever els=
e
> if anything is needed to ensure that objects 2-4 exist in E).
>
> 1. N^2.
>
> 2. The initial object among all objects X with an element 0: 1 --> X
> and maps s,t: X --> X satisfying st =3D ts.
>
> 3. As for 2 with ts =3D t in place of st =3D ts.
>
> 4. As for 3 with st =3D s in place of ts =3D t.
>
...
>
> I could well imagine 1 and 2 turning out to be isomorphic, but I feel I
> would get a lot from seeing the proof of whichever way that goes.
>
> I presume that 3 and 4 are isomorphic on the ground that s and t can be
> mapped to any two endomorphisms whence there must exist an isomorphism
> exchanging s and t. I imagine I would get less out of a rigorous proof
> of that unless there's a bug in the previous sentence. If there's no
> bug then this would seem to constitute a subtle difference from algebra=
,
> where the signature labels the operations in a way that prevents such a=
n
> interchange and puts 3 and 4 in distinct albeit equivalent varieties.
>
> Whether or not 1 and 2 are isomorphic, they are in some sense both
> representations of the ordinary product of N with itself.
>
> Where I have greater difficulty is imagining an isomorphism between 2
> and 3 merely on the ground that they have the same underlying object.
> I'm really not following your logic here. 2 implements product
> concurrently whereas 3 and 4 implement it sequentially. How could they
> be isomorphic in every topos? (I can see that they'd have to be
> isomorphic in Set, and presumably certain other toposes which however I
> have no idea how to characterize.) I regard 3 and 4 as equivalent
> definitions of the ordinal w^2 (w =3D \omega) in a topos.
>
I=B4m pretty sure the objects (1)-(4) are isomorphic. Here=B4s a sketch o=
f the
proof:
Let X be the object (3), i.e. the initial object with a morphism 0:1---->=
X
and morphisms s:X---->X, t:X---->X with st=3Ds. Let Y be the object (2),
i.e. the initial object with a morphism 0:1---->Y and morphisms u:Y---->Y=
,
v:Y---->Y.
(1)&(2):
We clearly have maps 0 x 0: 1----> N^2, succ x 1_N and 1_N x succ :
N^2---->N^2, inducing the map Y---->N^2. For an element a of Y, we can
form maps f_{t,a}: N---->Y by 0 ]----> a, succ ]----> t, and f_{s,a} by
0 ]---->a, succ ]----> s. We can now form a map N x N ----> Y by
f(a,b)=3Df_{t,{f_{s,0}(a)}}(b). We can check that these maps form an
isomorphism.
(2)&(3):
Lemma: X is a monoid
We construct the addition X x X---->X by its exponential transpose
X---->X^X. This is the map induced by 1_X:1---->X^X, s^X:X^X---->X^X, and
t^X:X^X---->X^X.
We think of this monoid structure as ordinary ordinal addition.
We now construct morphisms s=B4 and t=B4 X---->X, given by s=B4(x)=3Dx + =
1 and
t=B4(x)=3D\omega + x. It is clear that s=B4 and t=B4 commute. This induce=
s a
morphism Y---->X.
On Y, we can create the projection map p:Y---->N as Y is isomorphic to N =
x
N. We also have the inclusion i : N ----> N x N given by a ]----> (a,0).
Now ipu and v satisfy ipuv=3Dipu (ipu is the map \_ + \omega. This induce=
s a
map X ----> Y, which will be the inverse of the map Y ----> X.
I will check the details later to make sure. But I would be very surprise=
d
if there were any problems.
Toby
From rrosebru@mta.ca Sun Feb 22 02:23:18 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 22 Feb 2009 02:23:18 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1Lb7jP-00062P-Nn
for categories-list@mta.ca; Sun, 22 Feb 2009 02:22:27 -0400
Date: Sat, 21 Feb 2009 09:18:29 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: Re: Fixing the constructive continued-fraction definition of the reals: proofs and refutations
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1Lb7jP-00062P-Nn@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 67
Toby Kenney wrote:
> Vaughan Pratt wrote in part:
>> I could well imagine 1 and 2 turning out to be isomorphic, but I feel I
>> would get a lot from seeing the proof of whichever way that goes.
Thanks very much, Toby. I didn't (and still don't) have any intuition
into what objects and morphisms are present in the free topos with NNO,
but your proof will help me fill in the gaps in this neighborhood of it.
On the one hand there are lots of objects one can talk about in language
analogous to that characterizing the NNO, on the other there are also
lots of morphisms one can talk about that identify those objects (up to
isomorphism), and I'm still at the very early stage of learning how to
walk along that ridge line without falling off one side or the other.
Joyal and Moerdijk, Algebraic Set Theory, show how to construct
sup-semilattices with sups up to a specified size S. Obviously not
every topos with NNO supports every S, but presumably S = K
(Kuratowski-finite) is always present. Your proof if correct shows that
ts = t is too strong. What if I relax it to ts <= t and proceed as in
J&M to construct the initial such object? Can you still construct your
isomorphism, or do we end up with a weaker relationship? If the latter
then we should have t(0) >= t(s(0)) = t(1) >= t(2) >= ... >= x for any
natural number x. Obviously t(0) is minimal among all terms having at
least one t, which should make t(0) the ordinal w.
The one disconcerting thing here is that initiality has made t(0) an
infinite sup even though I assumed only finite sups. I don't know
whether this means that the methods of J&M can't construct this initial
algebra, or that in every topos with NNO one can construct the requisite
sup-semilattices with countable sups. I suppose it must be the latter.
(I'm a complete novice here, as I've said before, so I hope people will
be patient with my appalling ignorance of topos-theoretic techniques.)
Vaughan
From rrosebru@mta.ca Sun Feb 22 02:23:31 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 22 Feb 2009 02:23:31 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1Lb7kN-00063L-0f
for categories-list@mta.ca; Sun, 22 Feb 2009 02:23:27 -0400
From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
Date: Sat, 21 Feb 2009 19:17:59 +0100
To: Paul Taylor <pt09@PaulTaylor.EU>, <categories@mta.ca>
Subject: categories: Re Dedekind versus Cauchy reals
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
Message-Id: <E1Lb7kN-00063L-0f@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 68
Dear Paul and Andrej,
I was aware of the fact that locatedness is part of definition of Dedekind
cut it guarantees. It guarantees that there are close enough approximations
for any required degree of precision.
Having had a look at Andrej's slides I can't say that they provided me with
an understanding of the operational semantics of the language.
The impression I got is that he is using (kind of) interval arithmetic for
determining truth values of terms of type \Sigma. That's ok but doesn't
answer the question what is a computationally given real number.
Do I understand your approach correctly as follows: when given a Dedekind
cut as a mapping c : Q -> 2_\bot and an accuracy eps then
\exists p,q : Q c(p) = 0 /\ c(q) = 1 /\ q-p < eps
is true and computing this truth value gives the witnesses p and q.
I.e. one evaluates terms of type \Sigma of the ASD language in a way
reminiscent of logic programming.
Thomas
From rrosebru@mta.ca Mon Feb 23 01:33:32 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 23 Feb 2009 01:33:32 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LbTQY-00028p-EA
for categories-list@mta.ca; Mon, 23 Feb 2009 01:32:26 -0400
Mime-Version: 1.0 (Apple Message framework v624)
Content-Type: text/plain; charset=US-ASCII; format=flowed
Content-Transfer-Encoding: 7bit
From: Paul Taylor <pt09@PaulTaylor.EU>
Subject: categories: Dedekind versus Cauchy reals
Date: Sun, 22 Feb 2009 14:09:29 +0000
To: Categories list <categories@mta.ca>
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Paul Taylor <pt09@PaulTaylor.EU>
Message-Id: <E1LbTQY-00028p-EA@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 69
Thomas Streicher asked about the "operational semantics" of the ASD
calculus, and in particular computation with Dedekind cuts. As he
says, the public documentation is rather limited at the moment, but
Andrej and I don't want to give all our ideas away before we have
made good use of them ourselves.
The first thing that one should say about "operational semantics"
is that mathematical formulae do NOT come with a prescibed way of
computing them. A large part of what makes mathematics interesting
is that there may be many ways of looking at a problem, besides the
"obvious" one. The two situations in which notation does come with a
preferred way of computing with it are long multiplication and lambda
calculus, but even these cases are open to INGENUITY in finding better
algorithms.
> I was aware of the fact that locatedness is part of definition of
> Dedekind cut it guarantees. It guarantees that there are close enough
> approximations for any required degree of precision.
Yes. In fact, there are two notions of locatedness, and this is the
stronger one, which is necessary for arithemetic. There are some
comments linking these ideas to the Archimedean axiom and the Conway
numbers in Sections 11 and 12 of "The Dedekind reals in ASD".
> when given a Dedekind cut as a mapping c : Q -> 2_\bot and an
> accuracy eps then
>
> \exists p,q : Q c(p) = 0 /\ c(q) = 1 /\ q-p < eps
>
> is true and computing this truth value gives the witnesses p and q.
Yes, that's right, except that "a mapping c : Q -> 2_\bot" is not
a very helpful way of formulating it. When computing a real number,
what we have (going back very clearly to Archimedes) is a pair of
logical formulae, each with a single free variable (p and q in your
notation, d and u in ours). One of which says when p is less than
the real number being computed, and the other when q is greater.
In order to fix the precision, we add another constraint that
squeezes them close together.
Then, as Thomas rightly says,
> one evaluates terms of type \Sigma of the ASD language in a way
> reminiscent of logic programming.
He claimed that this
> doesn't answer the question what is a computationally given real
> number.
Yes, it does, exactly. Notice that the "real number" is only on
the "outside" of the computation, and is only manifested when we want
to print it out --- hence my earlier pun that it is "peripheral".
The "guts" of the computation are with LOGICAL formulae.
> The impression I got is that he is using (kind of) interval
> arithmetic for determining truth values
Yes, but interval arithmetic is only one of a variety of tools.
Also, if you only think of intervals as a way of computing real numbers
to a given precision, you miss their real power. Plainly, these
intervals just get wider and wider.
Really, one should think of interval analysis as USING CRUDE ARITHMETIC
TO DERIVE STRONG LOGICAL INFORMATION ABOUT FUNCTIONS.
For example, if, when a function f is applied to an interval [d,u]
using Moore arithmetics, the result f[d,u] lies within an interval
(e,t), which we may determine purely ARITHMETICALLY, then we know
the LOGICAL statement that All x:[d,u]. e < f(x) < t.
Since f is given, not just as a funtion in the set-theoretic sense
of a collection of input--output pairs, but as a FORMULA in a certain
language, we may differentiate it formally, and apply interval
arithmetic to that, obtaining even stronger LOGICAL information about
the behaviour of the function.
Examining the language, the real work consists of manipulating
inequalities between polynomials over certain ranges of the variables.
Often we just want to know whether the inequality ALWAYS, SOMETIMES
or NEVER holds. A simple way to answer this question may just be
Moore-wise evaluation,
Then there is the sitation where the inequality is f(x,y) > 0 in
a certain rectangle. The polynomial defines a curve (=0) and two
regions (<0 and >0). As we increase the precision, the curve
becomes closer to being a straight line, and the main numerical
computation is of the gradient of this line, and of a narrow
rectangle that encloses the curve.
Just as the well known Moore arithmetic provides a way of evaluating
universally quantified statments, so Kaucher arithmetic with back-
to-front intervals answers existential statements.
I don't want to go into more detail that this, because we want to
get the credit for making this work (although we are keen to invove
more collaborators). But also, these are just SOME of the things
that might be done, AFTER ESCAPING FROM THE MENTAL STRAITJACKET of
computation with Cauchy sequences or intervals.
Paul Taylor
From rrosebru@mta.ca Mon Feb 23 01:33:34 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 23 Feb 2009 01:33:34 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LbTRb-0002A3-9n
for categories-list@mta.ca; Mon, 23 Feb 2009 01:33:31 -0400
Date: Sun, 22 Feb 2009 18:19:19 -0400 (AST)
Subject: Re: categories: Fixing the constructive continued-fraction definition of the reals: proofs and refutations
From: "Toby Kenney" <tkenney@mathstat.dal.ca>
To: "Vaughan Pratt" <pratt@cs.stanford.edu>, categories@mta.ca
MIME-Version: 1.0
Content-Type: text/plain;charset=iso-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Toby Kenney" <tkenney@mathstat.dal.ca>
Message-Id: <E1LbTRb-0002A3-9n@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 70
The proof I gave is not quite ideal - I showed that if the objects 1-4 yo=
u
list all exist, then they are isomorphic. In theory, it would still be
possible for object 3, say, not to exist. I think the following is a
better proof:
Let X be an object with morphisms 0 : 1 ----> X, s,t : X ----> X such tha=
t
ts=3Dt. We want to construct the map N^2 ----> X. We have a map
f : N ----> X, given by considering X with just 0 and t. For every n in N=
,
we can also form a map g_n : N ----> X by g_n(0)=3Dt^n(0), and g_n(succ)=3D=
s.
Now we can form the map h : N^2 ----> X by h(a,b)=3Dg_a(b). I think this
must be the unique map preserving everything necessary.
Your suggestion of relaxing the condition to ts <=3D t seems to require
changing from ordinary objects to partially-ordered objects. I think the
initial one should be just the free monoid on two generators, with some
partial order. You probably want to insist that s and t be inflationary.
If you=B4re considering partially-ordered objects, then this won=B4t be
isomorphic to N^2. I=B4m not sure whether there will be any isomorphism i=
n
the topos, even without requiring it to preserve order. You could
alternatively consider a condition like t=3Dsts. I=B4m not really sure wh=
at
you mean by your claim that t is the ordinal w - I think the object you
describe isn=B4t even totally ordered - how can you compare t^2(s(0)) and
t^2(0)? If you take a condition like t=3Dsts to make it totally ordered, =
you
still have a decreasing chain t > ts > ts^2 > ...
It looks like this should be something like the interval in N x Z,
lexicographically ordered, going from (0,0) (so without the pairs (0,-n))=
.
If this is still an attempt to construct the reals, then I don=B4t see an=
y
sensible way to describe addition on an infinite lexicographic product of
copies of Z (the integers).
On the matter of it being disconcerting finding infinite sups, the
definition doesn=B4t mention any form of partial order, so it shouldn=B4t
really be any more surprising than finding (Kuratowski) finite sups.
Sorry this email is mostly just intuition, rather than firm fact.
Hopefully some wiser people than I will be able to put more substance to
it.
Toby
> Toby Kenney wrote:
>> Vaughan Pratt wrote in part:
>>> I could well imagine 1 and 2 turning out to be isomorphic, but I feel=
I
>>> would get a lot from seeing the proof of whichever way that goes.
>
> Thanks very much, Toby. I didn't (and still don't) have any intuition
> into what objects and morphisms are present in the free topos with NNO,
> but your proof will help me fill in the gaps in this neighborhood of it=
.
>
> On the one hand there are lots of objects one can talk about in languag=
e
> analogous to that characterizing the NNO, on the other there are also
> lots of morphisms one can talk about that identify those objects (up to
> isomorphism), and I'm still at the very early stage of learning how to
> walk along that ridge line without falling off one side or the other.
>
> Joyal and Moerdijk, Algebraic Set Theory, show how to construct
> sup-semilattices with sups up to a specified size S. Obviously not
> every topos with NNO supports every S, but presumably S =3D K
> (Kuratowski-finite) is always present. Your proof if correct shows tha=
t
> ts =3D t is too strong. What if I relax it to ts <=3D t and proceed as=
in
> J&M to construct the initial such object? Can you still construct your
> isomorphism, or do we end up with a weaker relationship? If the latter
> then we should have t(0) >=3D t(s(0)) =3D t(1) >=3D t(2) >=3D ... >=3D =
x for any
> natural number x. Obviously t(0) is minimal among all terms having at
> least one t, which should make t(0) the ordinal w.
>
> The one disconcerting thing here is that initiality has made t(0) an
> infinite sup even though I assumed only finite sups. I don't know
> whether this means that the methods of J&M can't construct this initial
> algebra, or that in every topos with NNO one can construct the requisit=
e
> sup-semilattices with countable sups. I suppose it must be the latter.
>
> (I'm a complete novice here, as I've said before, so I hope people will
> be patient with my appalling ignorance of topos-theoretic techniques.)
>
> Vaughan
>
>
From rrosebru@mta.ca Mon Feb 23 01:34:20 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 23 Feb 2009 01:34:20 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LbTSK-0002Ba-LQ
for categories-list@mta.ca; Mon, 23 Feb 2009 01:34:16 -0400
Date: Sun, 22 Feb 2009 21:01:51 -0500
From: Jacques Carette <carette@mcmaster.ca>
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: Categorical development of algebra?
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Jacques Carette <carette@mcmaster.ca>
Message-Id: <E1LbTSK-0002Ba-LQ@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 71
Has anyone ever redone the classical development of algebra (magma,
monoid, semigroup, quasigroup, group, ring, modules, etc) as appropriate
diagrams in the Kleisli category of signatures and translations?
Jacques
From rrosebru@mta.ca Mon Feb 23 01:35:48 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 23 Feb 2009 01:35:48 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LbTTk-0002E8-Cx
for categories-list@mta.ca; Mon, 23 Feb 2009 01:35:44 -0400
From: MFPS <mfps@math.tulane.edu>
To: mfpsmail@tulane.edu, categories@mta.ca
Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
Mime-Version: 1.0 (Apple Message framework v930.3)
Subject: categories: MFPS Call for Participation
Date: Sun, 22 Feb 2009 07:58:49 -0600
Sender: categories@mta.ca
Precedence: bulk
Reply-To: MFPS <mfps@math.tulane.edu>
Message-Id: <E1LbTTk-0002E8-Cx@mailserv.mta.ca>
Status: RO
X-Status:
X-Keywords:
X-UID: 72
Dear Colleagues,
Registration is now open for MFPS 25, which will take place at
Oxford from April 3 through April 7. A list of accepted papers and an
outline program are also available. Participants will be housed either
in University College or in Linton Lodge, a hotel located not far from
the Computer Laboratory where the meetings will take place. We offer
reduced registration fees for students and for faculty who attend only
the last two days of the program.
To register for the meeting, please point your browser at http://www.math.tulane.edu/~mfps/mfps25
Accommodations are being held only until March 24, so please
register before then to reserve a room.
Thanks, and best regards,
Mike Mislove
Mathematical Foundations of
Programming Semantics
http://www.math.tulane.edu/~mfps
From rrosebru@mta.ca Mon Feb 23 19:22:11 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 23 Feb 2009 19:22:11 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1Lbk73-0002Cj-9s
for categories-list@mta.ca; Mon, 23 Feb 2009 19:21:25 -0400
From: Michael Fourman <michael.fourman@gmail.com>
To: Paul Taylor <pt09@PaulTaylor.EU>, <categories@mta.ca>
Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
Mime-Version: 1.0 (Apple Message framework v930.3)
Subject: categories: Re: Dedekind versus Cauchy reals
Date: Mon, 23 Feb 2009 09:03:51 +0000
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Michael Fourman <michael.fourman@gmail.com>
Message-Id: <E1Lbk73-0002Cj-9s@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 73
On 22 Feb 2009, at 14:09, Paul Taylor wrote:
> don't want to give all our ideas away before we have
> made good use of them ourselves
Others who adopted this approach, long ago, have since become
frustrated that they get no credit for ideas that (yet) others have
independently (re)invented.
Publish or perish!
Professor Michael Fourman FBCS CITP
Head of School
Informatics Forum
10 Crichton Street
Edinburgh
EH8 9AB
http://homepages.inf.ed.ac.uk/mfourman/
For diary appointments contact :
ajudd(at)ed-dot-ac-dot-uk
+44 131 650 2690
From rrosebru@mta.ca Mon Feb 23 19:22:11 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 23 Feb 2009 19:22:11 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1Lbk5N-00027N-5Y
for categories-list@mta.ca; Mon, 23 Feb 2009 19:19:41 -0400
Date: Mon, 23 Feb 2009 00:16:37 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: Re: Fixing the constructive continued-fraction definition of the reals: proofs and refutations
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: quoted-printable
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Vaughan Pratt <pratt@cs.stanford.edu>
Message-Id: <E1Lbk5N-00027N-5Y@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 74
Toby Kenney wrote:
> I think the following is a better proof:
Toby, thanks for that. Peter J. suggested a proof in a separate email
to me, let me absorb and compare them.
> Your suggestion of relaxing the condition to ts <=3D t seems to require
> changing from ordinary objects to partially-ordered objects. I think th=
e
> initial one should be just the free monoid on two generators, with some
> partial order. You probably want to insist that s and t be inflationary=
.
Quite right, I forgot to specify that s and t were monotone (which
implies inflationary), and I also left out that 0 is the empty sup.=20
(According to J&M in "Algebraic Set Theory" 1995, specifying=20
inflationary rather than monotone for the class as a whole gives the=20
hereditarily transitive sets, i.e. the von Neumann ordinals. Monotone=20
gives a larger class and a weaker notion of ordinal which nonetheless is=20
inflationary as a consequence of monotonicity and initiality.)
> If you=B4re considering partially-ordered objects, then this won=B4t be
> isomorphic to N^2. I=B4m not sure whether there will be any isomorphism=
in
> the topos, even without requiring it to preserve order. You could
> alternatively consider a condition like t=3Dsts. I=B4m not really sure =
what
> you mean by your claim that t is the ordinal w - I think the object you
> describe isn=B4t even totally ordered - how can you compare t^2(s(0)) a=
nd
> t^2(0)? If you take a condition like t=3Dsts to make it totally ordered=
, you
> still have a decreasing chain t > ts > ts^2 > ...
The conditions I forgot to mention, 0 <=3D x and t monotone, should give=20
t^2(0) <=3D t^2(s(0)).
> It looks like this should be something like the interval in N x Z,
> lexicographically ordered, going from (0,0) (so without the pairs (0,-n=
)).
> If this is still an attempt to construct the reals, then I don=B4t see =
any
> sensible way to describe addition on an infinite lexicographic product =
of
> copies of Z (the integers).
If both coordinates still have complemented subobjects, in particular if=20
{0} x w and w x {0} are both complemented subobjects, then I should=20
throw in the towel, consistent with Peter's advice. Are they? If w x=20
{0} is not a complemented subobject then we're moving in the right=20
direction: the next step is to define a suitable final coalgebra.
Vaughan
From rrosebru@mta.ca Thu Feb 26 02:51:21 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 26 Feb 2009 02:51:21 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1Lca2p-0003G3-DV
for categories-list@mta.ca; Thu, 26 Feb 2009 02:48:31 -0400
Date: Wed, 25 Feb 2009 20:08:48 -0500 (EST)
From: Michael Barr <barr@math.mcgill.ca>
To: Categories list <categories@mta.ca>
Subject: categories: ticked arrowheads in xy-pic and diagxy
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Michael Barr <barr@math.mcgill.ca>
Message-Id: <E1Lca2p-0003G3-DV@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 75
A month or two ago, Micah McCurdy wrote to ask me if it was possible to
make an arrow with a tick in the middle (that is ----+---->) and I said I
didn't know how to do that and suggested he ask Ross Moore. Ross told him
that xy-pic didn't have that capacity. Well, Micah discovered that it
did. Here are some samples, using diagxy, but that is just a front end to
xy-pic.
$$\bfig
\node a(0,0)[A]
\node b(300,400)[B]
\arrow/@{>}|-*@{>}/[a`b;f]
\efig$$
$$\bfig
\ptriangle/>`>`@{>}|-@{|}/[A`B`C;f`g`h]
\efig$$
$$\bfig
\morphism/@{>}|-@{+}/<700,0>[ABCDE`F;h]
\efig$$
$$\bfig
\morphism/@{>}|-*@{|}/<700,0>[ABCDE`F;h]
\efig$$
As far as I can tell, the * between the - and the @ has no effect. The
one limitation is that what goes inside the -@{ } must be a \dir. This is
a limitation for me, since I cannot figure out the syntax of \newdir. For
this to work, it clearly has to be something that tex can rotate.
Michael
From rrosebru@mta.ca Thu Feb 26 02:51:21 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 26 Feb 2009 02:51:21 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1Lca1S-0003E1-Kg
for categories-list@mta.ca; Thu, 26 Feb 2009 02:47:06 -0400
Date: Wed, 25 Feb 2009 20:52:02 +0600 (NOVT)
From: "Serge P. Kovalyov" <kovalyov@nsc.ru>
To: categories@mta.ca
Subject: categories: Re: Question on E-coreflective subcategories
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: "Serge P. Kovalyov" <kovalyov@nsc.ru>
Message-Id: <E1Lca1S-0003E1-Kg@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 76
Dear Colleagues,
> Let A be a full isomorphism-closed coreflective subcategory of a
> category C, G : C -> A be a coreflection. Let (E, M) be a factorization
> system for C-morphisms, such that class G(E) contains class of all
> A-isomorphisms and is contained in class of all A-retractions.
> Is any of the following statements correct:
> 1. If functor G preserves M, then it preserves E.
> 2. If any M-morphism is mono, then an M-morphism belongs to Mor(A)
> provided that its codomain belongs to Ob(A).
John Kennison provided me with excellent counter-example to both
statements. They are found in settings where M is "large" enough.
Specifically, (1) is refuted as follows:
Let C = Sets x {0,1} where {0,1} is the ordered category with 0 < 1.
Then E = All isos of C plus all maps (f,1):(S,1) to (T,1) with f onto.
And M = All maps (f,1):(S,1) to (T,1) with f one-to-one plus all maps from
(S,0)
And A = Sets x {0}
(2) is refuted by taking an order with cardinality > 2, a minimum
element, and a maximum element, for C, {min C, max C} for A, and (Iso,
Mor) for factorization system on C. John suggested the simplest example,
3-chain 0 < 1 < 2.
Thanks,
Serge.
From rrosebru@mta.ca Thu Feb 26 02:51:21 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 26 Feb 2009 02:51:21 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1Lca2A-0003F7-5c
for categories-list@mta.ca; Thu, 26 Feb 2009 02:47:50 -0400
Date: Wed, 25 Feb 2009 21:30:10 +0100
From: Carlos Areces <areces@pluton.loria.fr>
Subject: categories: E. W. Beth Dissertation Prize: 2009 call for submissions
Content-type: text/plain
To: undisclosed-recipients:;
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Carlos Areces <areces@pluton.loria.fr>
Message-Id: <E1Lca2A-0003F7-5c@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 77
E. W. Beth Dissertation Prize: 2009 call for submissions
Since 2002, FoLLI (the European Association for Logic,
Language, and Information, www.folli.org) awards the
E. W. Beth Dissertation Prize to outstanding dissertations
in the fields of Logic, Language, and Information. We invite
submissions for the best dissertation which resulted in a
Ph.D. degree in the year 2008. The dissertations will be
judged on technical depth and strength, originality, and
impact made in at least two of the three fields of Logic,
Language, and Computation. Inter-disciplinarity is an
important feature of the theses competing for the E. W.
Beth Dissertation Prize.
Who qualifies.
~~~~~~~~~~~~~~
Nominations of candidates are admitted who were awarded a
Ph.D. degree in the areas of Logic, Language, or Information
between January 1st, 2008 and December 31st, 2008. There is
no restriction on the nationality of the candidate or the
university where the Ph.D. was granted. After a careful
consideration, FoLLI has decided to accept only dissertations
written in English. Dissertations produced in 2008 but not
written in English or not translated will be allowed for
submission, after translation, also with the call next year
(for 2009). Respectively, nominations of full English
translations of theses originally written in other language
than English and defended in 2007 and 2008 will be accepted
for consideration this year, too.
Prize.
~~~~~~
The prize consists of:
* a certificate
* a donation of 2500 euros provided by the E. W. Beth Foundation.
* an invitation to submit the thesis (or a revised version
of it) to the new series of books in Logic, Language and
Information to be published by Springer-Verlag as part of LNCS
or LNCS/LNAI. (Further information on this series is available
on the FoLLI site)
How to submit.
~~~~~~~~~~~~~~
Only electronic submissions are accepted. The following documents
are required:
1. the thesis in pdf or ps format (doc/rtf not accepted);
2. a ten page abstract of the dissertation in ascii or pdf format;
3. a letter of nomination from the thesis supervisor.
Self-nominations are not admitted: each nomination must be
sponsored by the thesis supervisor. The letter of nomination
should concisely describe the scope and significance of the
dissertation and state when the degree was officially awarded;
4. two additional letters of support, including at least one letter
from a referee not affiliated with the academic institution that
awarded the Ph.D. degree.
All documents must be submitted electronically to
bethaward2008@gmail.com.
Hard copy submissions are not admitted.
In case of any problems with the email submission or a lack of
notification within three working days after submission, nominators
should write to goranko@maths.wits.ac.za or policriti@dimi.uniud.it,
with a cc to bethaward2008@gmail.com.
Important dates:
Deadline for Submissions: March 16, 2009.
Notification of Decision: July 1, 2009.
Committee :
* Anne Abeill=C3=A9 (Universit=C3=A9 Paris 7)
* Natasha Alechina (University of Nottingham)
* Wojciech Buszkowski (Adam Mickiewicz University, Poznan)
* Didier Caucal (IGM-CNRS)
* Nissim Francez (The Technion, Haifa)
* Valentin Goranko (chair) (University of the Witwatersrand, Johannesburg=
)
* Alexander Koller (Saarland University)
* Alessandro Lenci (University of Pisa)
* Gerald Penn (University of Toronto)
* Alberto Policriti (Universit=C3=A0 di Udine)
* Rob van der Sandt (University of Nijmegen)
* Colin Stirling (University of Edinburgh)
From rrosebru@mta.ca Sun Mar 1 18:13:18 2009 -0400
Return-path: <categories@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 01 Mar 2009 18:13:18 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from <categories@mta.ca>)
id 1LdtrI-0005tR-Of
for categories-list@mta.ca; Sun, 01 Mar 2009 18:10:04 -0400
Date: Sat, 28 Feb 2009 11:55:34 -0500 (EST)
From: Michael Barr <barr@math.mcgill.ca>
To: Categories list <categories@mta.ca>
Subject: categories: More arrow decorations
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: categories@mta.ca
Precedence: bulk
Reply-To: Michael Barr <barr@math.mcgill.ca>
Message-Id: <E1LdtrI-0005tR-Of@mailserv.mta.ca>
Status: O
X-Status:
X-Keywords:
X-UID: 78
By playing with Micah's discovery (which is actually documented on page
39, third line from the bottom of Fig. 13), I have come up with the
following potentially useful decorations:
$$\bfig \morphism/@{>}|-@{|}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{x}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{o}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{*}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{||}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{)}/<500,500>[A`B;f] \efig$$
$$\bfig \morphism/@{>}|-@{(}/<500,500>[A`B;f] \efig$$
The same ideas also work in native xy-pic and, for all I know, in the
matrix version as well.
Michael