Prof. Helmut Schwichtenberg Lecture at NII Logic Seminar
Date: February 21, 2013, 14:00--16:00
Place: National Institute of Informatics, Lecture Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/)
Speaker: Prof. Helmut Schwichtenberg (Ludwig Maximilian University of Munich)
Title: Proofs and computations with infinite data
Abstract: Ulrich Berger and Monika Seisenberger recently studied extraction from proofs involving (only) abstract reals. They considered a proof using coinduction of the proposition that any two reals in [-1,1] have their average in the same interval, and informally extract a Haskell program working with stream representations of reals. We report on a formalization of this proof, and a machine-extraction of its computational content, in the Minlog proof assistant. This required an extension of this system to also take coinduction into account. The underlying formal system is a theory TCF of computable functionals. It is similar to Heyting arithmetic in all finite types, but with the Scott/Ershov partial continuous functionals as the domain of quantifiers. TCF has free type, predicate and function variables, to allow for abstract developments (groups, fields, real analysis). The underlying inference machinery is minimal logic (implication, universal quantification plus inductively and coinductively defined predicates). Computable functionals (of finite type, with free algebras at ground types) are given by their defining equations. Since the logic is constructive, program extraction by means of a realizability interpretation is possible and a soundness theorem holds.
問合せ先: 龍田 真 (国立情報学研究所) e-mail: [email protected] http://research.nii.ac.jp/~tatsuta