最終更新日時: Last modified: 2014-08-21
13:15 ～ 13:30
オープニング＋連絡など
13:30 ～ 14:00
卜部 夏木（東京大学）
演題：Generic Forward and Backward Simulations III: Quantitative Simulations by Matrices
梗概：
We introduce notions of simulation between semiring-weighted au- tomata as models of quantitative systems. Our simulations are instances of the categorical/coalgebraic notions previously studied by Hasuo---hence soundness wrt. language inclusion comes for free---but are concretely presented as matrices that are subject to linear inequality constraints. Pervasiveness of these formalisms allows us to exploit existing algorithms in: searching for a simulation, and hence verifying quantitative correctness that is formulated as language inclusion. Trans- formations of automata that aid search for simulations are introduced, too. This verification workflow is implemented for the plus-times and max-plus semirings.
14:00 ～ 14:30
室屋 晃子 (東京大学)
演題：Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction
梗概：
We present a prototype implementation of the memoryful GoI framework of [Hoshino, Muroya and Hasuo, CSL-LICS 2014] that translates lambda terms with algebraic effects to transducers. Those transducers can be thought of as “proof nets with memories” and are constructed in a compositional manner by means of coalgebraic component calculi. The transducers thus obtained can be simulated in our tool, too, helping us to scrutinize the step-by-step interac- tions that take place in higher-order effectful computation.
14:30 ～ 14:45 休憩
14:45 ～ 15:15
浦本 武雄（京都大学）
演題：正規言語のvariety theoryの現代的定式化について
梗概：
正規言語は、正規表現によって記述できる言語であったが、一つの正規言語を記述するにも複数 の正規表現があり得る。そのため、書き下した正規表現を（なんらかの基準の下で）最も良い正 規表現に最適化する問題は、正規表現によるパターンマッチの処理効率を挙げる上でも基本的な 問題となる。正規言語のvariety theoryはこの種の問題に対して、一定の方法論を提供するものであり、形式言語理論の中でも特 に豊かな歴史と内容を持つ理論である。近年、variety theoryの研究では、Stone双対定理を使って理論を再証明・再構築する動きがあり、本研究もそ の文脈に属している。本発表では特に、正規言語のvariety theoryの背景からはじめ、ガロア圏や可換代数の理論と、正規言語のvariety theoryがどのよう に関連していくのかについて話す。
15:15 ～ 15:45
柳澤 名由太（京都大学）
演題：Simple Proof for FLP Impossibilities
梗概：
分散コンピューティングの分野におけるここ20年間で最も目覚ましい発展として，組合せ位相幾 何学を用いた種々の不可能性証明が挙られる．しかし，得られた結果の多くはtask specificなものであり，一般のtaskについて論じたものは少ない．そこで．我々はslim taskというクラスを定義し，そのクラスに属するすべてのタスクの不可能性をwait-free crash failureを伴うasynchronous layered immediate snapshot modelにおいて証明した．
15:45 ～ 16:00 休憩
16:00 ～ 16:30
倉永 崇（名古屋大学）
演題：A Logic for Logic-free Logics
梗概：
1つのagentを固定したときの、そのagentのidiolectの形式的な扱いを可能にする 枠組みの構築を目指している。そのidiolectに属する各文は、当のagentにとって、 出力とも入力ともみなせるため、2種類の意味論が自然に考えられ、それぞれおよそ、 表示的、動的なものに対応する。当面の目標は、この2つの意味論を1つの大きな 枠組の中に取り込むことだが、完成はしていない。今回は、まだその断片でしかない 各枠組みについて紹介する。
16:30 ～ 17:30
安部 達也（理化学研究所）
演題：メモリ一貫性モデルを考慮した半自動定理証明に向けて
梗概：
メモリ一貫性モデルを考慮したプログラム検証のために無閉路有向グラフによるプログラムの表 現を提案し、共有メモリとストアバッファとを状態とする操作的意味論を与える。また、ホーア スタイルの論理を与え、その意味論に対する健全性・相対完全性を示す。最後に、この表現を採 用するにいたった動機、特に、半自動定理証明に向けての試みについて紹介する。
18:00 ～ 20:00
懇親会（神奈川大学内 19号館地下1階LUX）
10:00 ～ 10:45
田中 義人（九州産業大学）
演題：Semilattice models for EL
梗概：
EL is a lightweight description logic, which is of importance for providing a logical foundation for ontologies. From the point of view of modal logics, the syntax of EL is a fragment of multi-modal logic which contains only top, bottom, conjunction and diamonds as its language, and its interpretations are Kripke models, which are equivalent to Boolean algebras with operators (BAOs). In this talk, we present an algebraic semantics for EL based on semilattices with operators (SLOs). In [1], Stokkermanns proved that a concept inclusion of EL is valid in the class of SLOs if and only if it is valid in every interpretations of EL, which means a natural proof system is sound and complete with respect to the interpretations of EL, as one can identify algebraic semantics with proof systems. However, it is not clear that the systems with additional axiom schemas are still complete with respect to the interpretations of EL.
We approach this problem by means of algebraic models, and present some results including that the only four subvarieties of the variety of SLOs defined by equations $f(x\land y)=fx\land fy$ and $fx\leq ffx$ are embeddable in to BAOs, from which follows that the only four axiom schemas have a complete system with respect to the interpretations of EL, if the axiom schemas corresponding above equations are assumed.
This is a joint work with A.Kurucz, F.Wolter and M.Zakharyaschev.
[1] Viorica Sofronie-Stokkermansmans. Locality and subsumption testing in EL and some of its extensions. In Carlos Areces and Robert Goldblatt, editors, Advances in Modal Logic 7 (AiML'08), pages 315?339. College Publications, 2008
10:45 ～ 11:00 休憩
11:00 ～ 11:30
向井 国昭（慶應義塾大学 名誉教授）
演題：文字クラスのブール代数上の最小オートマトンの構成とProlog限定節文法への組み込み
梗概：
正規表現から有限オートマトンを合成する方法は形式言語理論の古典としてもよく知られているが, 次の要請をすべて満たす実装はまだ無いようである(サーベイ中)．(1) 正規表現は文字クラス表現が指定可能． (2) 連接および星演算の他に，ブール演算が指定できる．(3) 状態数が最小である. (4) Prologの限定節文法の自然な拡張として，とくに，マクロ機能として組み込めること． 以上の要請をすべて満たす実装が得られたことを報告する．オートマトンを余代数として実装しているので， 終余代数定理と双模倣双関係により合成手続きの正当性は明白である．なお, 文字クラスは整数の区間のなす ブール代数としてモデル化しているが，生成されるコードは状態名としての生成述語以外は 新たな実行時ライブラリ述語は必要ない. マクロはSWI-Prologの開発版上に実装した. 動作は安定している.
11:30 ～ 12:00
星野 直彦（京都大学）
演題：Memoryful Geometry of Interaction
梗概：
Girard’s Geometry of Interaction (GoI) is interaction based semantics of linear logic proofs and, via suitable translations, of functional programs in general. Its mathematical cleanness identifies essential structures in computation; moreover its use as a compilation technique from programs to state machines―“GoI implementation,” so to speak―has been worked out by Mackie, Ghica and others. In this paper, we develop Abramsky’s idea of resumption based GoI systematically into a generic framework that accounts for computational effects (nondeterminism, probability, exception, global states, interactive I/O, etc.). The framework is categorical: Plotkin & Power’s algebraic operations provide an interface to computational effects; the framework is built on the categorical axiomatization of GoI by Abramsky, Haghverdi and Scott; and, by use of the coalgebraic formalization of component calculus, we describe explicit construction of state machines as interpretations of functional programs. The resulting interpretation is shown to be sound with respect to equations between algebraic operations, as well as to Moggi’s equations for the computational lambda calculus. We illustrate the construction by concrete examples.
12:00 ～ 12:30
クロージング＋連絡など