EVENT

Talk by Prof. Helmut Schwichtenberg at NII Logic Seminar: "Logic for exact real arithmetic"

Date:

April 2 (Mon.)

Time:

14:00-16:00

Place:

National Institute of Informatics
Room 1208, 12th floor

Speaker:

Prof. Helmut Schwichtenberg (Munchen University)

Title:

Logic for exact real arithmetic

Abstract:

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.

Contact:

TATSUTA Makoto <tasuta [at] nii.ac.jp>