tozima's blog

主に自分のための、論文の読書記録

Automated Synthesis in Symbolic-Heap Separation Logic

POPL 2018

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

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

概要

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

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

  1. 生成された制約集合 \mathcal{C} の部分集合 \mathcal{D} \subseteq \mathcal{C} を適当に選び*2、
  2. その制約の解 \overline{U} を具体的に構成し、
  3. 元の判断に代入して \Gamma, \overline{U}(\vec{x}) \vdash \Delta の妥当性を検査して、正しければそれを補題とする

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

私見

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

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

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

Classifying and Solving Horn Clauses for Verification

2013 VSTTE

Philipp Rümmer, Hossein Hojjat and Viktor Kuncak

プログラム検証の文脈で使われている Craig interpolation の変種たちを CHC solving を使って分類した論文（計算量などの性質についても少し議論されている）

技術的な結果としては各種 interpolation と各種 CHC の等価性や計算量の解析などあるものの、本論文の価値は interpolation のサーベイ論文としての面にあるのではないだろうか。いろいろな interpolation の変種たちが出典付きで載っていて、interpolation について網羅的に調べたり、特定の interpolation の導入の動機を知りたかったりしたときに使えそう。

論文振り返り

僕の論文が小馬鹿にされているのを聞いて、むっとして反論を考えていたのだけど、冷静になって考えてみると、そうした反論は論文中に書かれているべきであり、また実際にいろいろと反省すべき点もあので、せっかくの機会に過去の論文を振り返り、反省を次の論文に生かしたいと思って書いています。

"An Intersection Type System for Deterministic Pushdown Automata" (IFIP TCS 2012)

Minamide & Tozawa (APLAS 2006) の CFL-RHL (= Regular Hedge grammar の生成する Language) 包含判定アルゴリズムが、自然に CFL-SPDL (= Superdeterministic Push-Down オートマトンの受理する Language) 包含判定に拡張できるということを示した論文。元々は高階に拡張することを念頭に置いていたため型システムの言葉で書いてあり、それがタイトルにも入っているが、交差型（Intersection type）は本質ではなく、査読者にも不評だった。Minamide & Tozawa 式の記法のような、オートマトンの専門家に読みやすい記法にするべきだったと、今は思う。（当時は型の記法の方が "万人にとって" 分かり易いはずだという勘違いをしていた。恥ずかしい限りである。）

肝心の貢献については、価値ある新しい命題の証明には至らなかったため、「オリジナルの証明よりも簡潔である」という、非常に主観的かつ乱暴な主張をすることになってしまった。この点については、批判は甘んじて受けねばなるまい。実際のところ、プッシュダウンオートマトンの専門家の視点から見たときに、オリジナル（Greibach & Friedman, J.ACM 1980）の証明がどの程度の複雑なものであるかは、当時も今も、とんとわからない。SPDAの定義ひとつを取っても、本論文における定義は Greibach & Friedman の定義よりも良いと思う（例えば、SPDL が RHL の拡張であることが自然に表現されている）が、オートマトンの専門家には Greibach & Friedman から本論文における定義と同じ直観を得られるのかもしれない。（定義を思いつきさえすれば、２つが同じ言語を定めることは自明なのだが。。。）[追記 3 Oct 2014：少し考えた結果、論文中の定義と Greibach & Friedman の定義の間に違いなんて、大してないという結論に至った。]そういった忌憚のない意見は、南出先生（筑波大学）を訪問したときに、研究グループの誰かに伺えばよかったのだが、つい忘れてしまっていた。なお、忌憚のない意見は現在も募集中です。メールでもくれるとありがたいです。

Minamide & Tozawa のアルゴリズムが SPDA に拡張できるという結果は、自明ではないとは思う。この点を強調した論文の流れにした方が良かったのかもしれない。例えば、Minamide & Tozawa のアルゴリズムの紹介、その SPDA への拡張、実装・評価、というような。応用を思いつかないので、評価のサンプルインプットに困ってしまうが。実際の論文は「Minamide & Tozawa よりもすげーぜ！」といった体であり、大変に残念なできである。

ひとつくらい、非自明な帰結について触れておこう。CFL-SDPL包含判定は 2-EXPTIME complete であることが知れらているが、２段の指数関数のうちひとつは、CFL reachability problem の（最短の） witness の長さが exponential であるという事実から従う。より具体的には、次の通りである：

  • PDA A と SPDA B が与えられたとする
  • SPDA B のスタックを忘却した有限状態オートマトンを B' とする（B' は B の over-approximation になるように取る）
  • B' の状態の組（＝ B の状態の組）ごとに、L(A)-reachability を解き、witness を構成する。こうして構成された witness 達の長さの最大値を k とする
  • このとき、L(A) ⊆ L(B) は、k に対して指数時間で解ける

余談だが、Colin Sterling が「本論文の技術に inspire された real-time deterministic DPDA の言語同値性判定」のトークをしていて、大変に驚いたし、嬉しかった。この論文で提案した技術も、まったくの無価値というわけではなかったということだろう。それだけが救いである。

Swift の Array型の var の挙動

Swift の Array型の（書き換え可能な）変数の挙動が変だと、少し前に話題になっていたけれども、

var x = [1, 2, 3] : Array

なんてやったら x の型は（OCaml風の記法で）int array ref 型なんですが、int array は int list ref とか int table ref みたいなものだと思うと、x の型は int table ref ref みたいになるわけで、そりゃ、取扱いには注意せにゃならんでしょうよ。本当にこんな型の変数が必要なのかどうかから考え直すべきではないでしょうか。

