CSCAT 2024

理論計算機科学と圏論ワークショップ

Computer Science and Category Theory

日時：2024年3月14日（木）～15日（金）

Date: 14 (Thu) - 15 (Fri)  March 2024

千葉大学（西千葉キャンパス）で対面開催

千葉大学 西千葉キャンパス（最寄り：JR 西千葉駅）
理学部４号館１階 マルチメディア１教室

幹事：塚田武志（千葉大学）tsukada _at_ math.s.chiba-u.ac.jp

cscat-map.pdf

CSCATとは

CSCAT（理論計算機科学と圏論ワークショップ）は、数学の分野である圏論の情報科学への応用に関心を持つ研究者による研究集会です。通常の学会では、時間の制約などのため研究の詳細にまで立ち入った発表と議論はなかなかむずかしいのが実情です。本研究集会は、１つ１つの発表に長い時間を割り当て、じっくりと話を聞き議論する場を提供することを目的としています。 

参加登録・発表申し込み（3月7日締切）

未登録でも参加いただけます

発表申し込みはこちらから

参加登録（発表なし）はこちらから

懇親会（3月10日締切）

3/14 18:00 から 世炉思食 （西千葉駅すぐ）で行います。「ツカダ」で予約してあります

3/14 のワークショップ終了後に、西千葉駅近郊あるいは千葉駅近郊で懇親会を行います
参加希望者は 3/10 までにこちらからお申し込みください

プログラム（暫定）

[日付と曜日があっていなかったので直しました。日付が正しく、曜日が誤っていました。2024/3/11]

3/14 (木)

13:00--13:45 河瀬悠人（京都大学） Formal accessibility in a virtual equipment 

13:45--14:30 奈須隼大（京都大学 RIMS） (Hyper)doctrines as virtual double categories 

BREAK

15:00--15:30 谷口雅弥 （理化学研究所） Operad for Lambek Calculus

15:30--16:00 中村誠希 （東京工業大学） On Existential Calculi of Relations with Transitive Closure

16:00--16:30 Lechenne Serge （National Institute of informatics） Braids, twists, trace and duality in combinatory algebras 

3/15 (金)

10:30--11:15 今村悠希（大阪大学） Category theory for the homotopy theory of dg categories 

11:15--12:00 池渕未来 （京都大学） 代数理論のQuillenホモロジーの具体計算

LUNCH BREAK

13:30--14:15 荒武永史（京都大学数理解析研究所） Axiomatizability of Models Represented by Sheaves

14:15--15:00 伊藤耀 （東北大学情報科学研究科）  Coh，ScottL，Σ加群の圏と有限モデル

BERAK

15:30--15:45 Clovis Eberhart （国立情報学研究所） A Compositional Approach to Petri Nets

15:45--16:30 洞龍弥 （東京大学大学院数理科学研究科） Combinatorial games as recursive coalgebras

講演題目および要旨（申込順）

荒武永史（京都大学数理解析研究所） Axiomatizability of Models Represented by Sheaves

In the theory of sheaf representation of rings, it is well-known that von Neumann regular rings (resp. domain representable rings) are precisely the rings of global sections of sheaves whose stalks are fields (resp. integral domains). More generally, the classes of models represented by some kinds of sheaves have been considered in the context of universal algebra and model theory. However, the existing studies do not seem to answer to the question of why global section models in the above examples can be characterized elementally. In this talk, we present a sufficient condition for first-order axiomatizability of the class of models represented by sheaves whose stalks are T-models for a given first-order theory T. We exploit Coste's theory of categorical spectra and the previous studies on subcategories of locally finitely presentable categories. 

奈須隼大（京都大学 RIMS） (Hyper)doctrines as virtual double categories 

The applications of (virtual) double categories have been expanding in recent times. We propose a method to view hyperdoctrines as virtual double categories, which opens up the possibility of “double categorical logic”. We will see that some known classes of hyperdoctrines can be translated into properties of possessing certain colimits as virtual double categories. We will start this talk by introducing double categories of relations as motivational examples. Then, we will delve into general results including the equivalence of elementary existential fibrations with additional Beck-Chevalley conditions and Frobenius cartesian equipments.  (This talk is partly based on joint work with Keisuke Hoshino (RIMS)) 

今村悠希（大阪大学） Category theory for the homotopy theory of dg categories 

dg圏とは、加群の複体の圏Chで豊穣された豊穣圏である。dg圏には擬同値と呼ばれる、圏同値よりも弱い同値概念があり、すべてのdg圏は擬同値のもとで区別するべきとされる。擬同値に関するdg圏のホモトピー論は、dg圏の圏dgCat上の擬同値を弱同値とするモデル圏構造によって実現される。すなわちモデル圏構造を用いることで擬同値に関するdgCatの局所化hodgCatが構成できる。局所化hodgCatは擬同値なdg圏を同型にするものの中で最も普遍的な1圏である。
一方、dg圏の圏dgCatは2圏の構造も備えており、圏論が展開できる。しかしこれはdg圏のホモトピー論を考慮できておらず、擬同値のレベルでdg圏を区別するべきという観点から適切とはいえない。
本講演では、hodgCatの上にあるような2圏(双圏)を導入し、擬同値を考慮したdg圏の"ホモトピー"圏論を、形式的に圏論を展開する枠組みの一つであるproarrow equipmentの観点から考察する。 

