CSCAT 2022

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

Computer Science and Category Theory

日時：2022年3月9日（水）〜10日（木）

Date: 9 (Wed) -- 10 (Thu) March 2022

オンライン(zoom)での開催です．
幹事：浅田和之（東北大学，HP)

CSCAT 2022 will be held online (zoom).

Organizer: Kazuyuki Asada (Tohoku University)

Email address can be found at the end of my HP

CSCATとは

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

参加登録（3月7日締切）

こちらから参加登録をお願いします．

ZoomのURLなどの情報は参加登録された方およびCSCATのメーリングリストに送信します．

参加登録が間に合わなかった方でも，CSCATのメーリングリストに登録されている方は参加可能です（が参加登録をしていただけると人数把握のため助かります）．

Click here to register. Then you will receive a URL of the Zoom meeting.

発表申込（3月7日締切，空きがあれば締切後も受付）

発表をご希望の方はこちらから申込をお願いします．

発表を申し込まれた方は参加登録は不要です．

Click here if you apply for your presentation.

Program

3/9

12:50 - 13:00 オープニング
13:00 - 13:40 中田哲 直観主義算術に対するトポス理論的次数構造について
13:40 - 14:20 内藏理史 A General Semantic Construction of Dependent Refinement Type Systems, Categorically

休憩（gather）

14:40 - 15:20 吉田智哉 Continuous functions on final comodels of free algebraic theories
15:20 - 16:00 Cédric HO THANH Recurrence theorems for topological Markov chains

休憩（gather）

16:20 - 17:00 荒武永史 Limits, Colimits, and Spectra of Modelled Spaces

3/10

13:00 - 13:40 浅田和之 A Compositional Approach to Parity Games
13:40 - 14:20 塚田武志 Module Models of Linear Logic

休憩（gather）

14:40 - 15:20 藤井宗一郎 Quantaloidal approach to constraint satisfaction
15:20 - 16:00 長谷川真人 The internal operads of combinatory algebras

休憩（gather）

16:20 - 17:00 星野恵佑 PCAs as algebras over operads
17:00 - 17:10 クロージング

