Logic for exact real arithmetic
Continuing earlier work of the first author with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-04-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5419/pdf |
| _version_ | 1797268558342782976 |
|---|---|
| author | Helmut Schwichtenberg Franziskus Wiesnet |
| author_facet | Helmut Schwichtenberg Franziskus Wiesnet |
| author_sort | Helmut Schwichtenberg |
| collection | DOAJ |
| description | Continuing earlier work of the first author with U. Berger, K. Miyamoto and
H. Tsuiki, it is shown how a division algorithm for real numbers given as a
stream of signed digits can be extracted from an appropriate formal proof. The
property of being a real number represented as a stream is formulated by means
of coinductively defined predicates, and formal proofs involve coinduction. The
proof assistant Minlog is used to generate the formal proofs and extract their
computational content as terms of the underlying theory, a form of type theory
for finite or infinite data. Some experiments with running the extracted term
are described, after its translation to Haskell. |
| first_indexed | 2024-04-25T01:34:23Z |
| format | Article |
| id | doaj.art-531fa55311f54e1bacc71e9c66825b5e |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:23Z |
| publishDate | 2021-04-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-531fa55311f54e1bacc71e9c66825b5e2024-03-08T10:33:57ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-04-01Volume 17, Issue 210.23638/LMCS-17(2:7)20215419Logic for exact real arithmeticHelmut SchwichtenbergFranziskus WiesnetContinuing earlier work of the first author with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assistant Minlog is used to generate the formal proofs and extract their computational content as terms of the underlying theory, a form of type theory for finite or infinite data. Some experiments with running the extracted term are described, after its translation to Haskell.https://lmcs.episciences.org/5419/pdfmathematics - logic |
| spellingShingle | Helmut Schwichtenberg Franziskus Wiesnet Logic for exact real arithmetic Logical Methods in Computer Science mathematics - logic |
| title | Logic for exact real arithmetic |
| title_full | Logic for exact real arithmetic |
| title_fullStr | Logic for exact real arithmetic |
| title_full_unstemmed | Logic for exact real arithmetic |
| title_short | Logic for exact real arithmetic |
| title_sort | logic for exact real arithmetic |
| topic | mathematics - logic |
| url | https://lmcs.episciences.org/5419/pdf |
| work_keys_str_mv | AT helmutschwichtenberg logicforexactrealarithmetic AT franziskuswiesnet logicforexactrealarithmetic |