real-valued logic

Stream: general

[Alexandre Rademaker]

Can you elaborate on that?

[Kevin Buzzard]

What kind of an answer do you expect to get if you attempt to "evaluate" (whatever that means) an arbitrary real number computed as a sup?

[Mario Carneiro]

Indeed, I think the fact that they are uniquely suitable for doing logic is intrinsically linked to the fact that they are not computable, because this would otherwise imply that arbitrary formulas can simply be evaluated to a truth value, which is obviously false for nondecidable propositions

[Alexandre Rademaker]

Hum... hi Kevin, thank you for your attention, programming languages use some approximation right? Evaluation couldn’t be bound to some approximation?

[Alexandre Rademaker]

Hi Mario, once more, maybe a silly question... but what do you mean for nondecidable proposition? 1) A proposition for which we can’t find the truth assignment (interpretation) that make it true/false or; 2) a proposition for which given a truth assignment (interpretation) we can’t evaluate it’s truth value?

In general (2) is “easy” and (1) can be undecidable, right? But we may be talking about different things...

[Alex J. Best]

Reals with approximations (some sort of interval / ball arithmetic) that allow one to compute the first few digits of a real number would be cool type to have in mathlib, but mathlibs real is not defined this way. It is defined the mathematical way as quotients of Cauchy sequences of rationals, so even computing the first few terms of this cauchy sequence doesn't actually tell you anything about the real number, as the sequence is only guaranteed to be eventually close to whatever real it converges too.

[Adam Topaz]

Is it possible to spit out the first few digits of a real number inside something like an IO monad?

[Johan Commelin]

It needs to be able to decide whether x = 0.99999998 or x = 1.000000001 to do that, right?

[Johan Commelin]

So maybe you want to allow it an error margin?

[Anne Baanen]

Apart from that, you need to make sure to bound the rate of convergence of the sequence. It could be the sequence is 0 for the first 9999999999 terms and then jumps to 1.

[Heather Macbeth]

Can you represent a real number as a sequence of nested intervals (whose length tends to zero)?

[Anne Baanen]

Brouwer does so IIRC, where the n'th interval has length at most 10^-n.

[Adam Topaz]

Yeah I think that's what Alex is suggesting.

[Bryan Gin-ge Chen]

#1038 has a few ideas too.

[Kevin Lacker]

what you typically do in non-Lean programming when you are fidgeting about precision is instead of using a real number stored as a variable, you use functions like f(epsilon) where f returns an approximation that is correct within epsilon. which is kind of what that PR proposes. it's not really clear to me what problem this is trying to solve, but I think that will be more tractable for exact computation than handling reals as a sequence of things.

[Mario Carneiro]

One design question that comes up when doing real computations is whether to work "forward" or "backward" to get the approximation order. With computable reals, you are usually working backward, meaning that each step in the computation is given a target approximation order and gets to pick the approximation order to request of its inputs. By contrast, in interval arithmetic, you generally say that the inputs are given at some approximation order, and then you work forward to find out how much accuracy you can get for each of the intermediate steps; at the end you get some approximation level and if that's not good enough then you redo the whole computation at higher accuracy.

[Mario Carneiro]

I think the latter method is more appropriate for actual verified computations, since you can encode the good enough initial approximation order pretty easily as a witness in the script. Most of our numerical computations (such as the calculations of e and pi) are like that

[Mario Carneiro]

the nice thing about the former (computable reals) method is that it is more well encapsulated; you actually get something that you can call a "real number", namely a function which given a target approximation will provide a rational which is at least that close to the true value

[Mario Carneiro]

you can even mostly use it to replace the real type itself, if you take an appropriate quotient. The quotient kind of destroys your ability to get actual answers to questions though