プログラム

最終更新日時: Last modified: 2021-09-10

2021年開催予定の第三十二回ALGIのプログラムです。

※プログラムは暫定のものです。講演数や講演時間，講演される方のご希望などにより変更される可能性があります。

10:00 ～ 10:15

オープニング＋連絡など

10:15 ～ 10:45

西澤弘毅（神奈川大学）

演題：Stone dualities from opfibrations

梗概：ストーン双対性は、ある代数たちの圏とある位相空間たちの圏の間の反変圏同値であり、その本質的な情報は双対随伴の中にある。本研究では、位相に関する議論なしでこの双対随伴を得ることを目的とし、代数と付加的なパラメータを基に、形式空間という抽象的な位相空間を構成する方法を示す。通常の位相空間はその例になる。

11:00 ～ 11:30

西原秀明（産業技術総合研究所）

演題：攻撃木の妥当性と infomorphism による抽象化関係の表現

梗概：攻撃木分析(Attack Tree Analysis)はセキュリティ分析における主要なツールであり，攻撃可能性や必要とする資源の見積もりといった定量的分析に用いられている．しかしつくられる木構造の妥当性はレビューに依存しており，正しく攻撃をモデル化できているか確認する手法がない．そこで攻撃の影響を論理式として記述し，その抽象化詳細化関係を使って攻撃木の妥当性を定義した(safecomp 2020)．これについて，影響と抽象化詳細化関係を classification と infomorphism で形式化する試みを進めており，本発表ではその経過について述べる．

12:30 ～ 13:00

冨田悠（京都大学）

演題：Categorical realizability for non-symmetric monoidal closed categories

梗概：In categorical realizability, it is common to construct categories of assemblies from applicative structures. Well known are the cases of partial combinatory algebras (PCAs) and BCI-algebras, which induce Cartesian closed categories and symmetric monoidal closed categories. For a non-symmetric case, in our previous study, we introduced BI-bullet-algebras inducing (non-symmetric) closed multicategories. However, applicative structures realizing non-symmetric tensor products were not known.

In this talk, we introduce a new class of applicative structures called bi-BDI-algebras. Bi-BDI-algebras are generalizations of PCAs and BCI-algebras, and feature two sorts of applications (left and right applications). Applying the categorical realizability construction to bi-BDI-algebras, we obtain non-symmetric monoidal closed categories of assemblies.

13:15 ～ 13:45

Daniel GAINA（Institute of Mathematics for Industry, Kyushu University）

演題：Stability of termination and sufficient-completeness under pushouts via amalgamation

梗概：In the present study, we provide conditions for the existence of pushouts of signature morphisms in constructor-based order-sorted algebra, and then we prove that reducibility and termination of term rewriting systems are closed under pushouts. Under the termination assumption, reducibility is equivalent to sufficient-completeness, which is crucial for proving several important properties in computing for constructor-based logics such as completeness, existence of initial models and interpolation. In logic frameworks that are not based on constructors, sufficient-completeness is essential to establish the soundness of the induction schemes which are based on some methodological constructor operators. We discuss the application of our results to the instantiation of parameterized specifications.

Reference

[1] Daniel Gaina, Masaki Nakamura, Kazuhiro Ogata and Kokichi Futatsugi, Stability of termination and sufficient-completeness under pushouts via amalgamation , Theoretical Computer Science, vol. 848, pp. 82-105, 2020.

14:00 ～ 15:00

新屋良磨（秋田大学）

演題：代数・論理・言語の対応：星無し言語を中心に

梗概：星無し言語(star-free language)は特殊な正規表現で記述できる言語であり，「一階述語論理で定義可能」や「統語モノイドが非周期的」などの論理・代数的な特徴付けを持つ性質のよい正規言語の部分体系である．本講演では前半で星無し言語の基本的な定理を紹介し，後半で最近の研究の動向や講演者自身の研究の紹介を行う．

10:00 ～ 10:30

前原悠究（九州大学）

演題：Equivalence of cubical and simplicial approaches to weak ω-categories

梗概：In higher-dimensional category theory, one often has to consider category-like structures in which the usual axioms hold only up to something weaker than equality (e.g. bicategories). When dealing with such weak structures (and weak maps between them), it can be more practical to leave the globular world and take an approach based on a different kind of combinatorics (e.g. simplicial, multi-simplicial, cubical, cellular, etc.) depending on the task at hand. It is then crucial to prove that different combinatorics still yield equivalent approaches in a suitable sense. In this talk, I will discuss such an equivalence between cubical and simplicial approaches to weak ω-categories. This talk is based on joint work with Tim Campion, Brandon Doherty, and Chris Kapulkin.

10:45 ～ 11:45

今村拓万（京都大学数理解析研究所）

演題：p-距離空間とデータフローシステム

梗概：Kahnネットワークは有限個の決定的プロセスからなるデータフローシステムである．各計算段階において，プロセスは，現在の自分自身または他のプロセスの出力をもとに，有限文字列を出力する．この計算を繰り返した極限において，プロセスは有限または無限文字列を出力する．有限文字列を不完全データと考えることにすると，全てのプロセスが完全なデータを出力するか，というロックフリー性の問題が現れる．Wadgeは巡回和テストと呼ばれる十分性条件を提案した．Matthewsは距離の一般化であるp-距離の概念を導入し，巡回和テストの正当性を0-完備p-距離空間の縮小写像原理に帰着することで証明した．本講演の前半では，p-距離空間の概念と，それに基づく巡回和テストの正当性証明を紹介する．後半では，p-距離の「非対称性」から出てくる，幾つかの（解決済み／未解決）問題を紹介する．

12:45 ～ 13:15

竹内泉（産業技術総合研究所）

演題：数学と変数　─自由変数と束縛変数─

梗概：数学に於ける自由変数と束縛変数の使用について、言語学的分析を行なう。

13:30 ～ 14:00

中村誠希（東京工業大学）

演題：ポジティブ関係計算の formula-size game について

梗概：ポジティブ関係計算は３変数ポジティブ存在論理と二項関係の表現力に関して等価である一方、表現の簡潔さに関しては指数的な差が生じる。本講演では、ポジティブ関係計算の formula-size game を導入する方法により、３変数ポジティブ存在論理がポジティブ関係計算と比較して指数的に簡潔であることを示す。

14:00 ～ 14:15

クロージング＋連絡など