Automated Synthesis in Symbolic-Heap Separation Logic

(Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo and Wei-Ngan Chin)

Separation logic の symbolic heap の entailment problem を解くために、自動で補題発見をしようというもの。その方法は、補題が必要そうな場所に（解釈を定めない）述語変数を置き、述語変数付きの判断の証明探索を行いながら述語変数への制約を収集し、集まった制約を解くというもの。未知述語変数付き判断の証明規則には、普通の証明規則に加えて、例えば 「」 という判断は「 という制約の下で空の仮定から証明できる」のような述語変数への制約付き規則がある。

概要

こういった研究の場合、まずポイントとなるのは、どこでどのように述語変数を使うかであろう。本論文においては次のようにしている：証明したい判断についての証明探索中で というゴールが出現したら、 と の適当な部分 を取り出して、 や といった形の未知述語変数付き判断を考える（つまり上手い U と V を探す）。ここで は に現れる変数全部の列挙である*1。もしこのような U があれば、そのひとつの解を としたとき、 を補題として登録する。

上の直感を押さえたら、後は比較的細々とした（しかしながら一定の重要性のあると判断されたであろう）ヒューリスティクスの話である。数ある議論の中で最も大切であろうヒューリスティクスを紹介する。ここでポイントとなるのは という判断の証明のための制約集合は、判断だけに依存するのではなく、証明の構造に依存するということである。極端な話、 が証明可能であれば U への制約は空にもできるが、一方で という制約付き規則を使って証明することもできる。この例では２つの制約は論理的に等価だが、 の証明探索中で可逆でない規則を使用すると論理的に等価でない制約を得ることがありえて、一般には解の有無まで異なる場合があるのが難しいところである。本当に欲しい制約は「目的の判断を証明する際に本当に現れる証明構造」から抽出される制約であるが、それが何であるかは探索中には分からない。したがって、本論文では、

1. 生成された制約集合 の部分集合 を適当に選び*2、
2. その制約の解 を具体的に構成し、
3. 元の判断に代入して の妥当性を検査して、正しければそれを補題とする

という手順で補題発見を行っている。

私見

最後に本論文の手法の本質的な限界について指摘しておく。本論文の補題の構成方法から、証明したい判断中に現れない再帰的な述語を自動で発見することはできない。それは未知述語 U を探す方法が、本質的には既存の証明探索手法に過ぎないためである。したがって、例えば list という述語（＝単方向リストであることを表す述語）だけが与えられた状況下で、証明には「要素が偶数のみから成るリスト」という概念が必要になる場合には、本論文の手法では原理的に扱えないものと思われる。

*1:実際にはここまでシンプルではない。その差は、例えば、対象が symbolic heap であることに由来する spatial formula と pure formula の区別などに起因するもの。また の方の右辺には、本当は存在量化が入る。

*2:細部が判然としないが、すべての部分集合を網羅的に試し、最初に成功したものを採用するようである。