プログラム (ALGI 2016)

最終更新日時: Last modified: 2016-08-31

13:45 ～ 14:00

オープニング＋連絡など

14:00 ～ 15:00

田中 康平（信州大学 経法学部）

演題：オイラー標数とその応用

梗概：

空間のホモトピー不変量として知られるオイラー標数の応用として，センサーネットワークにおける数え上げ問題に焦点を当てる。また，前半にオイラー標数を含めた代数トポロジーの基本的な事柄を振り返る。

15:00 ～ 15:15 休憩

15:15 ～ 15:45

片岡 俊基（東京大学 情報理工学系研究科）

演題：Categories of Filters as Fibered Completions

梗概：

良く知られているように semilattice L のフィルター全体は poset をなし， L の完備化となる。 これの類似として，圏 C の対象の上の（抽象）フィルターを対象とする圏が C の適切な意味での完備化となることが Butz により示された。 また， Butz はこの完備化に対応する filter logic を提案した。

フィルターの圏の定義は具体フィルター圏，抽象フィルター圏の2通り提案されていた。 具体フィルター圏からの忘却関手はファイブレーションとなり，これをフィルターファイブレーションとよぼう。 まず， C 上のフィルターファイブレーションが， C の部分対象ファイブレーションの適切な意味での完備化となることを見る。 この事実と Butz による結果を比較すると，圏論的論理からは次のように説明される： 圏 C の内部論理を拡張した filter logic の自由な圏モデルが抽象フィルターの圏であるのに対し，自由なファイブレーションモデルはフィルターファイブレーションとなる。

次に，一階述語論理の (left exact または regular または coherent) フラグメントの圏モデル全体と，良いファイブレーションモデル全体の間に adjoint triple があることを示す。 ファイブレーションモデルから圏モデルの非自明な構成として圏の局所化が用いられる。とくに，抽象フィルター圏は具体フィルター圏の局所化である。 このことにより， Butz の意味での完備化を表す随伴が，ファイブレーションの完備化を表す随伴を経由することが分かる。

15:45 ～ 16:15

向井 国昭（慶應義塾大学 名誉教授）

演題：Channel理論の分類圏としての再考察

梗概：

Barwise/Seligmanの情報の流れの理論ーChannel理論ーは, 圏論のことばを使うとむしろ分かりやすい. 分類と情報射全体のなす分類圏は, 位相空間と連続写像全体のなす位相 圏の自然な一般化である. 分類圏がトポスをなすことにも注意する. colimit/limitも存在する．Channel理論に組み込まれているregular theory (identity, weakening, global cut)のおかげで, 与えられた制約を満たす普遍分類が存在する. これらの簡明な性質はロジックプログラミング, データベース, マルチメディア, 選好理論などさまざま な分野の意味論に統合的な視点をもたらす. 以上の観察と考察に並行して開発してきた計算実験用Prologライブラリを, チャネル理論の教育と普及のため公開する.

16:15 ～ 16:30 休憩

16:30 ～ 17:00

吉田 聡 (公立鳥取環境大学)

演題：様相論理S4に基づくプロトコル検証

梗概：

BAN論理とSPINを用いた先行のプロトコル検証に対して、あらためて様相論理S4に基づいて行った検証を紹介する。また、2つの検証のプロセスを比較し、より効率的に検証を実施するための改善案について議論する。

17:00 ～ 17:30

上村 太一（京都大学 数理解析研究所）

演題：Interpreting type theory in a higher category

梗概：

Martin-Lof の *intentional* type theory は locally cartesian closed (∞,1)-category の internal language であると期待されているが, 今のところ type theory の (∞,1)-category での解釈は確立していない. 一方, Martin-Lof の *extensional* type theory は Seely によって locally cartesian closed category と対応することが分かっている. 本講演では, Seely の方法を拡張して locally cartesian closed (∞,1)-category での intentional type theory の解釈を与える.

18:30 ～

懇親会（松本駅周辺を予定） 懇親会への参加を希望される方は、8/20（土）までに西澤 (nishizawa AT kanagawa-u.ac.jp) に メールでお知らせください。

10:00 ～ 10:45

西村 進（京都大学 大学院理学研究科）

演題：分散プロトコル合成のための半順序位相

梗概：

単体的複体を用い、分散計算システムの抽象化と特徴付けを行う位相幾何的手 法が1990年代から研究されてきている。この位相幾何的手法に基づいて、与え られた分散システムの仕様から自動的に分散プロトコルを導出する手法を提案 する。この問題は決定不能問題であることが知られているが、不完全ではあっ ても健全なアルゴリズムであって、典型的な分散プロトコルに関しては導出が 可能なようなものを与えることを目標とする。 提案する手法は、与えられた仕様から組合わせ的な操作によってcanonicalな 半順序位相を構築し、この位相上で単体的複体の変形によってプロトコルを発見 するものである。本発表では、この手法の正当性に関する位相幾何的議論を行 い、さらに現実的な計算時間でプロトコルを発見するためのhyperforestを用い たアルゴリズムを提案する。

10:45 ～ 11:15

古澤 仁（鹿児島大学 大学院理工学研究科（理学系））

演題：一様連続関係とセルオートマトン

梗概：

関係の一様連続性を定義し，連続性との関連について述べる． また，一様連続性を用いて群上の非決定的セルオートマトンの大域的な特徴づけをおこなう．

11:15 ～ 11:30 休憩

11:30 ～ 12:30 特別講演

玉木 大（信州大学 理学部）

演題：An introduction to directed homotopy theory

梗概：

It often happens that we need to deform our object of study continuously in many areas of science. The notion of homotopy was introduced in mathematics to describe continuous deformations. In theoretical computer science, the notion of homotopy has been used in the study of concurrency since the discovery of Gunawardena. However, deformations used in the theory of concurrency is slightly different, in the sense that the process of deformation cannot be reversed. Processes in concurrency do not have time-reversal symmetry. Homotopy should be one-directed. Similar situations also appear in pure mathematics. For example, spaces with singular points have canonical stratifications, for which Woolf and MacPherson proposed to use directed homotopy. In this talk, we review basic ideas in directed homotopy theory, together with some recent topics.

12:30 ～ 12:45

クロージング＋連絡など