[logic-ml] Talk by Ulrich Berger (17th January, 11.00-)

[Kazushige TERUI]

みなさま

今週木曜に京都大学にて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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20190115/8b7ec06f/attachment.html>