手頃な演習問題

手頃な演習問題のメモ。

\Sigma を（空でない）有限集合とし \mathit{Reg}_{\Sigma} を \Sigma 上の正規言語の集合とする。この集合に部分集合関係によって順序集合となる：つまり L_1, L_2 \in \mathit{Reg}_{\Sigma} について、 L_1 \le L_2 iff L_1 \subseteq L_2。この順序について \mathit{Reg}_{\Sigma} はCPOを成すか。証明または反例を与えよ。

この問題そのものがひっかけ問題っぽい要素を持っている*1のですが、本当にひっかけ問題にしたかったら、 \Sigma が空でないという条件を外すのがおすすめです

*1: \mathit{Reg}_{\Sigma} から \mathcal{P}(\Sigma^*) への埋め込みが連続でないことを示すのは、上の課題の答えとしては不十分であるということです。

トレース意味論とゲーム意味論

トレース意味論とは、プログラムの意味を「実行したときに起きるイベントの列」として表現したものです。イベントとして何を考えるかは目的次第ですが、例えば「入出力」や「関数へ引数を渡す」などといったものが考えられます。以下でポイントになるのは、トレースは「列」だということです。トレースが持っている情報はイベント発生の時間的前後関係だけであって、因果関係などのイベント同士の依存関係は表現されません。

ゲーム意味論*1の基本的な考察対象は「プレイ」と「相互作用列（interaction sequence）」と呼ばれるものですが、これは本質的にはトレースにイベント同士の依存関係の情報が加わったものです。

トレース意味論の方が素朴で直観的に分かりやすい面もあると思うのですが、僕はゲーム意味論の方が好きです。僕がこうした意味論を使うのはプログラム検証のための性質を定義する場面になるのですが、トレース意味論は情報が多すぎて、定義した性質が実は検証できないという事態に陥りやすいと思うからです。一方ゲーム意味論では、イベント列から「使っても良い情報」を切り出す方法が確立されています。「View」と呼ばれる概念がそれです。「View」しか見られないというのは、はっきり言って不便なのですが、それと引き換えに「View」だけから定義できる性質はプログラムの構文との相性が良いです。

こういった理由で、僕にはトレース意味論は素朴すぎるように感じられます。もちろん用途次第ではトレース意味論の方が適している場合もあるはずですが。

*1:ここではHO/N styleのゲーム意味論を考えています。AJM styleのものは趣が異なります。

型無しλ計算の big-step semantics と game semantics

　　　　次のようなツイートを見かけたので、私なりの回答を。

　　　　「計算が止まらない」には少なくとも二種類、

(\lambda x. x\,x) (\lambda x. x\,x) \longrightarrow (\lambda x. x\,x) (\lambda x. x\,x)

のように無意味な計算が延々続くものと、

\lambda f. Y\,f \longrightarrow \lambda f. f (Y\,f) \longrightarrow \lambda f. f (f (Y\,f)) \longrightarrow \dots \longrightarrow \lambda f. f (f (f (f \dots))))

のように意味のある計算が続いた結果として無限サイズの値を返すものがあって、これらは区別されます。通常の型無しλ計算の big-step semantics では後者の評価は「停止する」と考えます。

　　　　Big-step semantics は項 Mと値 Vの関係 M \Downarrow Vを与えるものですから、はじめに「値はなにか」ということを考える必要があります。型無しλ計算では、値をλ抽象 \lam x. Mとするのが通例で、住井先生の以下のツイートもこの設定での話であろうと思います。

 

値をすべてのλ抽象とした場合、「評価が停止しない」項はBoehm木も \bot であり、Boehm木で考えても一点につぶれています（また game semantics でも一点に潰れます）。またBoehm木が \botでないなら、遅くとも head variable が決まるときには「評価が停止」しています。ちなみに逆は成り立たなくて、Boehm木は \bot だが「評価が停止する」項が存在します。例えば M = \lambda f. \lambda x. fとして、 N = M (Y\,M)を考えます。すると、

N = M (Y\,M) \longrightarrow \lambda x. Y\,M

ですので評価は停止します。しかしながら、

\lambda x. Y\,M \longrightarrow \lambda x. M (Y\,M) = \lambda x. N

であることを踏まえると、

N \longrightarrow^* \lambda x. N \longrightarrow^* \lambda x. \lambda y. N \longrightarrow^* \dots

となり NのBoehm木は \botです。

 　　　　それでは値をBoehm木とするような big-step semantics は考えられるかというと、困難があるように思います。できるのなら co-inductive なルールに基づく評価規則になるのだろうと思いますが、適用の規則が難しそうです。それなら game semantics でいいじゃないか、と思ってしまいます。
　　　　最後に small-step semantics との関係について。まず、small-step semantics と Boehm thoery は異なります。βη同値な項は同じBoehm木を持ちますが、同じBoehm木を持つβη同値ではない項が知られています。*1直観的には、βη同値性は有限ステップの簡約による等しさで、Boehm木の等しさは無限ステップの簡約による等しさなので、後者の方が各同値類が大きいということになるかと思います。

 

*1:Wikipediaの不動点演算子か何かの項に例があったと思います。βη同値ではないが、同じBoehm木はλf. f (f (f ...) )を持つ項が挙げられていたはずです。