CSCAT 2023
理論計算機科学と圏論ワークショップ
Computer Science and Category Theory
日時：2023年3月9日（木）〜10日（金）
Date: Thu 9 -- Fri 10 March 2023
京都大学での対面開催
幹事：室屋晃子（京都大学数理解析研究所）
会場：京都大学吉田キャンパス 総合研究2号館 478号室（構内マップの34番の建物です）
CSCAT 2023 will be held offline. It may go online (zoom), depending on the COVID-19 situation.
Venue: Room 478, Research Bldg. 2, Kyoto University
Organizer: Koko Muroya (RIMS, Kyoto University)
Email: kmuroya[at]kurims.kyoto-u.ac.jp
CSCATとは
CSCAT（理論計算機科学と圏論ワークショップ）は、数学の分野である圏論の情報科学への応用に関心を持つ研究者による研究集会です。通常の学会では、時間の制約などのため研究の詳細にまで立ち入った発表と議論はなかなかむずかしいのが実情です。本研究集会は、１つ１つの発表に長い時間を割り当て、じっくりと話を聞き議論する場を提供することを目的としています。
参加登録・発表申込（3月1日締切）
発表申込はこちらから
Registration for speakers
参加登録（発表なし）はこちらから
Registration for non-speakers
Program)
Thu 9 March (PM)
12:50 - 13:00 Opening
13:00 - 13:40 内藏 理史 Satoshi KURA Higher-Order Weakest Precondition Transformers via a CPS Transformation
13:40 - 14:20 前原 悠究 Yuki MAEHARA Coinductive equivalences in algebraic weak ω-categories
14:20 - 14:40 Coffee break
14:40 - 15:20 河瀬 悠人 Yuto KAWASE Finitary Monads on LFP Categories and Birkhoff's Variety Theorem
15:20 - 16:00 JS Lemay Classical Distributive Restriciton Categories
16:00 - 16:20 Coffee break
16:20 - 17:00 Free discussion
Fri 10 March (AM, PM)
10:30 - 11:10 Masahiro HAMANO Double Glueing over Free Exponential: with Measure Theoretic Applications
11:10 - 11:50 洞 龍弥 Ryuya HORA Internal parameterization of Hyperconnected quotients
11:50 - 13:30 Lunch break
13:30 - 14:10 星野 恵佑 Keisuke HOSHINO Towards Structres of Higher Dimensional Cagegorical Structures
14:10 - 14:50 眞田 嵩大 Takahiro SANADA ファイブレーションを用いた分割細分アルゴリズムとHopcroftの最適化の構造
14:50 - 15:00 Closing
Title and abstract
内藏 理史 Satoshi KURA (National Institute of Informatics) Higher-Order Weakest Precondition Transformers via a CPS Transformation
Weakest precondition transformers are essential notions for program verification, and various extensions have been studied. However, only a few consider both higher-order languages and syntactic calculation of weakest precondition transformers. In this paper, we consider weakest precondition transformers for a higher-order functional language with computational effects and recursion and show that we can calculate them via a CPS transformation. We prove this in a general framework of categorical semantics. Because of this generality, two existing methods for program verification can be understood as instances of our result. Specifically, we show how to instantiate our result to (1) verification of trace properties by Kobayashi et al. and (2) expected cost analysis by Avanzini et al.
arxiv: https://arxiv.org/abs/2301.09997
前原 悠究 Yuki MAEHARA (九州大学) Coinductive equivalences in algebraic weak ω-categories
There are many different approaches to weak higher-dimensional categories. One proposed by Leinster, based on an idea of Batanin’s, defines weak ω-categories as the algebras for a particular monad on the category of globular sets. Intuitively, this monad encodes only the existence part of the pasting theorem for globular pasting diagrams. In this talk, I will make precise (and sketch a proof of) the uniqueness part, and discuss some of its applications. This talk is based on joint work with Soichiro Fujii (Macquarie University) and Keisuke Hoshino (Kyoto University).河瀬 悠人 Yuto KAWASE (京都大学) Finitary Monads on LFP Categories and Birkhoff's Variety Theorem
An algebraic theory, sometimes called an equational theory, is a theory defined by finitary operations and equations, such as groups and rings. It is well known that algebraic theories are equivalent to finitary monads on Set. In this talk, we generalize this phenomenon to locally finitely presentable (LFP) categories from the perspective of partial Horn logic. For each LFP category A, we define an "algebraic concept" relative to A, which will be called an A-relative algebraic theory, and show that A-relative algebraic theories are equivalent to finitary monads on A. Finally, we generalize Birkhoff's variety theorem for classical algebraic theories to our relative algebraic theories.JS Lemay (Kyoto University) Classical Distributive Restriciton Categories
In the category of sets and partial functions, the Cartesian product $\times$ is not a categorical product. Instead the categorical product is given by $A + B + A \times B$, where $+$ is the disjoint union. In this talk, we give a restriction category explanation of why this is the case. We will show that in a distributive restriction category, $A + B + A \times B$ is a product if and only if the restriction category is classical, that is, has disjoint joins and complements. This is joint work with Robin Cockett.Masahiro HAMANO (National Cheng Kung University) Double Glueing over Free Exponential: with Measure Theoretic Applications
This talk presents a compact method to lift the free exponential construction of Mellies-Tabareau-Tasson over the Hyland-Schalk double glueing for orthogonality categories. A condition ”reciprocity of orthogonality” is presented simply enough to lift the free exponential over the double glueing in terms of the orthogonality. The method applies to the monoidal category TsK of the s-finite transition kernels with countable biproducts.
We show (i) TsK^op has the free exponential, which is shown to be describable in terms of measure theory. (ii) The s-finite transition kernels have an orthogonality between measures and measurable functions in terms of Lebesgue integrals. The orthogonality is reciprocal, hence the free exponential of (i) lifts to the tight orthogonality category T(TsK^op), which subsumes Ehrhard et al’s probabilistic coherent spaces as the full subcategory of countable measurable spaces.
To lift the free exponential, Lebesgue monotone convergence theorem plays a crucial role to guarantee Mellies-Tabareau-Tasson’s limit construction over symmetric monoidal equalisers. Our measure-theoretic orthogonality is considered as a continuous version of the orthogonality of the probabilistic coherent spaces for linear logic, and in particular provides a two layered decomposition of Crubille et al’s direct free exponential for the spaces.
洞 龍弥 Ryuya HORA (東京大学 大学院 数理科学研究科 修士1年) Internal parameterization of Hyperconnected quotients
Topos理論に関する私の研究(Internal parameterization of Hyperconnected quotients, arXiv:2302.06851, https://arxiv.org/abs/2302.06851 )について，
1. Lawvereの未解決問題への一歩であること
2.中心的役割を果たす概念 local state classifier が素朴で触っていて楽しいこと
の2点を中心に話します．
1. Topos理論において最も基本的な定理の一つは，Lawvere-Tierney topologyとsubtoposの一対一対応です．Lawvereはこの現象をsubtoposのinternal parametrizationと呼び，quotient topos (connected geometric morphism)にも同様のinternal parametrizationがないか問いました．これが彼の未解決問題集の1番です．私の論文は，その未解決問題の部分的解決で(も)あり，hyperconnected quotient (hyperconnected geometric morphism)のinternal parameterizationを与えています．
2. 論文の鍵となる概念，local state classifierは，"全てのモノ射の余極限"という素直すぎる方法で定義されます．この定義は，hyperconnected quotientに関する素朴な考察から示唆されるものです．発表の後半では，定義の背景にある直感を説明し，いくつかの例を挙げます．
星野 恵佑 Keisuke HOSHINO (RIMS) Towards Structres of Higher Dimensional Cagegorical Structures
Small categories forms a 2-category, but when profunctors are also taken into account, they form a double category Prof. In general, it is natural to assume that the collection of 1- dimensional structures such as categories forms a 2-dimensional structure in several senses. Furthermore, the collection of n-dimensional structures is expected to have an n + 1-dimensional structure. The main objective of this talk is to give an answer to this expectation.
In this talk, we use the theory on familial monads introduced by Shapiro, as a general framework for defining higher categories. In general, for a cartesian monad T, a generalised notion of category, called T- category in this talk, is defined, whereas in a paper by Shapiro, it is asserted that there exists another familial monad fc[T] whose algebras coincide with T-categories whenever T is familial. We obtain fc^n by repeating this process, and suggest that fc^n-categories (=:virtual n + 1-tuple categories) can be considered an example of concepts of (n + 1)-dimensional structure.
On the other hand, we investigate the virtual double category of T-categories and T-profunctors, Prof(T), in terms of pseudo simplicial category, i.e. pseudo functor from the category of simplices to 2-category of categories. We show that one can define a (2-truncated) pseudo simplicial category of T-categories and T-profunctors and Prof(T) is the free objects with respect to a “nerve” 2-functor from the 2-category of virtual double categories to the 2-category of pseudo simplicial categories, hence Prof(T) can be seen as the “realization” of the pseudo simplicial set as a virtual double category.
Combining those observations, we suggest an definition of the fc-pseudo simplicial category of virtual double categories, and the virtual triple category of virtual double categories as its realization. Moreover, we suggest a way to define the virtual n + 2-tuple category of virtual n + 1-tuple categories, in general.
眞田 嵩大 Takahiro SANADA (京都大学) ファイブレーションを用いた分割細分アルゴリズムとHopcroftの最適化の構造
決定性有限オートマトン(DFA)の双模倣性を計算する効率的なアルゴリズムとしてHopcroftの分割細分(partition refinement)アルゴリズムが知られている。DFAを余代数に拡張することにより、より広いクラスの状態遷移システムに対して双模倣性を計算するアルゴリズムの研究がなされてきた。
この講演ではファイブレーションを用いて余代数の上に余帰納的に定義された双模倣性を計算するアルゴリズムを提案する。ファイブレーションを用いることにより、アルゴリズムの正しさを証明するための条件が明確になる。また、計算量を評価するために重み付き木に関する不等式を導出して適用する。この不等式はこの種のアルゴリズムの計算量評価でなされてきた複雑な議論の本質を明らかにする。(joint work with Ryota Kojima, Yuichi Komorida, Koko Muroya, and Ichiro Hasuo)
過去の CSCAT
CSCAT 2020 (京都大学) COVID-19感染拡大のため中止
CSCAT 2011 (慶應義塾大学) 東日本大震災のため中止
CSCAT 2008 (東北大学)
CSCAT 2006 (広島大学)
CSCAT 2005 (筑波大学) メイリングリストを開設
CSCAT 2004 (産業技術総合研究所)
CSCAT 2003 (慶應義塾大学) 「理論計算機科学と圏論」の名を冠してワークショップ化