Post #1782139
2026-04-27 21:47 UTC
Replies (2)
-
@screwlisp@gamerplus.org 2026-04-27 21:49
@simon_brooke acl2 and not coalton: Since ACL2 base does not have real numbers, we get the wonderful logical result "the square root of two does not exist". ( ACL2(r) exists for when it is important that there actually are irrational numbers). @vnikolov
-
@vnikolov@ieji.de 2026-04-28 03:36
@simon_brooke wrote: «Interestingly, SBCL doesn't think (√2)² = 2: CL-USER[1]: (sqrt 2) 1.4142135 CL-USER[2]: (* (sqrt 2)(sqrt 2)) 1.9999999» This kind of (correct) behavior is by far not specific to SBCL or even Lisp. Note that the value of (sqrt 2) (or sqrt(2) in other languages) is of course not √2, but an approximation. Maybe one expects that the above product tests exactly equal to 2 in a computer algebra system or better, but those are very different beasts; I don't think I have ever tried it myself, though. «I don't know how many bits SBCL's floating point representation is, but that sort of thing is exactly why I don't want to drop to floats when I don't have to.» Indeed, but I am not aware of a (very) smart representation of irrational algebraic numbers that is useful for doing ordinary calculations with them. If one has been found, that would be a great achievement. SBCL's `single-float' is 32 bits (as with many other implementations), but that is not particularly important in this context. To repeat the well-known, no floating-point format can represent exact values of irrational numbers. @screwlisp