プログラム

最終更新日時: Last modified: 2020-09-07

実際の講演順です。事後ですが，未記載だった梗概も追加しました。

10:00 ～ 10:15 

    オープニング＋連絡など

10:15 ～ 10:45 

浦本武雄（長浜バイオ大学）

演題：変形理論としての計算理論

梗概：

古典的なEilenberg理論の公理化・ガロア理論との統一から始まった一連の研究について、最近の観察を軸にして、その概要を紹介する。技術的に言えば本講演の主題は、「代数体Kが虚二次体であるときに、K上のalgebraic witt vectorのなすK代数が、モジュラー関数の変形族の特殊値によって定義されるベクトルのなすK代数と一致する」という現象に関わる。この現象に現れる主要概念とラングランズプログラムに現れる主要概念との類似を比較しながら、非可換類体論（および明示的類体論）のラングランズプログラムとは異なる定式化について考えたい。また古典的な計算理論における研究対象がこの現象の中でどのような役割を担うかを観察しながら、計算理論の古典的（で離散的）な対象を代数幾何学の文脈に自然に位置付けることが（も）できるのではないかという可能性についても議論したい。

11:00 ～ 11:30 

長谷川真人（京都大学）

演題：Lifting traced monoidal structure to the categories of algebras(work on progress)スライド(link)

梗概：

Given a monad on a category, we have the notion of algebras for the monad, and can construct the category of algebras and algebra homomorphisms (the Eilenberg-Moore category). When the category is equipped with some nice structure, it is natural to ask if the structure can be lifted to the category of algebras so that the forgetful functor preserves the structure. Such situations are ubiquitous in various areas of mathematics, physics and computer science.

In this talk we discuss conditions on monads for lifting the structure of monoidal categories (tensor categories), as well as several additional structures including symmetry/braiding, duality, closed structure, *-autonomy, and trace. In most cases, opmonoidal (= oplax monoidal) monads and Hopf monads provide satisfactory answers. However, the case of trace is subtle and seems to be still open.

(Joint work with J.S. Lemay)

12:30 ～ 13:00 

佐々木克己（南山大学）

演題：難しい推論と易しい推論の意味論的な区別について

梗概：

自然演繹法の体系では，一時的な仮定をもつ推論規則がある．それらに対応づけられる推論は，そうでない推論と比べ，難しいと捉えられることが多い．本発表では，その2種類の推論を区別する形式体系を整理しその意味付けを行う．

13:15 ～ 13:45 

南規楽（京都大学）

演題：tracking reactive systemのための論理

梗概：

tracking reactive systemは、反応の前後で何をどのように引き継いでいるか、という情報を加えたreactive systemである。[Leifer, 2001]の方法に基づき、idem pushoutを用いてlabeled transition systemを構成する。そのようにして得られるLTSのふるまいを記述する論理を提案する。

14:00 ～ 14:30 

新屋良磨（秋田大学）

演題：正則可測性：正則言語による極限的な近似可能性

梗概：

本講演では，正則可測性という，正則言語によるある種の「極限的な近似可能性」概念を導入し，種々の文脈自由言語の正則可測性・非可測性について解説する．また，正則可測性を考察する動機となったBuckによる自然数の部分集合に対する測密度の研究や原始語予想と呼ばれる未解決問題についても説明する．本講演の内容は[1]のプレプリントに基づく．

[1] Ryoma Sin’ya, Asymptotic Approximation by Regular Languages, available at https://arxiv.org/abs/2008.01413

10:00 ～ 10:30 

山本雄太（東京大学）

演題：HoTTの改変による微分形式の推論とその意味論

梗概：

  Homotopy type theory (HoTT) is a kind of dependent type theory that can serve as both the theoretical basis for proof assistants and foundations of mathematics. It interprets types as spaces, terms as its points, and identity types as homotopy equivalences so that it can reason about cells on spaces. However, its dual concept, namely a set of differential forms on spaces cannot be a model of HoTT.

  In this study, we modify the fragment of HoTT that only contains identity types to obtain a type theory Nullhomologous Type Theory (NullTT), which interprets identity types not as homotopy equivalences but as homologousness. This enables the (co)chain complex of space to be a model of NullTT so that NullTT can reason not only about cells but also about differential forms. We also discuss the possibility for NullTT to be a formal system to reason about BRST quantization, which is a field of theoretical physics.

  Homotopy type theory (HoTT)は依存型理論の一種であり、定理証明支援系の理論的基盤や数学全体の形式化などに用いられている。HoTTでは型が空間に、項がその点に、そして等号型がホモトピー同値に解釈され、空間上のcellについて推論することができる。しかし、その双対概念である空間上の微分形式はHoTTのモデルとなることができない。

  そこで本研究ではHoTTの等号型のみを含む部分体系を改変して等号型をホモトピーではなくホモロジーにより解釈できる型理論 Nullhomologous Type Theory (NullTT) を定義する。これにより空間の(余)鎖複体がモデルとなるので、NullTTは空間上のcellだけでなく微分形式についても推論できる。NullTTが理論物理学の一分野であるBRST量子化について推論できる可能性についても論じる。

10:45 ～ 11:15 

佐藤隆

