Implement computable real numbers

[urkud]

Hi,

I'd like to have real numbers that can be used for in-kernel computations. I mean, it would be nice to have, e.g., a function pi.approx : ℚ₊ → ℚ with a proof |pi.approx r - pi| ≤ r.

The main issue is that this function cannot be implemented as approx : ℝ → ℚ₊ → ℚ. I can think about two (not mutually exclusive) approaches.

1. Define new

   struct creal := (approx : ℚ₊ → ℚ) (sound : ∀ r₁ r₂, |approx r₁ - approx r₂| ≤ r₁ + r₂)

   with a (strong) setoid structure, then migrate some (or most) theorems to deal with this setoid.

2. Define

   def approximates (x : ℝ) (f : ℚ₊ → ℚ) := ∀ r, |x - real.of_rat (f r)| ≤ r

   then prove lemmas like

   approximates x f → approximates y g → approximates (x + y) (λ r, f (r / 2) + g (r / 2)

[cipher1024]

That sounds like a cool idea! We do accept pull requests if you feel like working on it.

[robertylewis]

Exact real number computation is a subtle topic, and I think that choosing the correct approach will depend on your application.

There's a huge gap between "computable in principle" and "computable in practice." Are you really going after kernel computation? Even simple rational arithmetic can be slow: #check (rfl : (1 : ℚ) / 10 + 1 / 10 = 2 / 10) is far from instant. VM computation is more reasonable.

I'm not sure how familiar you are, but there's a good amount written about this in Coq, surrounding the CoRN (Computational Real Numbers) library. https://arxiv.org/pdf/0805.2438.pdf http://users-cs.au.dk/spitters/calculemus.pdf http://corn.cs.ru.nl/

[kbuzzard]

We know a whole bunch about sin and cos and tan, and it would not surprise me if one could prove in Lean, without too much trouble, that $$\pi/4=1-1/3+1/5-1/7+...$$. This would give you a famously inefficient function pi.approx that was of no practical use (I just summed the first 1000 terms and I got pi to two decimal places; however a simple lemma in real analysis guarantees that 1/2001-1/2003+1/2005-... is in the range [0,1/2001]). Would you be interested in that sort of thing (because I could push this sort of idea amongst the Imperial undergraduates) or do you actually want something useful for real computations? Approximating pi well is a perhaps niche (at least from where I'm sitting in a maths department) research area but some smart people have made great progress in this area in the last 30 years or so (basically because mathematicians now have access to fast computers, I guess, so the problem became somehow less obscure). I just mention this example because it's (at least from where I'm sitting) a very clear way of understanding Rob's comment. The rational number that you get from summing the first 1000 terms has numerator and denominator with over 860 digits in lowest terms.

[urkud]

Actually, I'm not sure what do I want. Ideally, I want some framework where

a) one can build “approximators” for various real numbers with sane (though probably computationally inefficient) defaults;
b) there are ways to tweak this process by choosing particular approximators at various steps.

E.g., a straightforward lemma

lemma approx_plus : approximates f x → approximates g y → approximates (λ r, f (r / 2) + g (r / 2)) y

is very inefficient, if one of the numbers is actually a rational number. So, it would be nice to have

lemma approx_plus_param (c : rat) (hc : 0 < c < 1) : approximates f x → approximates g y → approximates (λ r, f (c * r) + g ((1 - c) * r)) y

In order to actually compute something in a reasonable time, one would need to use particular instances here and there. As for π, it would be nice to have something more effective, e.g., based on one of those formulas π/4=∑a_k\atan r_k.

Re @robertylewis : I have quite some math background, but about zero experience in this particular area. I'll look more carefully at CoRN, then come back here.

[digama0]

I think that mathlib computable reals should be modeled after some framework for exact real computation in a conventional programming language e.g. C. This way, it stays as close to practical computation as possible. I think that at this point we've decided not to pursue "naively computable" things, since they don't come with many benefits. Instead we have the "purely mathematical" version (where noncomputable things are okay if they make proofs easier) and the "ruthlessly practical computational" version which is used for VM computation, with a proven relation to the mathematical version.

From my point of view the Leibniz formula for pi is on the "purely mathematical" side. It's useful to know abstractly that this sequence converges, but it's not a reasonable method for actually calculating pi.

On a computational type, there is no problem with having separate functions add and add_rat if a different implementation works better in this case. The advantage of having the purely mathematical construct real around is that it allows you to express what these functions do.

I've done some research on this topic before, and a popular method seems to be functions that take n as input and produce a natural number k such that abs (x - k*2^n) <= 2^n (or something similar). That is, λ n, f n/2^n is a cauchy sequence for x : real with explicit modulus of convergence.

Another aspect of these computable reals that is sometimes important is the ability to memoize previous values, since subcomputations tend to use them over and over. We still need to work on the lean side a bit to support memoization for functions (there is a current PR for lean 3.5c about interior mutability that should help here).

[semorrison]

By

some framework for exact real computation in a conventional programming language e.g. C

you mean for example some interval arithmetic library, rather than float?

[digama0]

Interval arithmetic is another direction we could go, and probably more practical too, but no, I actually mean a library for so called "exact real arithmetic", which entails the manipulation of functions as data to perform operations on cauchy sequence representations like I indicated above. For example:

• http://axiom-wiki.newsynthesis.org/public/refs/exact-real-p162-boehm.pdf
• http://hackage.haskell.org/package/exact-real
• http://irram.uni-trier.de/

[YaelDillies]

The basics of interval arithmetic are about to hit mathlib in #16761.

[urkud]

Let me close this issue.