Home

A Lambda Calculus for Real Analysis

A Lambda Calculus for Real Analysis

Abstract Stone Duality is a revolutionary paradigm for general topology that describes computable continuous functions directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis.

This language is applied to the Intermediate Value Theorem: the solution of equations for continuous functions on the real line. As is well known from both numerical and constructive considerations, the equation cannot be solved if the function "hovers" near 0, whilst tangential solutions will never be found.

In ASD, both of these failures and the general method of finding solutions of the equation when they exist are explained by the new concept of overtness. The zeroes are captured, not as a set, but by higher-type modal operators. Unlike the Brouwer degree, these are defined and (Scott) continuous across singularities of a parametric equation.

Expressing topology in terms of continuous functions rather than sets of points leads to treatments of open and closed concepts that are very closely lattice- (or de Morgan-) dual, without the double negations that are found in intuitionistic approaches. In this, the dual of compactness is overtness. Whereas meets and joins in locale theory are asymmetrically finite and infinite, they have overt and compact indices in ASD.

Overtness replaces metrical properties such as total boundedness, and cardinality conditions such as having a countable dense subset. It is also related to locatedness in constructive analysis and recursive enumerability in recursion theory.

Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated Jean-Yves Girard's regrettably out-of-print Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX.

By Paul Snively at 2010-02-16 22:00 | Category Theory | Functional | Lambda Calculus | Logic/Declarative | Meta-Programming | Semantics | Type Theory | other blogs | 15865 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Neat.

Thanks for bringing this to my attention, after the recent Continuity Analysis of Programs [LtU]. I'll take a look at this; it may influence how I represent real number expressions in my language.

By dmbarbour at Tue, 2010-02-16 22:26 | login or register to post comments

Interesting Work

The Abstract Stone Duality work is quite interesting (though it hasn't progressed as fast as would be nice, and the Latex generated website is a bit unfortunate...).

I'm positive that I first heard about it here on LtU years ago (probably mentioned by Frank Atanassow), but googling around didn't seem to find any mention of it.

Anyone else recall this?

By Marc Hamann at Tue, 2010-02-16 23:31 | login or register to post comments

His book, "Practicical Foundations of Mathematics"

Paul Taylor's book was mentioned favorably by John Baez in his "This Week's Finds in Mathematical Physics," probably back around 2003 or so. I ordered the book and read and reread the early chapters many times. (For some reason the early chapters are more accessible to me...I think because there are more historical notes and mentions of connections to other areas, perhaps because about halfway through the book gets into really high-gear.)

This book, plus Baez's papers on categorification, re-ignited my interest in programming language theory, which led to LtU at around that time (though I didn't formally join until years later, and have generally tried to listen and learn and not spout off about things I haven't fully grokked). It also got me interested in FP, Haskell, and laziness, for which I am very grateful. I also followed Frank Atanassow's postings, and debates, with great interest. The big "flame war" (sort of) over types was immensely stimulating....too bad Frank doesn't post here anymore (or much of anywhere, it seems)

Martin Escardo has also done a lot of work on the "topological" side of computing, even implementing big parts of general topology in Haskell. And the book "Topology via Logic," by Steve Vickers, has a slightly different spin on things.

The recent big paper by Baez and Mike Stay,"Physics, Topology, Logic and Computation: A Rosetta Stone," is fascinating.

Whether quantum computers are even practical (or even can exist) is unclear to me, obviously, but if they are possible, with enough qubits and enough quantum error correction to be interesting, it'll be fascinating to find ways to program them. I expect FP and lazy-centric approaches will be crucial.

By Tim May at Wed, 2010-02-17 19:32 | login or register to post comments

Ouch

The big "flame war" (sort of) over types was immensely stimulating...

I hope you mean in something more than the red-meat sense. I consider it one of my most shameful threads here, and that's saying quite a bit. I considered asking Ehud and Anton to take my "contributions" there down, but in the end I felt that that would be intellectually dishonest.

...too bad Frank doesn't post here anymore (or much of anywhere, it seems)

Amen.

I didn't formally join until years later, and have generally tried to listen and learn and not spout off about things I haven't fully grokked).

As admirable as I think that is in important ways, I want to encourage you to post here regardless of whether you feel like you fully grok the subject at hand. The payoff for the many errors I've made here has been the response from the many people here who are both better informed than I, and, it goes without saying, more patient. There's no question in my mind that I would learn a great deal from your posts, and I hope that you would find that your experience in doing so would echo my own. :-)

By Paul Snively at Wed, 2010-02-17 21:59 | login or register to post comments

I should've called it a "spirited debate"

If this is the same type theory "debate" I am thinking of, it had Frank on the one side, forcefully arguing that a static type system is actually no more restrictive than non-static typing, e.g., one can always set a very general default type and be none the worse off for it.

I didn't think the thread was mean-spirited, though it got intense a few times.

This thread motivated me to get Pierce's book, for example.

I've come to think of types as vastly more important than as mere aids to helping with program correctness. In the "extended Curry-Howard isomorphism" slogan sense, "types are spaces," that is, spaces where certain things are true and other things are not. A set comprehension, in the standard mathematical notation sense, {a

Weirdly, wonderfully, in many important ways "topology is the mathematics of computation." More so than just logic is, and certainly more so than discrete mathematics, numerical calculations, or even algebra is. I never thought of it this way before reading some of the papers of Taylor, Vickers, Hyland, Escardo, Dana Scott, and others.

A lot of this seems pretty obvious now. And with so many great books and papers covering a lot of this, I don't see any reason to post cheerleader articles. (Usually if I can't figure something out, which is often!, I go back to the books and papers, which is why I don't ask dumb questions here.)

Also, this list or blog or whatever it is has a wide range of backgrounds, from notable language designers and type theory professors to students. For better or for worse, this tends to cause me to post less than on some other lists I've been on over the years.

A great site, or list, by the way.

By Tim May at Wed, 2010-02-17 23:24 | login or register to post comments

has a wide range of

has a wide range of backgrounds, from notable language designers and type theory professors to students. For better or for worse, this tends to cause me to post less

The hope, of course, is to achieve the opposite effect.

By Ehud Lamm at Thu, 2010-02-18 00:25 | login or register to post comments

It's a way of thinking

If you still know your undergraduate analysis and topology, you might conclude that there is "nothing new" in Paul's paper. But there is. It's the way he thinks and does real analysis which is new. So you have to read the paper with an open mind.

By andrejbauer at Wed, 2010-02-17 11:24 | login or register to post comments