Think Stitch
  最近の更新

Dominators に関する定理の証明

コンパイラのテキスト Modern Compiler Implementation in ML (1998) に出てくる dominators に関する定理を Isabelle で証明しました.

証明した主要な定理は次の2つです:

\[ D[s_0] = \{s_0\}, \quad D[n] = \{n\} \cup \left( \bigcap_{p \in \mathrm{pred}[n]} D[p] \right) \quad \mathrm{for}\ n \ne s_0 \]

\[ \mathit{DF}[n] = \mathit{DF}_\mathrm{local}[n] \cup \bigcup_{c \in \mathrm{children}[n]} \mathit{DF}_\mathrm{up}[c] \]

証明スクリプトはこちらです:

0  フォーマリズム

フォーマリズムの概要を解説します.

0.0  フローグラフ

まずフローグラフのノードを表す型 node を定義します.ノード間の接続は隣接関係 R で表します.ノード x からノード y への辺があるときかつそのときに限り (x, y) : R とします.

フローグラフには唯一の入り口があるとします.これを初期ノード s0 とします.すべてのノードは s0 から到達可能であるとします.これは反射的推移的閉包を使って表すことができます.

以上の前提を常に持ち回るのは面倒なので公理にしました.

typedecl node

axiomatization
  s0 :: "node" and
  R :: "node rel"
where
  reachable: "ALL n. (s0, n) : R^*"

0.1  パスの集合

初期ノード s0 から任意のノードへのすべてのパスの集合 Path を帰納的に定義します.

inductive_set
  Path :: "node list set"
where
  Path_b [intro, simp]: "[s0] : Path" |
  Path_i [intro]: "[| p#ps : Path; (p, q) : R |]
                    ==> q#p#ps : Path"

0.2  特定のノードへのパス

初期ノード s0 から指定されたノード n へのすべてのパスの集合 path_to n を定義します.

definition path_to :: "node => node list set" where
  "path_to n == {ps. ps : Path & hd ps = n}"

0.3  dominates 関係

ノード d がノード n を dominate しているという関係 d dominates n を定義します.(p.407)

「必ずノード d を経由する」という部分は「パスの要素であるノードからなる集合に d が含まれている」という形で表しました.

definition dominates :: "node => node => bool"  (infix "dominates" 60)
where "x dominates y == (ALL ps:path_to y. x : set ps)"

0.4  Dominators D[n]

ノード n のすべての dominator の集合 D[n] を定義します.

definition D :: "node => node set" where
  "D n == {x. x dominates n}"

0.5  Strictly dominates

関係 strictly dominates を定義します.長いので sdom にしました.(p.432)

definition sdom :: "node => node => bool" (infix "sdom" 60)
where "d sdom n == (d dominates n & d ~= n)"

0.6  Immediate dominator を定義するための述語 is_idom_of

Immediate dominator を定義する方法はいくつか考えられますが,あまり飛び道具を使いたくなかったので,ここでは definite description を使うことにしました.そのための述語 is_idom_of を定義します.(p.408)

definition is_idom_of :: "node => node => bool" where
"is_idom_of d n == (d ~= n & d dominates n &
                    (ALL x. x ~= n & x dominates n & d dominates x --> x = d))"

0.7  Immediate dominator idom(n)

Definite description "THE" を使って immediate dominator idom(n) を定義します.

余談ですが,テキストで関数の引数を D[n] とカギカッコで書く場合と idom(n) と丸カッコで書く場合は何が違うんでしょうね.

definition idom :: "node => node" where
  "idom n = (THE d. is_idom_of d n)"

0.8  Dominance Frontier

Dominance Frontier DF[n] を定義します.(p.432)

definition DF :: "node => node set" where
  "DF x = {w. EX p. (p, w) : R & x dominates p & ~(x sdom w)}"

0.9  Dominance Frontier を計算するための補助関数 DFlocal DFup children

Dominance Frontier を計算するための補助関数 DFlocal DFup children を定義します.(p.434)

definition DFlocal :: "node => node set" where
  "DFlocal n = {x. (n, x) : R & ~(n sdom x)}"
definition DFup :: "node => node set" where
  "DFup n = {x. x : DF n & ~((idom n) sdom x)}"

children には x ~= s0 が必要です.これは定義により初期ノード s0 が idom を持たないためです.

尚,p.434 の擬似コードにも s0 の idom に触れてしまうケースがあり,修正が必要です.

definition children :: "node => node set" where
  "children n = {x. x ~= s0 & idom x = n}"

1  証明した定理

1.0  D[n] についての性質 p.407

lemma D_s0: "D s0 = {s0}"
lemma D_step: "n ~= s0 ==> D n = {n} Un Inter {D p | p. (p, n) : R}"

1.1  DF[n] についての性質 p.434

lemma "DF n = DFlocal n Un Union {DFup c |c. c : children n}"

1.2  DFlocal[n] の計算アルゴリズムで使われている効率化

DFlocal[n] の計算では idom(y) を使う方がかんたんだと説明があり,擬似コードでもそのようになっています.これを証明しました.

ただし,そのままでは s0 の idom に触れてしまうケースがあるので修正が必要です.ノード n のすべての successor が s0 でないときだけ成り立ちます.(擬似コードも修正が必要です.)

lemma DFlocal_idom:
  "ALL y. (n, y) : R --> y ~= s0 ==>
   DFlocal n = {y. (n, y) : R & idom y ~= n}"

1.3  dominates が順序関係であること

上記性質を証明するための補題として dominates が順序関係であることを証明しています.特に D[n] の中では線形順序になります.

これは p.408 にある議論を形式化したものですが,well-founded ではなく帰納法を使いました(同じことですが).

lemma dominates_refl [simp]: "x dominates x"
lemma dominates_antisym: "[| x dominates y; y dominates x |] ==> x = y"
lemma dominates_trans: "[| x dominates y; y dominates z |] ==> x dominates z"
lemma dominates_linear: "[| d dominates n; e dominates n |] ==> d dominates e | e dominates d"

以上です.

2  教科書の errata

私が持っている1998年度版では DFup の定義に誤りがありました."dominated" は "strictly dominated" の誤りです.擬似コードも同様です.著者のページの errata を見たら1998年度版のところには訂正がありませんでした.1999年度版については訂正があるようです.つまり1999年度版にも誤りがあるということです.1999年度版は持っていないので確認できていませんが,同ページに似た文言があることからの推測です.

2017/12/02

© 2013-2017 PRINCIPIA Limited