河瀬悠人（京都大学） Formal accessibility in a virtual equipment 

We develop a formal theory of accessible and locally presentable categories in a virtual equipment. Our ultimate goal is to recapture Gabriel–Ulmer duality in the double categorical setting. As a preliminary step to that, in this talk, I will explain how several fundamental concepts should be formalized in a virtual equipment, which includes weighted (co)limits, commutation of weights, ind-completions, and Cauchy completions. This talk is based on a joint work with Keisuke Hoshino. 

Lechenne Serge （National Institute of informatics） Braids, twists, trace and duality in combinatory algebras 

Recently, Hasegawa investigated a class of combinatory algebras, called ribbon combinatory algebra, in which one can interpret both the braided untyped lambda calculus and framed oriented tangles. Such combinatory algebras can be obtained categorically, as any reflexive object in a ribbon category gives rise to such an algebra. Conversely, the ribbon category can be recovered from any combinatorial algebra, using the internal PROB construction developed by Hasegawa. Interestingly, certain algebras possess trace in the form of a combinator element Tr, and even duality in the form of a unit and counit. We therefore explore a systematic axiomatisation of thos categorical notion as combinator, in an extended class of algebra, called traaced combinatorial algebras, and explore the properties they have : mainly, they form both a sort of reciprocity the canonical trace construction in a ribbon category, and transcribe mathematically the graph interpretation of planar lambda terms introduced by  N. Zeidberger. 

Clovis Eberhart （国立情報学研究所） A Compositional Approach to Petri Nets

TBA

洞龍弥 （東京大学大学院数理科学研究科） Combinatorial games as recursive coalgebras

Combinatorial game theory is a field that analyzes games without probability, such as stone-taking games. A fundamental tool in combinatorial game theory is a binary operation on natural numbers known as the Nim-sum, which is performed by expanding numbers into binary form and then taking the bitwise exclusive OR of each digit.
In my talk, I suggest a categorical approach to addressing why this seemingly strange Nim-sum is so useful, considering combinatorial games as recursive coalgebras. 

池渕未来 （京都大学） 代数理論のQuillenホモロジーの具体計算

TBA

伊藤耀 （東北大学情報科学研究科）  Coh，ScottL，Σ加群の圏と有限モデル

線形論理の圏論的モデルはLNL随伴による余モナド構造により演算子！を解釈している．圏によっては複数の！の構造があり，Lafontモデル（多重集合など）や冪集合の有限モデルなど，それぞれ利点があるモデルとなる．2022年に塚田・浅田はΣ半環上の加群の圏が線形論理のモデルの一つであるLafontモデルを一般に構成できることを示した．この加群の圏はいくつかの係数環で有限モデルを構成できることが分かっている．本発表ではある条件を満たす係数環における線形論理の有限モデルの構成方法を紹介する．具体的には，はじめに正規直交基底をもつΣ半環I上の加群の圏OBMod_Iの有限モデルの構成方法を与える．そして，係数環Iから特定の係数環Rへの係数制限・拡大が正規直交基底を持つ加群の圏で閉じていることを示し，OBMod_Iの有限モデルのLNL随伴と係数制限・拡大との合成によりOBMod_Rの有限モデルを構成する．

谷口雅弥 （理化学研究所） Operad for Lambek Calculus

The Lambek calculus, a substructural logic, is commonly modelled algebraically using residuated monoids or semigroups based on biclosed monoidal categories. This presentation focuses on the weak commutative Lambek calculus, a variant of Lambek calculus with relaxed implication introduction rules.
Analysis of the corresponding algebraic models shows that this system requires weak commutativity. However, such conditions are not well suited for monoids. To address this problem, we propose an alternative algebraic model for the Lambek calculus using non-symmetric operads. Non-symmetric operads provide a more flexible framework that can naturally accommodate the property required by weak commutative Lambek calculus. By using this approach, we aim to gain a deeper understanding of the algebraic structures underlying substructural logics.
Through this work, we hope to contribute to the ongoing exploration of the connections between category theory, algebra and logic, and to provide new insights into the modelling and understanding of substructural logics such as Lambek calculus.

中村誠希 （東京工業大学） On Existential Calculi of Relations with Transitive Closure

This talk presents some (graph language, saturable path, and automaton) characterizations of the equational theories for fragments of the existential calculus of relations (ECoR) with transitive closure; ECoR is a restricted-negation fragment of Tarski's calculus of relations related to existential logic. These characterizations show the decidability/complexity of the theories. We then mention open problems and ongoing work. (The main part of this talk was presented at LICS 2023.) 

過去の CSCAT