Title and abstract

  • 中田哲（京都大学理学研究科）
    Title: 直観主義算術に対するトポス理論的次数構造について
    Abstract: (初等)トポスには直観主義数学のモデルとしての側面があることはよく知られている．この観点に立つと，部分トポスを取る操作は新たな数学的モデルを得る事に相当するが，その情報はLawvere-Tierney位相(LT位相)の概念を用いて調べることができる．更に，具体例として実効トポス(effective topos)におけるLT位相を見ると，実現可能性解釈の技法や計算論的次数構造との繋がりが知られていた．
    本講演では直観主義一階算術研究で重要な公理達に対して，トポス理論における議論を用いて新たに次数構造を定義する．そして，その次数構造とすでに知られている計算論的次数構造との対応などを考察する．

  • 内藏理史（NII）
    Title: A General Semantic Construction of Dependent Refinement Type Systems, Categorically
    Abstract:     Dependent refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. In this talk, we propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of fibred adjunction models from given (underlying) fibred adjunction models and posetal fibrations for predicate logic. We also consider interpreting recursion in dependent refinement type systems by generalizing Conway operators.

  • 吉田智哉（京都大学）
    Title: Continuous functions on final comodels of free algebraic theories
    Abstract: In a recent work, Garner gave a coalgebraic characterization of continuous functions between sets of infinite sequences; continuous functions are given by states of the final residual comodel and the set of continuous functions is the final bimodel. We apply his technique to the case of infinite trees but, in this case, the final residual comodel does not give all of the continuous functions. To capture functions given by the final residual comodel, we define the notion of continuous functions on sub-basis. Then these functions also constitute the final bimodel.

  • Cédric HO THANH（NII）
    Title: Recurrence theorems for topological Markov chains
    Abstract: Recurrence theorems place conditions under which probabilistic systems, specifically Markov chains, are expected to visit certain states infinitely often. For example, a printer with its many moving parts and the random requests it receives, may be described as a probabilistic system, and recurrence of the ""ready to print"" state is desirable. Recurrence theorems in the case of finite Markov chains are widely known.
    In this talk, we are interested in generalization to the infinitary setting. As it turns out, some care has to be put in the definition of infinite Markov chains. Rather than simply infinite, the introduct topological Markov chains, and show how standard constructions can be naturally extended to this framework: path spaces, cylinder sets, as well as the semantic of LTL and PCTL. With all these tools in hand, we finally state our recurrence theorems.

  • 荒武永史（京都大学数理解析研究所）
    Title: Limits, Colimits, and Spectra of Modelled Spaces
    Abstract: It is well-known that the construction of Zariski spectra of (commutative) rings yields a dual adjunction between the category of rings and the category of locally ringed spaces. There are many constructions of spectra of algebras in various contexts giving such adjunctions. Michel Coste unified them in the language of categorical logic by showing that, for an appropriate triple (T,T’,A), each T-model can be associated with a T’-modelled space and that this yields a dual adjunction between the category of T-models and the category of T’-modelled spaces and “A-morphisms”. In this talk, using Coste’s framework, we show the existence of limits and colimits in the categories of modelled spaces. To obtain limits of T’-modelled spaces, we also construct relative spectra of T-modelled spaces. As a corollary, we can show that the category of ringed spaces whose stalks are fields is complete and cocomplete. If time permits, we overview the construction of spectra, which exploits the theory of locally finitely presentable categories.

  • 浅田和之（東北大学電気通信研究所）
    Title: A Compositional Approach to Parity Games
    Abstract: In this talk, we introduce open parity games, which is a compositional approach to parity games. This is achieved by adding open ends to the usual notion of parity games. We introduce the category of open parity games, which is defined using standard definitions for graph games. We also define a graphical language for open parity games as a prop, which have recently been used in many applications as graphical languages. We introduce a suitable semantic category inspired by the work by Grellois and Melliès on the semantics of higher-order model checking. Computing the set of winning positions in open parity games yields a functor to the semantic category. Finally, by interpreting the graphical language in the semantic category, we show that this computation can be carried out compositionally. On-going work is also mentioned.
    (    Joint work with Kazuki Watanabe, Clovis Eberhart, and Ichiro Hasuo (all from NII), presented at MFPS 2021.)

  • 塚田武志（千葉大学）
    Title: Module Models of Linear Logic
    Abstract: This talk presents a general construction of models of linear logic based on modules over ring-like structures with partially-defined countable sums. Examples include models based on coherence spaces, finiteness spaces and probabilistic coherence spaces, as well as the relational and weighted relational models. In contrast to the classical presentation of above mentioned models, which explicitly uses bases to defined spaces, our approach is completely algebraic: a module is an additive algebra with action of a ring-like structure and a homomorphism is a function that preserves addition and action. An advantage of our algebraic treatment is that the category of modules (over a fixed ring-like structure) is locally presentable, from which it easily follows that this category becomes a model of intuitionistic linear logic with the cofree exponential. We then discuss constructions of classical models and show that the above-mentioned models are examples of our constructions.

  • 藤井宗一郎（京都大学数理解析研究所）
    Title: Quantaloidal approach to constraint satisfaction
    Abstract: The constraint satisfaction problem (CSP) is a computational problem that includes a range of important problems in computer science. We point out that fundamental concepts of the CSP, such as the solution set of an instance and polymorphisms, can be formulated abstractly inside the 2-category PFinSet of finite sets and sets of functions between them. The 2-category PFinSet is a quantaloid, and the formulation relies mainly on structure available in any quantaloid. This observation suggests a formal development of generalisations of the CSP and concomitant notions of polymorphism in a large class of quantaloids. We extract a class of optimisation problems as a special case, and show that their computational complexity can be classified by the associated notion of polymorphism.
    (Joint work with Yuni Iwamasa and Kei Kimura, presented at Applied Category Theory 2021.)

  • 長谷川真人（京都大学数理解析研究所）
    Title:     The internal operads of combinatory algebras
    Abstract: In the study of combinatory algebras and their applications, the notion of polynomials and combinatory completeness play the fundamental role. However, in our previous work on the braided lambda calculus, we observed that the traditional formulation of polynomials as functions does not work for braided combinatory algebras. To remedy this, we introduce internally-defined operads of combiatory algebras, which serve as an alternative way of handling polynomials and combinatory completeness. We show that the internal operad construction works well for planar, linear as well as braided combinatory algebras. As a by-product, we derive semantically-motivated axiomatizations of extensional combinatory algebras.

  • 星野恵佑（京都大学）
    Title: PCAs as algebras over operads
    Abstract: We observe that a PCA can be seen as an algebra over an operad whose value is taken in Rel. On the other hand, we extend the definition of morphism of right modules, which is another special class of algebras over operads, to non-functorial version, and obtain a 2-category of algebras over operads and their non-functorial morphisms. We show that the 2-category of PCAs, defined in the Longley's PhD thesis, is embedded to this 2-category and that the category of assemblies can be defined as a Grothendieck construction.


過去の CSCAT