it's weird that in math you can talk about a function f(x) that returns x if x is a rational number and -x otherwise
i'm like 99.999% sure there is no way to express that as actual computation
it's weird that in math you can talk about a function f(x) that returns x if x is a rational number and -x otherwise
i'm like 99.999% sure there is no way to express that as actual computation
@lanodan well, it operates on real numbers
forgot to mention that part
@lanodan
i know of one way to define the reals constructively in a dependent type system, and i'm fairly sure that in the general case, you can't algorithmically decide if one of them corresponds to a rational number
@lanodan basically you'd have to be able to find the limit of arbitrary series of rational numbers annnnnnd i don't have a proof i can point to but i strongly suspect that is not possible in the general case
@jelle_dc ye, and the representation that i know uses functions and proofs that they are Cauchy series, and things involving comparisons between functions are tricky
@lanodan
hmmmmmm, but how do you know the series converges to one? only its cauchiness proof is known, and that doesn't include the convergence point
@lanodan ye, but these are constructive reals, not (Either Real Rational)
@grainloom you are right, in intuitionist mathematics the computational functions R->R do not include these discontinuous pathological functions like the one you described
> Because any actual computation has finite precision, and so acts only on rationals.
https://github.com/andrejbauer/marshall
what about this then?
@RAOF and if it's using a finite precision, it's not the same function
@grainloom @lanodan in the general case you can't decide whether two real numbers are equal.
@RAOF still not finite precision tho, right?
@RAOF i guess so, except the number you get in the end can't simply be printed as decimal digits???
but not even floats are printed to their full precision afaik (and i'm kinda sad that i didn't find a way to do that with printf), what should matter is if this method of computation results in better approximations than floats/doubles/bignum rationals
@RAOF
(or at least that's what i'm curious about)
@RAOF
(also constructive reals seem to be the best way to deal with reals in type theory?? so if one wanted to prove things about them, this is how they'd do it??)
@grainloom I would not bother trying to deal with reals; they're one of the causes of 20th century mathematics' great failure.
You never encounter a real, only a computable number. (You can specify uncomputable numbers, but you can't do anything with them!)
@RAOF hmmm, i guess so
and there is that new floating point format thingy that packs Even Moar Numberz
@RAOF tbh I just wish I could transcribe my real analysis notes in some kinda dependently typed thingy, hence my interest
@RAOF if those notes resulted in code that i could run, all the better
@RAOF @anne You can, if you suppose that every time you run into an OOM error some magical force (human operator) will just re-run the computation with twice as much RAM :blobshrug:
@RAOF @grainloom You lose greater-than and close-to, yes, so some questions about these things you can't answer. Others you can. There are certainly computations you can do with these non-computable numbers. Computability is nuanced.
LoadAverage is a social network, courtesy of xrevan86, saintfury, pztrn. It runs on GNU social, version 2.0.0-dev, available under the GNU Affero General Public License.
All LoadAverage content and data are available under the CC-BY-3.0 license.