SLACS 2011 最終確定プログラム

場所：奈良女子大学G棟G302教室
9月12日(月)
14:00--14:10 （オープニング、連絡など）
14:10--14:30 小島侑子（奈良女子大学）「小型ロボットを制御するための汎用ライブラリの開発」
近年、安価で小型なロボットの登場がロボットの研究に新たな可能性をもたらしている。我々は、その1つであるLEGO MINDSTORMS NXTの制御プログラムの作成を容易にするため、新たなNXT制御ライブラリを提案する。特に、反射的行動を記述したライブラリにするなど、ロボットの行動制御の研究を容易にすることを主眼に置く。
14:30--15:00 中澤巧爾（京都大学）「Combinators for streams」
本発表では，型無しラムダ・ミュー計算に同等なcombinatory calculusとしてCLμを提案する． また，型無しラムダ・ミュー計算のモデルとしてstream modelを定義し，CLμの構造をもとにして stream modelの代数的な特徴付けを行なう．
（休憩）
15:45--16:30 Michele Basaldella（京都大学）「Infinitary completeness in ludics」
Traditional Goedel completeness holds between finite proofs and infinite models over formulas of finite depth. In this talk, we generalize it to a completeness theorem between infinite proofs and infinite models over formulas of infinite depth (that include recursive types).
16:30--17:00 藤田恵（奈良女子大学）・片山寛子（奈良女子大学）・新出尚之（奈良女子大学）・高田司郎（近畿大学） 「実世界の多様性に適応したBDIロボットについて」
近年、単一の目標達成に特化されたロボットでなく、動的に変化する環境のもとで自らの目的を達成するよう動作するロボットの実現が重要な研究課題となってきている。我々は、BDIモデルを実装したBDIロボットによるロボット制御が、複雑で多様性に富んだ実世界において自らの目的を実現していくロボットのためのアーキテクチャとして有効であることを示す。特に、意図の保持と破棄という機構によって、目標を達成する手段を柔軟に切り替えたり、複数の目的を並行に保持し整合的に実行したりできるBDIモデルの能力が、多様性への適応に非常に有用であることを論じ、また、実験を通じてそれを示す。
（移動）
18:30-- 懇親会
9月13日(火)
10:15--10:45 岡章弘（京都産業大学）・三好博之（京都産業大学）「リアクティブシステムのモノイダル2-圏による定式化」
LeiferとMilnerは圏を用いて抽象的なリアクティブシステムを定式化し，Milnerはその枠組みで具体的にバイグラフを用いてシステムの記述を行う研究を行った。しかしMilnerの体系では，リアクティブシステムからラベル付き遷移系(LTS)を導くのにサポートと呼ばれるデータが必要であり，そのために圏ではなく前圏(precategory)を用いているためかなり複雑である。そこでSosanneとSobocińskiはサポートと2-圏の2-セルとの類似性に着目して亜群によりenrichされた2-圏による定式化を行った。本講演ではこれにモノイダル積を加えることによりシステムの並置を陽に含む定式化を行う。これによりシステムをより自然に圏論的な構成として記述することができる。ここではさらにstcasticなシステムへの圏論的な拡張も視野に入れている。
（休憩）
11:15--12:00 向井国昭（慶應義塾大学）「チャネル理論の分類概念再訪」
Barwise/Seligmanのチャネル理論(1997)は，タイプとトークンの間の関係としての分類だけでなく，タイプ間の制約としての局所論理を動員して情報の流れをモデル化しようとする試みである．チャネル理論は，すでに抽象設計論(角田・菊池) など多くの発展および応用を得ている．
チャネル理論の局所論理は，大域カット則を充足する理論を正則とする．なぜ大域カットなのだろうか？ また，大域カットは通常のカット推論規則よりも強いが，有限の証明図および有限のシーケントに限定すればそれらは等価となるのだろうか？
この「保守拡大性」に関しては，選択公理を使って肯定的な証明が得られた．このようにチャネル理論の「重箱の隅」をつついているうちに，分類と情報射の意味と役割が次第によくわかってきた．大域カットのねらいも見えてきた．さらに位相空間(連続写像)や可測空間(可測写像)，もっと身近な線形空間(線形写像)やオートマトン(模倣)など， おなじみの数学的構造がすべてチャネル理論の分類(情報射)であることが実感をもって確認できた．この実感の共有は情報をめざす多くの人とくに学生諸君にとっても有用であると信じる．なお，井出陽子氏の関連結果 (修士論文2011) にもふれる．
12:00--12:20 片山寛子（奈良女子大学）「BDIロジックに基づくエージェント実行系の構築に向けて」
BDIモデルは、合理的エージェントの実現の基盤としてよく知られているが、BDIモデルの論理的な形式化に用いられるBDIロジックと現在提案されている手続的なBDIエージェントの実行系との間にはギャップがあることが指摘されている。本論文では、BDIロジックでの論理式による記述をそのまま実行可能なプログラムとして扱うようなBDIエージェントの実行系の実現に関するアイデアについて述べる。
（休憩）
13:20--14:20 丸山善宏（京都大学）「Duality and Abramsky's Representation of Quantum Systems」
Samson Abramsky recently proposed to represent quantum systems (or physical systems in general) as Chu spaces and as coalgebras. In this talk, we analyze duality-theoretic consequences of his representation of quantum systems, and then place the resulting dualities in a wider context of general duality theory, with the ultimate aim of clarifying the nature of duality between states and observables in quantum physics. We finally touch upon philosophical issues relating Abramsky's representation to Karl Popper's notion of verisimilitude.
14:20--14:50 小川美樹（奈良女子大学）・鴨浩靖（奈良女子大学）・新出尚之（奈良女子大学）「汎用的な証明図作成支援ソフトの構築」
証明図作成支援ソフトをJAVAで構築する。既存の物と比較して、次のような長所を持つものを作成しようと考えている。まず、JAVAで構築することによって汎用性の高いものにする。また、柔軟にレイアウトする機能を加える。さらに、半自動証明の機能も加える。
14:50--15:50 小林 聡（京都産業大学）「カットを含む証明のゲーム意味論」
構成的数学にΣ^0_1論理式に対する排中律を付け加えたものを極限計算可能数学 (LCM)と呼ぶ。構成的数学の証明からアルゴリズムを抽出できることはよく知ら れているが、LCM でも次のようにして一種のアルゴリズムを抽出できる。
LCM の算術の1つの形式化として無限論理上の Heyting Arithmetic のシーケン トを拡張して得られるある体系を考える。体系の閉論理式 A が任意に与えられ たとき、A に応じて1つのゲームが定まり、ゲームの先手の必勝法と A のカット なしの証明とがちょうどぴったり対応することがわかっている。このことを用い て、証明から必勝法という形でアルゴリズムを抽出でき、証明の内容を計算機上 で動かしてみせることができる。
では、カットを含む証明についてはどのようにアルゴリズムを対応させるべきで あろうか。本講演では、この問題に対していくつかのアイデアを示したあと、一 つの有望な方法として、カットを全て除去する代りに部分的な除去のみをくり返 しながら必勝手順を抽出する方法を提案する。また、この目的のためには Gentzen の Mix 規則を用いたのでは不都合なことを説明し、それに代る新たな規則を提案 する。
15:50--16:00 （クロージング、次回予告など）