正規様相論理における、非同値論理式の構成法について述べる。具体的には、 これまでS4のみに適用していた構成法の正規様相論理への拡張を述べる。 また、この方法と、L. S. Mossの2007年の論文で用いられた構成法との比較も述べる。
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.
点概念を仮定しない代数的な位相空間概念として frame (或は locale) が知られている。 本研究は、convex geometry における集合論的な convexity space の概念を束論的に抽象化することにより、点概念を仮定しない代数的な convexity space の概念として convexity algebra というものを導入し、 "pointfree convex geometry" のための土台を確立することを目的とする。 本発表では特に、convexity algebra から点を復元するための二種類の方法とそれぞれから導かれる二種類の双対性について考察する。
講演者が京都大学で行っているプログラム理論(主に core MLの操作的意味論・型システム) に関する大学院講義「ソフトウェア基礎論」のための演習システムの設計と実装について概説する.
演習システムは,学生が入力した具体的なMLプログラムの評価や型付けの導出を検査し正誤を返す CGI プログラムである.導出の正しさの検査をする部分は OCaml で書かれているが, これは推論規則や抽象構文定義を含む体系記述から自動的に生成されている. 自動生成をする理由は, 講義の進度に応じて拡大・修正されていく対象言語ひとつひとつについて導出検査器を手で作成するのは手間がかかり誤りが混入しやすいためである. 我々は,形式体系記述のためのメタ言語 Prelog(仮称) を設計し, 導出検査器を自動生成するコンパイラを作成した. Prelog の特徴は,推論規則中でOCaml関数によって実装された述語を使用できることにある. これにより,非形式的に記述される付帯条件を簡単に表現することができる.
一階論理上の等号計算は,下降形び定理証明の枠組みでは, その効率化が極めて難しいことが良く知られている. Brand の modfication 法は一つの対処法として有名であるが,依然として幾つもの問題点が残っている. 本発表では一つの改善法を提案し,実験的評価を行ったので報告する.
証明図作成支援ソフトをJAVAで構築する。既存の物と比較して、 次のような長所を持つものを作成しようと考えている。 まず、JAVAで構築することによって汎用性の高いものにする。 また、柔軟にレイアウトする機能を加える。さらに、半自動証明の機能も加える。
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の方が真に解析力が強いことも分かる。
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らによって得られた結果との比較をしたい.
中澤 巧爾 (京都大学大学院情報学研究科)