Limits of real numbers in the binary signed digit representation
We extract verified algorithms for exact real number computation from constructive proofs. To this end we use a coinductive representation of reals as streams of binary signed digits. The main objective of this paper is the formalisation of a constructive proof that real numbers are closed with resp...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-08-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/7310/pdf |
| _version_ | 1797268535991336960 |
|---|---|
| author | Franziskus Wiesnet Nils Köpp |
| author_facet | Franziskus Wiesnet Nils Köpp |
| author_sort | Franziskus Wiesnet |
| collection | DOAJ |
| description | We extract verified algorithms for exact real number computation from
constructive proofs. To this end we use a coinductive representation of reals
as streams of binary signed digits. The main objective of this paper is the
formalisation of a constructive proof that real numbers are closed with respect
to limits. All the proofs of the main theorem and the first application are
implemented in the Minlog proof system and the extracted terms are further
translated into Haskell. We compare two approaches. The first approach is a
direct proof. In the second approach we make use of the representation of reals
by a Cauchy-sequence of rationals. Utilizing translations between the two
represenation and using the completeness of the Cauchy-reals, the proof is very
short. In both cases we use Minlog's program extraction mechanism to
automatically extract a formally verified program that transforms a converging
sequence of reals, i.e.~a sequence of streams of binary signed digits together
with a modulus of convergence, into the binary signed digit representation of
its limit. The correctness of the extracted terms follows directly from the
soundness theorem of program extraction. As a first application we use the
extracted algorithms together with Heron's method to construct an algorithm
that computes square roots with respect to the binary signed digit
representation. In a second application we use the convergence theorem to show
that the signed digit representation of real numbers is closed under
multiplication. |
| first_indexed | 2024-04-25T01:34:02Z |
| format | Article |
| id | doaj.art-fc3f3d2ba9574d1a91936a6598c0a759 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:02Z |
| publishDate | 2022-08-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-fc3f3d2ba9574d1a91936a6598c0a7592024-03-08T10:39:30ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-08-01Volume 18, Issue 310.46298/lmcs-18(3:24)20227310Limits of real numbers in the binary signed digit representationFranziskus WiesnetNils KöppWe extract verified algorithms for exact real number computation from constructive proofs. To this end we use a coinductive representation of reals as streams of binary signed digits. The main objective of this paper is the formalisation of a constructive proof that real numbers are closed with respect to limits. All the proofs of the main theorem and the first application are implemented in the Minlog proof system and the extracted terms are further translated into Haskell. We compare two approaches. The first approach is a direct proof. In the second approach we make use of the representation of reals by a Cauchy-sequence of rationals. Utilizing translations between the two represenation and using the completeness of the Cauchy-reals, the proof is very short. In both cases we use Minlog's program extraction mechanism to automatically extract a formally verified program that transforms a converging sequence of reals, i.e.~a sequence of streams of binary signed digits together with a modulus of convergence, into the binary signed digit representation of its limit. The correctness of the extracted terms follows directly from the soundness theorem of program extraction. As a first application we use the extracted algorithms together with Heron's method to construct an algorithm that computes square roots with respect to the binary signed digit representation. In a second application we use the convergence theorem to show that the signed digit representation of real numbers is closed under multiplication.https://lmcs.episciences.org/7310/pdfmathematics - logic |
| spellingShingle | Franziskus Wiesnet Nils Köpp Limits of real numbers in the binary signed digit representation Logical Methods in Computer Science mathematics - logic |
| title | Limits of real numbers in the binary signed digit representation |
| title_full | Limits of real numbers in the binary signed digit representation |
| title_fullStr | Limits of real numbers in the binary signed digit representation |
| title_full_unstemmed | Limits of real numbers in the binary signed digit representation |
| title_short | Limits of real numbers in the binary signed digit representation |
| title_sort | limits of real numbers in the binary signed digit representation |
| topic | mathematics - logic |
| url | https://lmcs.episciences.org/7310/pdf |
| work_keys_str_mv | AT franziskuswiesnet limitsofrealnumbersinthebinarysigneddigitrepresentation AT nilskopp limitsofrealnumbersinthebinarysigneddigitrepresentation |