演題：Algebraic Theorems Equivalent to Induction（帰納法と同値な代数の定理）

梗概：

[FriSimSmi]は可算な代数を二階算術の部分体系で展開し，いろいろな定理がいくつかの集合存在公理とそれぞれ同値になることを示した．[Sim]はこのような逆数学現象を，代数に限らず，まとめている．

[SimSmi]と[Hat]は，基本体系とされるRCA_0で証明できてしまう定理について，それらがRCA_0を特徴付けるΣ^0_1帰納法と同値であることを，より弱い体系RCA_0^*の上で示した．それぞれ，任意の体上の多項式の既約分解と，有限生成アーベル群の基本定理（と関連する基底についての命題）が調べられている．

これらを踏まえ，本講演では，イデアル論の基本定理（任意の代数体における素イデアル分解）と，ガロアの基本定理（ガロア対応）について得られた結果を発表する．それぞれの定理を階層的に公理図式化し，RCA_0^*上でΣ^0_1帰納法と同値になる主張のみならず，適当な基本体系上でΣ^0_n帰納法と同値になる主張を提示する．この手法で先行研究の結果も拡張できる．

[FriSimSmi] Friedman, H., Simpson, S., and Smith, R., Countable algebra and set existence axioms, Annals of Pure and Applied Logic 25 (1983), 141-181.

[SimSmi] Factorization of polynomials and \Sigma^0_1 induction, Annals of Pure and Applied Logic volume 31 (1986), 289-306.

[Hat] Hatzikiriakou, K., Algebraic disguises of \Sigma^0_1 induction, Archive for Mathematical Logic volume 29 (1989), 47-51.

[Sim] Simpson, S., Subsystems of Second Order Arithmetic (Second Edition), 2010.

11:30 ～ 12:00 

河野友亮（フェリス女学院大学）

演題：命題記号を様相記号に持つ論理について

梗概：

動的論理や動的認識論理は、プログラムの実行や、情報を得たことによる状態や知識の変化を扱う論理である。そこで扱われる論理式の一つとして、[A]Bのように様相記号の中に論理式そのものが入ったものがある。これは例えば動的論理では「Aが真かどうかをテストし、真だったならばB」といった意味で用いられ、モデルにおける様相関係もこの意味を表現するような関係で定義される。しかしながら、論理式を様相関係に持つ概念としては、このように特定の用法、定義で用いられてるものはあるが、一般の論理として、そのようなものを扱った文脈はあまり存在していないように思われる。本発表では、この基本的な部分を提案し、モデルや演繹体系などを構成および分析する。

↓↓接続トラブルにより，午後の講演順，時間が変更されました↓↓

13:15 ～ 13:45 

GAINA Daniel（Kyushu University）

演題：Forcing and Calculi for Hybrid Logics

梗概：

 The definition of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the concept of stratified institution provides an abstract approach to Kripke semantics. This includes hybrid logics, a type of modal logics expressive enough to allow references to the nodes/states/worlds of the models regarded as relational structures, or multi-graphs. Applications of hybrid logics involve many areas of research, such as computational linguistics, transition systems, knowledge representation, artificial intelligence, biomedical informatics, semantic networks, and ontologies. The present contribution sets a unified foundation for developing formal verification methodologies to reason about Kripke structures by defining proof calculi for a multitude of hybrid logics in the framework of stratified institutions. To prove completeness, the article introduces a forcing technique for stratified institutions with nominal and frame extraction and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the significance of the general results is exhibited on a couple of benchmark examples of hybrid logical systems.

[1] Daniel Găină, Forcing and Calculi for Hybrid Logics, Journal of the ACM, vol. 67, issue 4, pp. 1-55, 2020 

14:00 ～ 14:30 

北澤 直樹（九州大学）

演題：高次元連結閉多様体のホモロジー群コホモロジー環他 幾何的情報の低次元空間への良い可微分写像の具体的構成を介した理解

梗概：

幾何学数学全般で重要な空間である(可微分)多様体のホモロジーコホモロジーのような代数的な量は重要な不変量である。これらの不変量などを、多様体の上の自身より次元の低く扱いやすい可微分写像や、自然に写像の逆像の連結成分を点とみなして得られる値域と次元の等しい多面体(Reeb 空間)といった幾何的な対象の構成を通じて、代数的な計算や一般的な考察等も大事にしながら理解しようという試みを紹介する。前世紀半ばには確立されていて、例えば自由度が高くて分類しやすい高次元の単連結閉多様体の分類などでも活躍し、現在に至るまであらゆる幾何学数学で基本的で強力な手法であり続ける Morse 関数の理論、その高次元版である折り目写像の特異点や特異点の集合やその像や逆像に着目して多様体の位相や可微分構造を観調べる話を基礎に、講演者なりに進めている研究の紹介である。

14:45 ～ 15:15 

上村 太一（University of Amsterdam）

演題：The Universal Exponentiable Arrow

梗概：

We show that the opposite of the category of finite generalized algebraic theories and interpretations between them is the finitely complete category freely generated by an exponentiable arrow.

15:15 ～ 15:30 

クロージング＋連絡など

参加予定者(氏名・所属。申込順・敬称略)