Lookahead analysis in exact real arithmetic with logical methods

Koepp, Nils and Schwichtenberg, Helmut (2022): Lookahead analysis in exact real arithmetic with logical methods. In: Theoretical Computer Science, Vol. 943: pp. 171-186

Abstract

Program extraction from proofs can be used to obtain verified algorithms in exact real arithmetic for e.g., the signed-digit code representation. In Minlog this has been done in the past with the use of certain coinductive predicates. In a next step we want to ana-lyze the lookahead of these extracted programs. Doing it by hand is quite cumbersome, so instead we change our definition. Instead of a coinductive predicate we use an induc-tive predicate for the representation of reals that already incorporates the lookahead. In this way the lookahead becomes part of the specification which is carried through all the proofs. In the end we extract programs for computations on a signed-digit representation and we can just read off the lookahead from the specification.(c) 2022 Elsevier B.V. All rights reserved.

• Item Type: Journal article
• Faculties: Mathematics, Computer Science and Statistics > Mathematics
• Subjects: 500 Science > 510 Mathematics
• ISSN: 0304-3975
• Language: English