Lambda calculus for real analysis by Paul Taylor
Paul Taylor has published a revised version of his `lambda`-calculus for real analysis. I recommend it to anyone who is interested in real analysis, be it a computer scientist, numerical analyst, or just a “true” analyst.
The first, second, and third time I talked to Paul I could not understand a word of what he was saying, and that's not just because he is a native speaker of English English. I only began to “get it” when he visited me in Ljubljana. So I think it's perhaps worth explaining a bit what this “`lambda`-calculus for real analysis” is about.
Suppose you took a course in geometry which did not start with the primitive notions “point” and “line”, or the axioms they satisfy. Instead, the teacher would first talk briefly about rational numbers and equivalence relations, then explain that a point is an ordered pair of certain equivalence classes of Cauchy sequences of rational numbers, while a line is a set of points satisfying certain conditions which look like they were pulled out of thin air. The teacher would tell you that you just had to take it on faith that this was the best way to do geometry and that eventually you would develop deep intuition about what it was all about. He would masterfully use very complicated rulers to draw various configurations of lines and points. But when you tried to use the same tools, you would discover that the rulers are quite difficult to use and have razor-blade sharp edges (supposedly that allows more accurate drawings, and makes the rules useful in the kitchen, too). Your drawings would always come out crooked and often smudged with blood. Only with years of training could you understand “circles”, whatever that was (you have never seen a picture). Would that strike you as a strange way of teaching geometry?
Now consider how we teach traditional topology, the science about spaces and continuous maps. First we speak briefly about sets, then we tell the students that a space is a pair of sets, one of them being a subset of the powerset of the other, satisfying certain conditions which look like they were pulled out of thin air. The students just have to take it on faith that it all makes sense and that eventually they will appreciate the depth of the concepts. In addition, we teach them lots of powerful set-theoretic constructions which allow an expert to define whatever topological space or continuos map he wants (and set theory is useful in functional analysis, too). However, the students usually get their constructions wrong and define things which are not spaces and are not continuous maps. It takes them several years to appreciate the notion of compactness. Does this strike you as a strange way of explaining the science of continuum and continuity?
Just like geometry is expressed directly in terms of points and lines, it should be possible to formulate topology directly in terms of spaces and continuous maps. What would such a theory look like? Abstract Stone Duality (ASD) is Paul's answer to the question. The paper `lambda`-calculus for real analysis is an application of ASD to the space of real numbers and real maps.
I cannot possibly explain all the ideas that the paper contains. Suffice it to say that topology becomes much more logical (pun intended). For example, compact spaces are closely related to universal quantifiers `forall` and the Hausdorff property is just continuity of inequality `!=`. And there is a nice duality at work: the dual of “compact” (related to `forall`) is “overt” (related to `exists`), and the dual of “Hausdorff space” (`!=` is continuous) is “discrete space” (`=` is continuous). Paul shows how Dedekind cuts are related to definite descriptions and connectedness to modal operators. And because the theory allows a computational interpretation it gives novel ideas on how to compute with real numbers. This stuff is worth reading. If you have questions, I will happily answer them, and maybe Paul will join the discussion, too.
Is this different take on topology somehow related to Arntzenius's "Gunk, Topology and Measure": http://philsci-archive.pitt.edu/archive/00001792/ which also aims at defining pointless spaces. (I am not a mathematician)
Well, the paper you reference does not seem to be written by a professional mathematician so it is hard to judge exactly what its mathematical contents is supposed to be. But yes, it is "somehow related", as are many, many other works dealing with the idea that spaces are more than just collections of points. This is a topic that was discussed by various philosophers and mathematicians throughout history.
"... does not seem to be written by a professional mathematician so it is hard to judge exactly what its mathematical contents is supposed to be."
Well, Arntzenius is a philosopher: http://www.philosophy.ox.ac.uk/members/frank_arntzenius and of course, instead of having to "translate" cryptic mathematical notations into "ideas" the understanding has to go (for once...) the other way around, his proposals are on pp18-21 which may be you didn't reach.
"... the idea that spaces are more than just collections of points."
Don't you think that there is a strong and surreptitious platonistic slant in this very turn of phrase? (i.e. looking for the "essence" of spaces...) It's even more surprising since your work (as shown on this blog) appears to have a very pragmatic orientation, looking for "working solutions" rather than "grand metaphysical principles".
You are a bit rash in concluding my philosophical stand on the nature of mathematics from the word "are", especially since this particular "are" appears in a sentence which does not express my opinion. It only explains that there are many other works, apart from the one you cited, which deal with the idea that spaces are more than just collections of point. Ooops, I said it again. I am doubly Platonistic now. Please read more carefully what I write.
Even if I did say "spaces are more than just collections of points", how would that imply anything about my position about Platonism? In fact, I do say that spaces are more than just collections of points. But I am not a Platonist. I am just expressing my view as to what sort of mathematical objects geometry and topology are trying to (or should) capture.
As far as translating cryptic mathematical notation goes: I did look at the paper you reference. True, nothing is hiding in it behind cryptic mathematical notation. Just some old regurgitated ideas, with relevant references missing.
I am sorry if I offended you...
I apologize for sounding so harsh. I did not meant to. Of course you did not offend me. I was just a bit annoyed that you were misinterpreting what I said. I should have waited a bit before replying. Thank you for showing interest in my blog, and I hope I did not scare you away!
This paper has now appeared in the Journal of Logic and Analysis, vol 2 no 5, but is still available from my website using the link under my name above.