SLACS 2009 - プログラム

スケジュール

8月31日(月)

13:00- 受付
14:00-15:20
木村大輔(東京大学) 「Dual Calculus with Inductive and Coinductive Types」 梗概 (40分)
佐々木克巳(南山大学) 「正規様相論理における、非同値論理式の構成法」 梗概 (40分)
15:20-15:40 休憩
15:40-17:20
杉山麿人(京都大学) 「Learning Figures with the Hausdorff Metric by Self-similar Sets」 梗概 (40分)
丸山善宏(京都大学) 「Two Notions of Point in Pointfree Convex Geometry」 梗概 (60分)
18:30- 懇親会

9月1日(火)

9:00-10:40
五十嵐 淳(京都大学) 「プログラム理論演習システムのための "Prelogical" Framework とその実装」 梗概 (40分)
岩沼宏治(山梨大学) 「一階論理上の下降形定理証明における等号計算の効率化」 梗概 (40分)
小川美樹(奈良女子大学) 「汎用的な証明図作成支援ソフトの構築」 梗概 (本発表はキャンセルされました)
10:40-11:00 休憩
11:00-12:00
大崎人士(産業技術総合研究所) 「可換文法−commutative grammar」 梗概 (60分)
12:00-13:30 昼食・休憩
13:30-14:30
宮部賢志(京都大学) 「An extension of van Lambalgen's Theorem to infinitely many relative 1-random reals」 梗概 (60分)
14:30-14:50 休憩
14:50-16:10
小島健介(京都大学) 「Kripke-Style Semantics and Correspondents of Modal Type Systems」 梗概 (40分)
江口直日(神戸大学) 「項書換え理論の計算量のクラスへの応用」 梗概 (40分)

梗概

Dual Calculus with Inductive and Coinductive Types

木村大輔(東京大学)

正規様相論理における、非同値論理式の構成法

佐々木克巳(南山大学 情報理工学部)

正規様相論理における、非同値論理式の構成法について述べる。具体的には、 これまでS4のみに適用していた構成法の正規様相論理への拡張を述べる。 また、この方法と、L. S. Mossの2007年の論文で用いられた構成法との比較も述べる。

Learning Figures with the Hausdorff Metric by Self-similar Sets

杉山麿人(京都大学大学院 情報学研究科 知能情報学専攻 知能情報基礎論分野)

The Gold-style learning model, which is a traditional model of computational learning theory, have been analyzed in detail, where learning targets are "discrete". However, this learning model is not so often used in knowledge discovery, since actual objects of experimental science are usually "continuous". Here we show a new Gold-style learning model for continuous targets, where the Hausdorff metric is introduced for measuring a generalization error of each hypothesis. We set learning targets as figures, which are compact sets on the Euclidean space, and represent figures by logic programs through self-similar sets. We prove classes of self-similar sets that can be learned in the limit from complete or positive data, and also prove that every figure can be learned effectively from complete data. Furthermore, we show that the number of positive examples is characterized by the Hausdorff dimension of a target figure.

Two Notions of Point in Pointfree Convex Geometry

丸山善宏(京都大学 文学研究科)

点概念を仮定しない代数的な位相空間概念として frame (或は locale) が知られている。 本研究は、convex geometry における集合論的な convexity space の概念を束論的に抽象化することにより、点概念を仮定しない代数的な convexity space の概念として convexity algebra というものを導入し、 "pointfree convex geometry" のための土台を確立することを目的とする。 本発表では特に、convexity algebra から点を復元するための二種類の方法とそれぞれから導かれる二種類の双対性について考察する。

プログラム理論演習システムのための "Prelogical" Framework とその実装

五十嵐 淳(京都大学大学院 情報学研究科)

講演者が京都大学で行っているプログラム理論(主に core MLの操作的意味論・型システム) に関する大学院講義「ソフトウェア基礎論」のための演習システムの設計と実装について概説する.

