皆様

LMUミュンヘンのHelmut Schwichtenberg先生の講演のお知らせです。 どうぞふるってご参加ください。

問合せ先： 石原　哉 北陸先端科学技術大学院大学 情報科学系 e-mail: [email protected] -----------------------------------------------

* 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.