Topic: real-valued logic
Alexandre Rademaker (Dec 18 2020 at 13:39):
Can you elaborate on that?
Kevin Buzzard (Dec 18 2020 at 13:44):
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 (Dec 18 2020 at 13:49):
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 (Dec 18 2020 at 14:11):
Hum... hi Kevin, thank you for your attention, programming languages use some approximation right? Evaluation couldn’t be bound to some approximation?
Alexandre Rademaker (Dec 18 2020 at 14:19):
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 (Dec 18 2020 at 14:46):
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 (Dec 18 2020 at 15:06):
Is it possible to spit out the first few digits of a real number inside something like an
Johan Commelin (Dec 18 2020 at 15:08):
It needs to be able to decide whether
x = 0.99999998 or
x = 1.000000001 to do that, right?
Johan Commelin (Dec 18 2020 at 15:08):
So maybe you want to allow it an error margin?
Anne Baanen (Dec 18 2020 at 15:09):
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 (Dec 18 2020 at 15:10):
Can you represent a real number as a sequence of nested intervals (whose length tends to zero)?
Anne Baanen (Dec 18 2020 at 15:10):
Brouwer does so IIRC, where the n'th interval has length at most 10^-n.
Adam Topaz (Dec 18 2020 at 15:10):
Yeah I think that's what Alex is suggesting.
Bryan Gin-ge Chen (Dec 18 2020 at 16:19):
#1038 has a few ideas too.
Kevin Lacker (Dec 18 2020 at 19:18):
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 (Dec 18 2020 at 19:42):
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 (Dec 18 2020 at 19:46):
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 (Dec 18 2020 at 19:48):
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 (Dec 18 2020 at 19:49):
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
Last updated: May 14 2021 at 04:22 UTC