# Logic for exact real arithmetic

## TL;DR

This paper presents a method to extract a division algorithm for real numbers represented as digit streams from formal proofs using coinductive predicates, with implementation in Minlog and translation to Haskell.

## Contribution

It introduces a formal proof framework for real arithmetic with coinductive definitions and demonstrates extraction of executable algorithms from these proofs.

## Key findings

- Successfully extracted a division algorithm from formal proofs.
- Implemented the algorithm in Haskell for practical use.
- Validated the approach with experimental results.

## Abstract

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.