From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5022 Path: news.gmane.org!not-for-mail From: Meredith Gregory Newsgroups: gmane.science.mathematics.categories Subject: Can you spot a flaw in this argument? Date: Thu, 25 Jun 2009 12:48:23 -0700 Message-ID: Reply-To: Meredith Gregory NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-7 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1246004823 4368 80.91.229.12 (26 Jun 2009 08:27:03 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 26 Jun 2009 08:27:03 +0000 (UTC) To: Categories Original-X-From: categories@mta.ca Fri Jun 26 10:26:56 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 1MK6lr-0004ux-V6 for gsmc-categories@m.gmane.org; Fri, 26 Jun 2009 10:26:56 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1MK63z-00061u-4Q for categories-list@mta.ca; Fri, 26 Jun 2009 04:41:35 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5022 Archived-At: All, This is an argument about effective theories and so i would love to hear from the topos-theory crowd. i'll state the argument in lowly computational terms, using two distinct proposals for foundational models of computing: the lambda calculus and the =F0-calculus. Both the lambda calculus and the =F0-calculus suffer a dependence on a theory of names (aka variables). Both require two things of whatever theory of names is provided to them: - at least countably infinitely many names - an effective equality on names Now, to this recent proposals[1] add a third constraint, namely - names are atomic -- they have no internal structure To my way of thinking these three constraints are incompatible. i cannot se= e how to make an effective equality on a countably infinite set of entities that have no internal structure on which to rest the equality check. It seems to me that the only possible expression of the equality is an infinit= e table which states the results of comparing every single pair of atoms -- which is not going to fit into any realizable model of computation of which i'm aware and understand. Is there a way around this? If there is, i would be eternally grateful to b= e enlightened. The reason i focus on foundational proposals for theories of computation is that one could drop the atomic requirement and allow names to have internal structure, but because of the other two constraints one is dangerously clos= e to sneaking into a supposedly foundational account a theory of names that i= s -- itself -- already sufficiently rich to model computation. (For example, in many implementations of lambda or =F0-calculus, names are ultimately represented as integers.) This would appear to undermine the foundational character of the model of computation in question. This has led me to constructions in which the internal structure of names *reflects* the structure of computations. In fact, this idea has a simple monadic characterization, but that's for another discussion. i've already posted to this list an intuitive account of red/black set theories that also side-step the issue of atoms with no structure which allows to recast the FM-Set-Theory-based accounts of names onto what appear= s to me to be the only construction that meets all the requirements mentioned above: sufficiently many names, effective equality, restricting internal structure of names to the structure of the proposal at hand. Again, if ther= e is a way to skate around this argumentation or debunk it, please consider this a sincere call for help to do so. Best wishes, --greg [1] See the Gabbay-Pitts papers on using FM-Set Theory for an account of fresh names and alpha-equivalence. --=20 L.G. Meredith Managing Partner Biosimilarity LLC 1219 NW 83rd St Seattle, WA 98117 +1 206.650.3740 http://biosimilarity.blogspot.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]