プログラム (ALGI 2011)

最終更新日時: Last modified: 2011-08-28

８月２３日（火）

13:15 〜 13:30

オープニング＋連絡など

13:30 〜 14:15

星野 直彦（京都大学数理解析研究所）

演題：

A characterisation of unique decomposition categories

梗概：

Geometry of Interaction (GoI) is a semantics of linear logic and cut elimination introduced by Girard. Among studies on categorical framework for GoI, Haghverdi gave a class of symmetric monodical categories called unique decomposition categories (UDC) so as to capture the execution formula in GoI categorically. The purpose of this talk is to give a categorical characterisation of UDC's in terms of subcategories of categories with countable biproducts. As an application of the characterisation, we give a categorical proof of a fundamental property of UDC's: if execution formulae of a given UDC make sense, then the UDC is traced.

14:15 〜 14:45 休憩

14:45 〜 15:30

宮部 賢志（京都大学数理解析研究所）

演題：

An optimal semimeasure and its convergence

梗概：

Solomonoffによって提案されたa priori probabilityは 確率1で正しい確率に収束する。 この「確率1」を「Martin-L\"ofランダムな列」で 置き換えられるかどうかは長年の未解決問題であったが、 最近、HutterとMuchnikにより否定的に解決された。 本講演ではその本質的な理由を探り、 より強いランダムネスの概念を使うことで、 肯定的な命題を与える。 このことは予測理論において「確率」の概念が 必要ではないことを示している。

15:30 〜 16:00

神志那 純，潮 俊光（大阪大学大学院基礎工学研究科）， 木下 佳樹（産業技術総合研究所）

演題：

部分観測Mealyオートマトンのスーパバイザ制御への余代数的アプローチ

梗概：

スーパバイザ制御はRamadgeとWonhamによって導入された離散事象システムの論 理的制御手法の１つである． 本発表では，不可観測事象を出力事象にもつMealyオートマトンのスーパバイザ 制御問題について考える． 余代数および余帰納的定義を用いてスーパバイザ制御問題を定式化する． 制御仕様を満たすスーパバイザと呼ばれる制御器が存在するための必要十分条件 を部分双模倣関係を用いて与え， スーパバイザが存在しない場合に最大部分言語を求めるアルゴリズムを提案する．

16:00 〜 16:30 休憩

16:30 〜 17:30

末永 幸平（京都大学情報学研究科 日本学術振興会特別研究員 (PD)）

演題：

Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling

梗概：

We add, to the common combination of a WHILE-language and a Hoare-style program logic, a constant dt that represents an infinitesimal (i.e. infinitely small) value. The outcome is a framework for modeling and verification of hybrid systems: hybrid systems exhibit both continuous and discrete dynamics and getting them right is a pressing challenge.We rigorously define the semantics of programs in the language of nonstandard analysis, on the basis of which the program logic is shown to be sound and relatively complete.

(Joint work with Ichiro Hasuo)

懇親会

８月２４日（水）

10:00 〜 10:45

西澤 弘毅（鳥取環境大学）

演題：

Relational Representation Theorem for Algebraic Quantales with respect to Completely Coprime Elements and Atoms

梗概：

We gives the sufficient condition of a quantale to be isomorphic to a sub-quantale of the quantale whose elements are binary relations on a set and whose order is given by inclusion and whose monoid structure is given by relational composition and the identity relation. A quantale has such relational representation, if it is completely coprime algebraic and the order of its completely coprime elements is discrete. We also show that the sufficient condition has other equivalent conditions.

(Joint work with Hitoshi Furusawa)

10:45 〜 11:00 休憩

11:00 〜 11:30

倉永 崇（名古屋大学大学院 多元数理科学研究科）

演題：

認知幾何学に向けて

梗概：

脳におけるchaotic itinerancyを見据え、脳の高次機能と 論理ないし言語との間を結ぶ幾何学的な装置の構築を目指している。 今回は、その基本的な考え方の提案と、general frameの変種、および presheafを使って得られる、ある種の”幾何学的な意味論”の紹介を行う。

11:30 〜 12:00

木下 佳樹（AIST）

演題：

NBE through Yoneda revisited in Agda

梗概：

古い話題ではあるが、Monoid の normalisation by evaluation を米田の補題で説明する。今回、Evaluator-reifier pair が ReflectionになっていることのAgdaによる証明をつけた。 以前は SML などによる項の定義しかなかった。

12:00 〜 12:30

クロージング＋連絡など