[logic-ml] Prof. Helmut Schwichtenberg at NII Logic Seminar

[Makoto Tatsuta]

         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 at nii.ac.jp
http://research.nii.ac.jp/~tatsuta