Talk by Prof. Helmut Schwichtenberg at NII Logic Seminar: "Logic for exact real arithmetic"
April 2 (Mon.)
National Institute of Informatics
Room 1208, 12th floor
Prof. Helmut Schwichtenberg (Munchen University)
Logic for exact real arithmetic
Real numbers in the exact (as opposed to floating-point) sense can be given in different formats, for instance as Cauchy sequences (of rationals, with Cauchy modulus), or else as infinite sequences (streams) of (i) signed digits -1, 0, 1 or (ii) -1, 1, bot containing at most one copy of bot (meaning undefinedness), so-called Gray code (di Gianantonio 1999, Tsuiki 2002).
We are interested in formally verified algorithms on real numbers given as streams. To this end we consider formal (constructive) existence proofs M and apply a proof theoretic method (realizability) to extract their computational content. We switch between different representations of reals by labelling universal quantifiers on reals x as non-computational and then relativising x to a predicate CoI coinductively defined in such a way that the computational content of x in CoI is a stream representing x.
The desired algorithm is obtained as the extracted term of the existence proof M, and the required verification is provided by a formal soundness proof of the realizability interpretation.
As an example we consider multiplication of reals.
This is a joint work with Ulrich Berger, Kenji Miyamoto and Hideki Tsuiki.
TATSUTA Makoto <tasuta [at] nii.ac.jp>