Exact computation over topological spaces

[frank waaldijk]

Dear all,

in December 2013 I submitted an article `Exact computation over topological spaces' to Logical Methods in Computer Science, having been invited to contribute to the special issue on CCA2013.

I haven't heard from LMCS since, and the paper is relevant (I believe) to current research in exact computation, continuous computation and constructive topology. 

Natural Topology (NToP) is especially relevant (I believe) to the upcoming Fifth Workshop on Formal Topology. NToP is practically the simplified BISH version of Brouwer's spreads, as I have posted before on this forum. Due to long-time health issues, I'm unable to attend such workshops, so the electronic highway will have to do.

For these reasons I have decided to now put the preprint of `Exact computation over topological spaces' on my math page. I would have liked to await the referees' comments before asking your attention, but it simply takes too long. You can find the abstract below. All comments are welcome. I would especially be interested in Andrej Bauer's comments, since the paper uses some of his research, and covers similar areas of exact computation. Similarly I would be interested to hear from Thierry Coquand whether NToP is what he had in mind in his 1996 preprint `Formal topology with posets', where he poses Question 0.4: `Maybe, following von Plato, it will be more elegant to start with an inequality on A instead?? Intuitively, we observe when two approximations differ. This is for instance the natural notion for Böhm trees.'

NToP starts with an apartness, but I know too little of type theory to see if these ideas correspond.

Best wishes to all,

Frank Waaldijk

http://www.fwaaldijk.nl/mathematics.html

ABSTRACT

We give an exposition of Natural Topology (NToP), which highlights its advantages for exact computation. The NToP-definition of the real numbers (and continuous real functions) matches the recommendations for exact real computation in [Bauer&Kavkler2008] and [Bauer&Kavkler2009]. We derive similar and new results on the efficient representation of continuous real-valued functions (defined on a suitable topological space). This can be generalized to continuous functions between suitable topological spaces. Other than in [Bauer&Kavkler2009], we do not need Markov’s Principle (but for practice this is a cosmetic difference).

NToP is a conceptually simple theory of topological spaces in BISH. It combines a pointfree with a pointwise approach, by integrating the partial-order on the topological basis with a pre-apartness relation. Simpler than formal topology and (constructive) domain theory, NToP enables a smooth transition from theory to practice. We define ‘natural reals’ as sequences of ‘sufficiently shrinking’ rational intervals. The construction directly yields an apartness topology which is equivalent to the metric topology.

A similar construction works for all ‘effective’ quotient spaces of Baire space (obtained through a $Sigma_{0,1}$-apartness). We work with a countable set of ‘basic dots’ which are usually basic neighborhoods. This allows for an efficient representation of compact spaces by finitely branching trees (contrasting to the framework of formal topology). For the natural reals, we can suffice with lean dyadic intervals. All our spaces are (also) pointwise topological spaces, enabling the familiar pointwise style of BISH and CLASS, as well as an incorporation of earlier constructive work in analysis.

The concept of ‘refinement morphism’ is seen to adequately capture the notion of ‘continuous function’. A refinement morphism simply sends basic dots to basic dots, in such a way that ‘points go to points’. In the case of the reals, every BISH-continuous real function can thus be represented by a morphism sending lean dyadic intervals to lean dyadic intervals. For a large class of spaces we prove that continuous functions can be represented by morphisms, that is if we work in CLASS, INT or RUSS. This then should be enough validation also for BISH. We conclude that NToP addresses the need expressed in [Bauer&Kavkler2008], to have a framework for constructive topology which is both theoretically and computationally adequate.

[Andrej Bauer]

Dear Frank,

I am vaguely familiar with your natural topology paper. I am afraid I
cannot devote time to your new paper just now because I have a rather
tall pile of refereeing/reviewing jobs to do (suffice it to say that
all of my digits are insufficient).

However, here are some quick remarks.

1. Seemingly innocuous theoretical moves are show stoppers in practice

You define reals in terms of intervals with rational endpoints. In
practice we do not use rationals but dyadic rationals. This seems like
a trivial change theoretically, but is not. Rationals form a field
whereas the dyadic rationals form an *approximate* field.

Another example: interval-based theories of real-number computation
usually assume that the interval operations are performed exactly,
i.e., [a,b] + [c,d] = [a+c, b+d]. But in practice this does not happen
and one always has to round things up and down very carefully and chop
off extra bits to save space. This creates an annoying disconnect
between theory and implementation.

So one ends up with "approximate everything" dyadic rationals with
approximate operations, rounding everywhere, and so on. Theoreticians
usually run away.


2. There are many types, not just the reals.

A comprehensive treatment of real-number computation must speak not
only about the reals, but about a calculus of types, of which the
reals are an example. A programming language always has an algebra of
types (products, exponentials, etc.) and so a theory of computation
needs to account for this structure. One way to phrase this is: what
is the categorical structure of your ambient category?


3. What about function spaces?

Continuing from the previous point, it is desirable to have function
spaces as "first-class" objects. Higher-order functions (integration,
differentiation, quantifiers, selection functionals) cannot be treated
systematically unless their domains of definition exist. In practice
you can get a lot of mileage by handling spaces of real functions, as
that gives you most of analysis. But of course it is better if you
have a cartesian closed category.

I consider the question "what is a good datatype for real functions?"
to be an open question. Should be use locally Lipschitz functions (a
la Abbas Edalat with lower and upper constants taking values in the
extended reals)? Or moduli of continuity? Or Paul Taylor's theory?


How does your theory fare with respect to the above three questions? I
recommend Paul Taylor's work as an example of a theory that is
sensitive to points 1 and 2, and at least aware of the importance of
3. But of course there are many others who worked in this area -- I am
just expressing my personal taste.

There is no shortage of theories of real-number computation, but there
is a severe shortage of implementations. With reals we are where the
integers were in 1980's. Nowadays it's common for programming
languages to have native support for big integers (Haskell, Python,
Java, OCaml), but one needs to install obscure libraries to get exact
reals. What we need is solid implementations of exact reals that can
be included as standard parts of programming languages. They will be
slow and laughed at first, but eventually someone will notice they
don't give bogus results, unlike floating point.

With kind regards,

Andrej

> --
> You received this message because you are subscribed to the Google Groups
> "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to constructivene...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[frank waaldijk]

Dear Andrej,

thanks for your quick reply, and your thoughtful remarks.

Let me try to address these remarks a little bit.

1) a) In NToP the reals are also defined as sequences of shrinking dyadic intervals. Real functions then can be represented by morphisms on these dyadic intervals, with lazy evaluation. This seems to be in rather close correspondence to the recommendations that you make in the two papers mentioned in the abstract above. But since I am not an expert at all in implementation, I will wait for you to find time to study this.

    b) The programmers' best solutions for rounding difficulties will indeed probably create a disconnect between theory and practice, that much is also explicitly acknowledged in the paper. But nonetheless it seems worthwhile to have a constructive theory of topology that is close to actual computing practice. 

2) Your second remark shows that my world is not so large... the paper does not claim to give a comprehensive treatment of real-number computation. I can imagine that the abstract in the end is too optimistic. It says: `We conclude that NToP addresses the need expressed in [Bauer&Kavkler2008], to have a framework for constructive topology which is both theoretically and computationally adequate.' 

This is meant as: NToP wants to help to find such a framework. It is not meant as that NToP already is that framework. And even then, the framework itself does not have to be the complete computational machinery...that is why it is a framework.

Looking around, I do not see any such framework that seems to fill the position. This can also easily be due to my very limited knowledge. You recommend Paul Taylor's work, so perhaps if I find the energy I will study it. It seems to me that formal topology is not suited for computation, and therefore I find NToP to be interesting enough to bring to attention. 

3) The space of the continuous real functions is again an NToP-space, and such functions are also representable by morphisms which send a dyadic interval to another dyadic interval (in such a way that reals go to reals). Does this mean that they are "first-class" objects? I would hope so, but I'm not sure what you mean. Several important function spaces can be similarly treated...but, function spaces in general are quite complicated, and I personally don't think there is a general solution. You are quite right that this is very relevant, but I am unaware of other frameworks which solve this question.

I completely agree with your remark that we need good real-number computation, and I have a lot of respect for all the effort of people trying to realise this. Maybe NToP can be of some help somewhere, maybe not... but the least I can do is bring it to the attention of the people working in these areas.

I hope to trigger your curiosity! But I understand your time problem. Thanks again for your interest,

best wishes,

Frank