日々の流転

λ. “The IDP framework for declarative problem solving” by Maarten Mariën, Johan Wittocx, and Marc Denecker

以前2009-03-04に数独を解いてみたIDP(Inductive Definition Programming)フレームワークの解説。背後にあるロジック、記述言語、動作例が中心で、ソルバーの仕組みにはあまり触れていない。

IDPの背後にあるロジックは、ソート付きの一階述語論理を帰納的定義で拡張したもので、問題は「指標Σ, セオリーT, 部分指標σ⊆Σ, 有限のσ構造A_Iの組〈Σ, T, σ, A_I〉が与えられたときに、A_Iの拡張で(A|_σ = A_I)、Tを満たす(A ⊨ T)ようなΣ構造Aを求める」というモデル拡張問題(model expansion problem)として形式化される。

また、問題の記述スタイルとしては、問題の一般的なルールをΣとTによって記述し、具体的な盤面など問題のインスタンスに固有の情報をA_Iで与えるというスタイルになっているのが面白い。

実装については以下のように書いてあった。

Its algorithms consist of an adaption of the DLL algorithm to rules, augmented with a variant of Smodels' AtMost. As such, the solver incorporates techniques from state of the art SAT and ASP solvers.

読んでると、解集合プログラミング(Answer Set Programming, ASP)との比較をかなりしている一方で、MaceやParadox等の一階述語論理のモデル発見器(model finder)については全く言及してなくて、ちょっと意外な感じがした。 ASPは最小エルブランモデルの一般化であるところの解集合を求めるので、ある意味全体が帰納的定義になっている一方で、一階述語論理のモデル発見器は帰納的定義が出来ないので、比較対象としてはASPの方が適当ということなのかな。 ただ、ASPが項をエルブラン宇宙で解釈するのに対して、IDPは一階述語論理のモデル発見器は任意の解釈をするので、実装的には一階述語論理のモデル発見器に近い部分もあると思うし、帰納的定義の追加による性能への影響とかも気になることは気になる。

それから、ちょっと気になったのは、以下の部分。

A historical AI argument (e.g. [15]) against FO as a computational logic is the semi-decidability of the deduction problem (and worse, undecidability in the case of FO(ID)).

一階述語論理FOがsemi-decidableなのはいいんだけど、一階述語論理に帰納的定義を加えたFO(ID)がundedidableというのはホント?　一階述語論理と同様に証明を枚挙して証明チェッカにかけるという方法は使えないのだろうか?

λ. お墓参りなど

家族でお墓参り。渋滞にはまってウンザリ。あと、やっぱり暑い。 お昼は、竹治(たけはる)というところで、まぐろ重なるものを食べた。

それから、プールでひと泳ぎし、夜は帰省した友人らと飲み会。 はじめて飲み会後にラーメン屋にいくなど。