Computer Science – Logic in Computer Science
Scientific paper
2011-06-17
Computer Science
Logic in Computer Science
Scientific paper
Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. Previously, we provided [arXiv:1105.2751v1] a fast implementation of the exact real numbers in the Coq proof assistant. Our implementation improved on an earlier implementation by O'Connor by using type classes to describe an abstract specification of the underlying dense set from which the real numbers are built. In particular, we used dyadic rationals built from Coq's machine integers to obtain a 100 times speed up of the basic operations already. In this article, we discuss various extensions of the implementation. First, we implement and verify the sine and cosine function. Secondly, we create an additional implementation of the dense set based on Coq's fast rational numbers. Thirdly, we extend the hierarchy to capture order on undecidable structures, while it was limited to decidable structures before. This hierarchy, based on type classes, allows us to share theory on the naturals, integers, rationals, dyadics, and reals in a convenient way. Finally, we obtain another dramatic speed-up by avoiding evaluation of termination proofs at runtime.
Krebbers Robbert
Spitters Bas
No associations
LandOfFree
Type classes for efficient exact real arithmetic in Coq does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Type classes for efficient exact real arithmetic in Coq, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Type classes for efficient exact real arithmetic in Coq will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-695858