From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/76 Path: news.gmane.org!not-for-mail From: Greg Meredith Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Wed, 11 Feb 2009 11:56:40 -0800 Message-ID: Reply-To: Greg Meredith NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1234405637 11083 80.91.229.12 (12 Feb 2009 02:27:17 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 12 Feb 2009 02:27:17 +0000 (UTC) To: "Prof. Peter Johnstone" , categories@mta.ca Original-X-From: categories@mta.ca Thu Feb 12 03:28:28 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1LXRJT-0000bs-42 for gsmc-categories@m.gmane.org; Thu, 12 Feb 2009 03:28:27 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXQju-0005g3-B0 for categories-list@mta.ca; Wed, 11 Feb 2009 21:51:42 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:76 Archived-At: 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 [1]. Then, using the type schemes devised by Luis Caires , 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 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 >