演習システムは,学生が入力した具体的なMLプログラムの評価や型付けの導出を検査し正誤を返す CGI プログラムである.導出の正しさの検査をする部分は OCaml で書かれているが, これは推論規則や抽象構文定義を含む体系記述から自動的に生成されている. 自動生成をする理由は, 講義の進度に応じて拡大・修正されていく対象言語ひとつひとつについて導出検査器を手で作成するのは手間がかかり誤りが混入しやすいためである. 我々は,形式体系記述のためのメタ言語 Prelog(仮称) を設計し, 導出検査器を自動生成するコンパイラを作成した. Prelog の特徴は,推論規則中でOCaml関数によって実装された述語を使用できることにある. これにより,非形式的に記述される付帯条件を簡単に表現することができる.

一階論理上の下降形定理証明における等号計算の効率化

岩沼宏治(山梨大学大学院 コンピュータ・メディア専攻)

一階論理上の等号計算は,下降形び定理証明の枠組みでは, その効率化が極めて難しいことが良く知られている. Brand の modfication 法は一つの対処法として有名であるが,依然として幾つもの問題点が残っている. 本発表では一つの改善法を提案し,実験的評価を行ったので報告する.

汎用的な証明図作成支援ソフトの構築

小川美樹(奈良女子大学大学院 人間文化研究科 情報科学専攻)

証明図作成支援ソフトをJAVAで構築する。既存の物と比較して、 次のような長所を持つものを作成しようと考えている。 まず、JAVAで構築することによって汎用性の高いものにする。 また、柔軟にレイアウトする機能を加える。さらに、半自動証明の機能も加える。

可換文法−commutative grammar

大崎人士(産業技術総合研究所)

An extension of van Lambalgen's Theorem to infinitely many relative 1-random reals

宮部賢志(京都大学 数理解析研究所)

Martin-L\"{o}f randomnessとは、0と1の無限列がランダムであることを、 計算の観点から定義づけしたものである。Kolmogorov Complexityやmartingaleにより同値な定義を与えられることも知られている。 これらは0と1の無限列と実数を同一視して、1-random realと呼ばれる。 1-random realはランダムな列として自然な性質を持っていて、van Lambalgenは、 ある列が1-randomであることと、その奇数番目の列が1-randomであり、 かつ偶数番目の列が奇数番目の列に対して1-randomであることが同値であることを示した。 しかし、無限個の互いにランダムな列では、成り立たない。今回の講演では、 それぞれの列の最初の有限個をうまく変更することで、van Lambalgenの定理が 無限個の無限列に拡張できることを示す。van Lambalgenの定理は、 Martin-L\"{o}f testを利用したシンプルな証明が知られているが、 今回はmartingaleを利用する。その議論からmartingaleの方が真に解析力が強いことも分かる。

Kripke-Style Semantics and Correspondents of Modal Type Systems

小島健介(京都大学大学院 情報学研究科)

Curry-Howard 同型対応の直観主義様相論理への拡張は、様々な動機から提案されている。 それらの既知の計算体系 (のうち可能様相に相当する型をもつもの)の多くについて、 対応する直観主義様相論理での可能様相は non-normal となる。 これは、通常の Kripke semantics における様相の意味付けと、 型システムにおける様相型の意味とが正確には一致しないためではないかと考えられる。 このような文脈で現れる non-normal な直観主義様相論理に対しても Kripke semantics が過去に考えられてはいるが、 計算体系における様相型の意味との関係は明らかではない。 本発表では、その関係がより明確になるような Kripke semantics の定義について考察する。

項書換え理論の計算量のクラスへの応用

江口直日(神戸大学 工学研究科)

本講演では,計算機によらずに計算量のクラスを特徴づけるという分野 (implicit computational complexity) の項書換え理論の観点からの研究について概説する. 特に,LOGSPACE, P, PSPACE, EXPと呼ばれる計算量のクラスに関する講演者の研究成果を紹介するとともに, 近年T. Arai, G. Moser, J.-Y. Marionらによって得られた結果との比較をしたい.


[SLACS 2009 home]

世話役

中澤 巧爾 (京都大学大学院情報学研究科)