Prof. Helmut Schwichtenberg at NII Logic Seminar
Date: April 2, 2018, 14:00--16:00
Place: National Institute of Informatics, Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/)
Speaker: 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.
問合せ先: 龍田 真 (国立情報学研究所) e-mail: tatsuta@nii.ac.jp http://research.nii.ac.jp/~tatsuta