皆様
LMUミュンヘンのHelmut Schwichtenberg先生の講演のお知らせです。
どうぞふるってご参加ください。
問合せ先：
石原 哉
北陸先端科学技術大学院大学 情報科学系
e-mail: ishihara(a)jaist.ac.jp
-----------------------------------------------
* JAIST Logic Seminar Series *
* The seminar below is held as a part of JSPS Core-to-Core Program,
A. Advanced Research Networks and EU Horizon 2020
Marie Skłodowska-Curie actions RISE project CID
(http://www.jaist.ac.jp/logic/ja/core2core, http://cid.uni-trier.de/).
Date: Wednesday 6 March, 2019, 15:20-17:00
Place: JAIST, Collaboration room 7 (I-56)
(Access: http://www.jaist.ac.jp/english/location/access.html)
Speaker: Professor Helmut Schwichtenberg (Mathematisches Institut, LMU
Muenchen)
Title: Equality and extensionality
Abstract:
We sketch a theory of computable functionals (TCF) based on
finitary algebras given by their constructors. Its intended semantics
admits non-total functionals. For closed algebras of level zero we
allow infinite stream-like objects. For higher types we define
(pointwise) equality as a logical relation, and extensionality by
diagonalization of equality. We define realizability and -- in the
spirit of Kolmogorov (1932) -- add an invariance axiom: every
computationally relevant (c.r.) formula A is equivalent to the
existence of an extensional realizer of A. Then we can prove (ordinary
and dependent) choice, and also a soundness theorem stating that the
computational content extracted from a proof of a c.r. formula A
realizes A.
