皆様
LMUミュンヘンのHelmut Schwichtenberg先生の講演のお知らせです。 どうぞふるってご参加ください。
問合せ先： 石原 哉 北陸先端科学技術大学院大学 情報科学系 e-mail: ishihara@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.