Re: "Kantor dust"

[Greg Meredith <lgreg.meredith@biosimilarity.com>]

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
>