tag:blogger.com,1999:blog-11295132.post4817033279790395322..comments2015-11-05T00:40:24.898-08:00Comments on A Neighborhood of Infinity: What is Topology?Dan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger12125tag:blogger.com,1999:blog-11295132.post-76194489954662390812008-04-07T20:21:00.000-07:002008-04-07T20:21:00.000-07:00I run into this post by accident, and I found thi...I run into this post by accident, and I found this outline of the basic (formal) topology ideas very interesting. I currently study a biological system that seems to be implementing very similar algorithms (as strange as it sounds). The work is submitted but not published yet, and I will probably post it online soon. I could send a link to it if you are interested.Yurihttp://www.blogger.com/profile/05097685480927120329noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-41778681076620256672008-03-15T01:19:00.000-07:002008-03-15T01:19:00.000-07:00This is the best motivation for the axioms of topo...This is the best motivation for the axioms of topology that I've ever seen, and the only one that's ever satisfied me! I've been searching for a motivation for a week or two, but I realize now that I was looking in the wrong places: geometry and analysis.<BR/><BR/>The more I learn about topology, the more misleading the common description of topology as "rubber sheet geometry" seems to be. Perhaps topologists ought to start using the slogan, "Topology is the study of affirmable sets"!Aaronhttp://www.blogger.com/profile/18281785407407667986noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-41089481053690640412008-02-25T10:30:00.000-08:002008-02-25T10:30:00.000-08:00Charles,Hey thanks! I found a few pages of his boo...Charles,<BR/><BR/>Hey thanks! I found a few pages of his book online here: http://books.google.com/books?id=9Hh_EoxeiV8C He is using 'affirmable' exactly how I'm using 'observable', including the comment on the top of page 9 about arbitrary unions.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-30614216368030979822008-02-25T06:46:00.000-08:002008-02-25T06:46:00.000-08:00You have given a good account of the "orthodox" de...You have given a good account of the "orthodox" definition in general topology, but motivated by computational observability, roughly as it was done in theoretical computer science in the (1970s? and) 1980s. However, Punya is quite right to query the meaning of the "arbitrary" unions and suggest that maybe they ought to be countable, because there is plainly a serious mis-match here between set theory and computation.<BR/><BR/>There is certainly a tradition in pure mathematics of restricting attention to countable unions. This is found in particular in probability and measure theory, because the unions correspond to sums of real numbers, which only exist when at most countably many of them are non-zero. For a similar reason, "cozero" sets in functional analysis (ie the subspaces on which real-valued functions take nonzero values) also form such a system. The definitions are prefixed with the Greek letter sigma (σ), though this seems a bizarre choice. More abstractly, a number of people in South Africa, in particular, study sigma-frames, ie lattices with countable joins over which finite meets distribute.<BR/><BR/>However, countability is the wrong idea. It is really just a mutilated form of set theory, which naturally generates and deals with larger "cardinalities". If you believe in set theory, you should accept these as part of the system. On the other hand, the mathematical objects that matter are already either countable or countably based, so this mutilation doesn't actually change very much. <BR/><BR/>Countability completely misses the point of computation. We should be talking about <B>recursive enumerability</B> (RE) instead. The set of non-terminating programs is countable in the classical sense but not RE. What sense does it make to make a parallel observation composed of parts that only qualify for inclusion if some other observation <I>fails</I> to be made?<BR/><BR/>There is another mathematical tradition that objects to the <I>arbitrary</I> unions because they are <B>impredicative</B>, ie the thing being defined lies amongst the data for the definition. I'm not going to try to explain this point of view in any detail, because, being a categorist, I am rather keen on universal properties, which are inherently impredicative. I shall just point out how arbitrary unions lead to a solution of the <B>halting problem</B>: given any program P, consider the union (in the sense of this blog) of all programs Q for which P&Q fails (ie P and Q do not both terminate); this gives the negation of P, ie a program that terminates iff P doesn't.<BR/><BR/>Recursive enumerability and/or predicativity are such fundamental ideas that they should really be built into the foundations, not bolted on afterwards. In other words, we want a type theory for all of our investigations that takes account of them from the start.<BR/><BR/>In the case of predicativity, this is what Per Martin-Löf's type theory does. Along with it come Peter Aczel's CZF (constructive Zermelo-Fraenkel set theory), and Formal Topology, on which there are a number of authors, most notably Giovanni Sambin, although I am not sure that they sing from quite the same hymn-sheet. Algebraic Set Theory (originally by André Joyal and Ieke Moerdijk, but now led by Steve Awodey) is a different tradition, but talks about similar ideas, and I hope to see some convergence in the next few years. In Formal Topology, there are no "arbitrary" open sets or unions thereof. Instead there are "basic" open sets that may perhaps be generated by some recursive process, along with rules for saying when certain families of them "cover" a finite intersection of others. This is entirely consistent with tradition in analysis, where open balls are used, rather than general open subsets. Recursive enumerability is somehow built in to the recursive nature of definitions in Martin-Löf type theory, although this relationship has not so far been laid out very clearly, so far as I am aware.<BR/><BR/>My theory, <A HREF="http://www.PaulTaylor.EU/ASD" REL="nofollow">Abstract Stone Duality</A>, is based on a different idea, but also ends up with recursive enumerability built in. Instead of regarding the system of open subsets as a <I>set</I> with the algebraic structure of meets and joins, it treats it as <I>another space</I>. The machinery for handling an algebraic theory and its models is provided by the categorical notion of <B>monad</B>, but please note that the category of algebras is the one called after Eilenberg and Moore, which is bigger than the Kleisli category that Eugenio Moggi used for his application of monads to computer science.<BR/><BR/>We can get a long way by "pretending" that the spaces have joins of chains, as in domain theory, without actually asserting this as an axiom. <I>Finite</I> meets and joins, along with the monadic structure and the <B>Phoa principle</B> that I mentioned in my <BR/><A HREF="http://sigfpe.blogspot.com/2008/02/how-many-functions-are-there-from-to.html" REL="nofollow">previous posting</A>, already recover a lot of the basic results about general topology. The next thing to add is the natural numbers object <B>N</B>, along with general recursion and <B>N</B>-indexed union. Then we already have a theory of general topology with recursively enumerable unions instead of arbitrary ones, and in particular the lattice of RE sets provides the topology on <B>N</B> itself. When we add an axiom for joins of chains, we get a complete theory of <B>computably based locally compact spaces</B>.Paul Taylorhttp://www.paultaylor.eu/ASD/lamcranoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-48378422970685106032008-02-25T01:29:00.000-08:002008-02-25T01:29:00.000-08:00Steven Vicker's textbook Topology via logic treats...Steven Vicker's textbook <I>Topology via logic</I> treats topology in a somewhat similar manner: not identical since he doesn't try to justify observability in terms of physical computation, but he does try to ground the intuitions of topology in terms of observability.Charles Stewarthttp://www.linearity.org/casnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-82907228911386079332008-02-24T22:00:00.000-08:002008-02-24T22:00:00.000-08:00It is interesting that the notionof a topology inv...It is interesting that the notion<BR/>of a topology involves two iterations<BR/>of the powerset: a set of subsets closed under ... .<BR/><BR/>There is another approach to topology,<BR/>sometimes called formal topology where<BR/>you start with neighbourhoods which<BR/>have an inclusion relation, and a <BR/>"covering" relation between neighbourhoods<BR/>and families or sets of neighbourhoods.<BR/>If these have the right properties, one<BR/>can <B>define</B> the notion of point<BR/>(using coinduction). <BR/><BR/>To find out about formal topology,<BR/>start at http://www.math.unipd.it/~sambin/.<BR/><BR/>The cover relation in formal topology<BR/>is a "higher order" relation, as it is<BR/>between a neighbourhood and a subset of<BR/>the neighbourhoods. So the whole<BR/>structure involves two iterations<BR/>of powerset.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-63766918238528485792008-02-24T21:12:00.000-08:002008-02-24T21:12:00.000-08:00Hi Dan, On your website you have a page comparing ...Hi Dan, <BR/>On your website you have a page comparing various x86 compilers and you say "Tell me how to get an assembly listing out of the free evaluation of this compiler and I'll test my code."<BR/>referring to the Digital Mars compiler. The compiler switch you are looking for is -cod.<BR/>Sorry to post this here but I couldn't find your e-mail address anywhere.Jackhttp://www.blogger.com/profile/04805435564360543720noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-64332996600740886412008-02-24T07:48:00.000-08:002008-02-24T07:48:00.000-08:00Good stuff! I would only add a short paragraph to ...Good stuff! I would only add a short paragraph to explain that the intersection of an infinite collection of observable sets does not have to be observable.Peterhttp://cvfordummies.comnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-9685923622361868062008-02-23T18:43:00.000-08:002008-02-23T18:43:00.000-08:00Luke,One statement of the compactness theorem is p...Luke,<BR/><BR/>One statement of the compactness theorem is precisely that the set of all valuations in propositional calculus forms a compact space when endowed with the right topology. But I haven't defined compactness in this post.<BR/><BR/>For completeness: A cover of a topological space is a (possibly infinite) set of open spaces whose union is the entire space. A subcover is a subset of these sets whose union is still the entire space. A compact space is one where every cover has a finite subcover. That has a nice interpretation in terms of what I call observability but this box really is too small.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-37385108327055031132008-02-23T18:32:00.000-08:002008-02-23T18:32:00.000-08:00"But every Ui is observable, so there is some comb..."But every Ui is observable, so there is some combination of machines that can prove x in Ui"<BR/><BR/>That sounds an awful like the compactness theorem I know from logic. Because of the name of that theorem, I suspect first order logic forms a topology where the open sets are the sets of satisfiable sentences.<BR/><BR/>Thanks for this intro. Topology is a big area of math that I've seen very little of.Lukehttp://www.blogger.com/profile/09807388788677769669noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-70965331653122596472008-02-23T18:03:00.000-08:002008-02-23T18:03:00.000-08:00No, I mean arbitrary unions. As I (briefly) mentio...No, I mean arbitrary unions. As I (briefly) mentioned, I'm not assuming there is an algorithm to determine which set in an arbitrary union to use, just that there is one. This means that the analogy with computability isn't exact. Escardo discusses this subject here: http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf where he finds a way to make the analogy exact. But I'm interested in going the other way, seeing if there are useful intuitions about general topology that can be gained from thinking about the computer science angle.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-75758595644214006872008-02-23T17:46:00.000-08:002008-02-23T17:46:00.000-08:00It seems your arbitrary unions are in fact countab...It seems your arbitrary unions are in fact countable unions. Is that just to keep the exposition simple, or is this computability-theoretic analogy not exact?Punyahttp://www.blogger.com/profile/05291490934126560979noreply@blogger.com