Post 9mncfB1PxTUcq52YoS by jelle_dc@octodon.social
(DIR) More posts by jelle_dc@octodon.social
(DIR) Post #9mmT9M08VaTssXER2u by grainloom@cybre.space
2019-09-10T13:24:38Z
1 likes, 0 repeats
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 otherwisei'm like 99.999% sure there is no way to express that as actual computation
(DIR) Post #9mmT9MGnVdoBiD1k12 by lanodan@queer.hacktivis.me
2019-09-10T13:26:07.448731Z
0 likes, 0 repeats
@grainloom Well, it could be done in elixir with function guards, maybe Haskell too.
(DIR) Post #9mmTwvZr1fyVPCZqrI by grainloom@cybre.space
2019-09-10T13:28:42Z
0 likes, 0 repeats
@lanodan well, it operates on real numbersforgot to mention that part
(DIR) Post #9mmTwvo2AxJk7BDAxc by grainloom@cybre.space
2019-09-10T13:30:20Z
1 likes, 0 repeats
@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
(DIR) Post #9mmTww1VMs5omxVvxQ by grainloom@cybre.space
2019-09-10T13:32:02Z
0 likes, 0 repeats
@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
(DIR) Post #9mmTwwN84TOFs1dCfA by lanodan@queer.hacktivis.me
2019-09-10T13:35:02.370981Z
0 likes, 0 repeats
@grainloom Hmm, I guess you would have to transport rational number in tuples anyway and you could just check if p and q are integers.
(DIR) Post #9mmVNLjeUf7Y15K5Ds by grainloom@cybre.space
2019-09-10T13:42:25Z
0 likes, 0 repeats
@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
(DIR) Post #9mmVNLxTfGBChxn7lw by lanodan@queer.hacktivis.me
2019-09-10T13:51:02.257218Z
0 likes, 0 repeats
@grainloom Uh? "In mathematics, a rational number is any number that can be expressed as the quotient or fraction p/q of two integers"https://en.wikipedia.org/wiki/Rational_number
(DIR) Post #9mmX1PBlAnzsGS8MwS by grainloom@cybre.space
2019-09-10T14:04:21Z
0 likes, 0 repeats
@lanodan ye, but these are constructive reals, not (Either Real Rational)
(DIR) Post #9mmX1Q2E1jxqtAgGie by clacke@libranet.de
2019-09-10T14:09:19Z
0 likes, 0 repeats
@grainloom @lanodan In other words, showing that a given number can be expressed as a fraction is not trivial.It's hard for us to imagine how that could be, because we are so used to representing all numbers as approximate fractions.
(DIR) Post #9mme9ANSpAQKK9FxEO by yaaps@banana.dog
2019-09-10T15:13:29Z
2 likes, 0 repeats
@clacke @lanodan @grainloom Not trivial is an understatementProving rationality is subject to the halting problem because p and q can be arbitrarily largeProving irrationality involves setting your expression equal to p/q then applying algebraic transformations until the resulting form demonstrates a logical impossibility. Any algorithm deployed will depend on the function used to derive the quantity being tested. In the absence of a generalized algorithm for proving irrationality, the hypothetical function in the OP is uncomputable
(DIR) Post #9mn51Kn6v7BB4Dk57Q by rain@niu.moe
2019-09-10T20:30:26Z
0 likes, 0 repeats
@grainloom you are right, in intuitionist mathematics the computational functions R->R do not include these discontinuous pathological functions like the one you described
(DIR) Post #9mnE8ux9lgoopu8F9s by epicmorphism@satania.space
2019-09-10T22:12:40.745430Z
0 likes, 0 repeats
@grainloom @lanodan yeah it is not decidable for computable reals
(DIR) Post #9mncX0xhTdrZK1PRlg by RAOF@dev.glitch.social
2019-09-10T22:10:20Z
1 likes, 0 repeats
@grainloom @lanodan in the general case you can't decide whether two real numbers are equal.
(DIR) Post #9mnce5q5k3cgTYE4MC by clacke@libranet.de
2019-09-11T02:47:06Z
0 likes, 0 repeats
@RAOF @lanodan @grainloom But on the other hand hey, if you've shown that they're rational, then suddenly the equiality comparison becomes a piece of cake.
(DIR) Post #9mncfB1PxTUcq52YoS by jelle_dc@octodon.social
2019-09-10T13:31:51Z
0 likes, 0 repeats
@grainloom I mean the main problem is representing real numbers isn't it? Otherwise it's just a dynamic type check
(DIR) Post #9mncfBNkcRMDxLUOci by grainloom@cybre.space
2019-09-10T13:33:07Z
1 likes, 0 repeats
@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
(DIR) Post #9mncm0xrkWaLfqdi8u by RAOF@dev.glitch.social
2019-09-10T22:06:45Z
0 likes, 0 repeats
@grainloom it's pretty easy to express as a computation, actually: it's just x.Because any actual computation has finite precision, and so acts only on rationals.
(DIR) Post #9mncm1JUS7smkukyqe by clacke@libranet.de
2019-09-11T02:48:34Z
0 likes, 0 repeats
@RAOF @grainloom That's a narrow view of computation limited to what's practical and actually done.
(DIR) Post #9mncqeiDuVCI6jXHkG by grainloom@cybre.space
2019-09-10T22:07:43Z
0 likes, 0 repeats
@RAOF > Because any actual computation has finite precision, and so acts only on rationals.https://github.com/andrejbauer/marshallwhat about this then?
(DIR) Post #9mncqeyWvsF0vJAJA8 by RAOF@dev.glitch.social
2019-09-10T22:12:46Z
0 likes, 0 repeats
@grainloom that doesn't operate in the reals; it operates on a (countable!) subset of the reals.
(DIR) Post #9mncqfAwBkALXmyDVA by grainloom@cybre.space
2019-09-10T22:14:03Z
0 likes, 0 repeats
@RAOF still not finite precision tho, right?
(DIR) Post #9mncqfO3OyeqCT6gwi by RAOF@dev.glitch.social
2019-09-10T22:16:38Z
0 likes, 0 repeats
@grainloom it kinda depends on what you mean by “computation” 😜You can symbolically manipulate those things in ways which mimic computation. It's certainly interesting. Is it computation?
(DIR) Post #9mncqfhYEUFnAwEGKu by grainloom@cybre.space
2019-09-10T22:20:47Z
0 likes, 0 repeats
@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
(DIR) Post #9mncqftxUMB7nQ2Afw by grainloom@cybre.space
2019-09-10T22:21:06Z
0 likes, 0 repeats
@RAOF (or at least that's what i'm curious about)
(DIR) Post #9mncqg9CZgN6YhALR2 by grainloom@cybre.space
2019-09-10T22:21:55Z
0 likes, 0 repeats
@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??)
(DIR) Post #9mncqgRzRpOtUxxLii by anne@beach.city
2019-09-10T23:12:04Z
0 likes, 0 repeats
@grainloom @RAOF Some numbers can be proven non-algebraic by showing that there is a sequence of rationals that converges to them faster than polynomially. Still a proof problem, but one that can be easy for non-algebraic real numbers.
(DIR) Post #9mncqgjMPFIMMq5DnM by RAOF@dev.glitch.social
2019-09-10T23:18:05Z
0 likes, 0 repeats
@anne @grainloom Right, but there are necessarily calculations that you can specify which will not be exact (possibly because you can't actually perform them).For example: let x be the number specified as 1/2{number of bits of memory in the computer}. x/2 is now necessarily not exact, because you can't specify it.
(DIR) Post #9mncqgxtXCvB5uspRw by grainloom@cybre.space
2019-09-10T23:31:27Z
0 likes, 0 repeats
@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:
(DIR) Post #9mncqhFyRzNnzzLGd6 by RAOF@dev.glitch.social
2019-09-10T23:33:07Z
1 likes, 0 repeats
@grainloom @anne you quite rapidly run out of universe to convert into RAM 😜
(DIR) Post #9mncw4J0BOfSvoJt56 by anne@beach.city
2019-09-10T23:15:59Z
1 likes, 0 repeats
@grainloom @RAOF you're using the wrong language here - the string representation of python floats is (by definition and as implemented) precisely as many decimal digits as are needed to uniquely specify the float.(I think a round trip through strings might lose track of which NaN you have.)