みなさま
今週木曜に京都大学にてUlrich Bergerさんによるご講演があります。 詳細は下記の通りです。よろしければご参加ください。
京都大学数理解析研究所 照井一成
========== Time: 11:00-12:00, 17th January, 2019 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学 本部構内 総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34)
Speaker: Ulrich Berger (Swansea University)
Title: Extracting the Fan Functional
Abstract: Consider a continuous functional F : (N -> B) -> N where N is the type of natural numbers and B is the type of Booleans, both endowed with the discrete topology, and the function space N -> B carries the pointwise topology. By a compactness argument (Koenig's Lemma or Fan Theorem), F is uniformly continuous. Therefore, there exists a least modulus of uniform continuity for F, that is, a least natural number m such that F equates any two arguments that coincide below m. The mapping F |-> m is called Fan Functional. Gandy showed that the Fan Functional is computable. Later it was shown that it is computable even in the restricted sense of Kleene's schemata (S1-S9), or, equivalently, PCF. In this talk we show that the Fan Functional is the computational content of a constructive proof of the uniform continuity of F.