3 ms·
Square root of two represented exactly in Haskell (turing equivalent): newtype Real = Real { isGreaterThan :: Rational -> Bool } sqrt2 :: Real sqrt2 = Real (\
by tathougies 8y ago
Square root of two represented exactly in Haskell (turing equivalent):
newtype Real = Real { isGreaterThan :: Rational -> Bool }
sqrt2 :: Real
sqrt2 = Real (\r -> r * r < 2)
Doing arithmetic on these numbers is a more complicated matter. But this representation is exact.
- gowld 8y agoperhaps for clarity write that as newtype Real = Supremum { isGreaterThan :: Rational -> Bool } sqrt2 :: Real sqrt2 = Supremum (\r -> r * r < 2)
- kps 8y ago√2 is a bad example for this purpose; there are only countably many algebraic numbers.
- tathougies 8y agoMy representation is countable, but not because of the fact it uses the algebraic term 'r * r' in its definition of sqrt(2). My representation is based on dedekind cuts, implemented in Haskell, which is based on the lambda calculus. There are countably many lamdda terms. Thus, I can only represent countably many real numbers. My representation can store all the computable numbers, but there are computable numbers that are not algebraic. For example, e is not algebraic, but it is computable. Here is a representation of e factorials :: Rational factorials = 1:zipWith (*) [1..] factorials eApproxes :: [Rational] eApproxes = scanl (+) 0 (map recip factorials) e :: Rational e = Rational (\r -> any (r <) eApproxes)