search

cartazio / numbers

Other
29 stars 13 forks source link

toRational for CReal? #28

Open arrowd opened 6 years ago

arrowd commented 6 years ago

I see there is a implementation for instance Real CReal, but its toRational implementation is commented out:

 -- toRational x@(CR x') = x' n % 2^n where n = digitsToBits digits

  toRational _ = error "CReal.toRational"

What's wrong with it?

cartazio commented 5 years ago

constructive reals Cant be turned into a finite representation in finite time.

a simple example is PI, clearly a Computable / constructive real.... theres no rational number equal to pi!

more broadly, theres no decidable way to know if theres a finite rational rep from the current CReal rep