Coq による証明付き Brick Corner Wang Tiling プログラム 松嶋 聡昭 （九州大学数理学府） 共同研究 ： 溝口 佳寛 （九州大学 IMI / JST CREST ） Alexandre Derouet-Jourdan (OLM Digital Inc. / JST CREST)

Presentation on theme: "Coq による証明付き Brick Corner Wang Tiling プログラム 松嶋 聡昭 （九州大学数理学府） 共同研究 ： 溝口 佳寛 （九州大学 IMI / JST CREST ） Alexandre Derouet-Jourdan (OLM Digital Inc. / JST CREST)"— Presentation transcript:

1 Coq による証明付き Brick Corner Wang Tiling プログラム 松嶋 聡昭 （九州大学数理学府） 共同研究 ： 溝口 佳寛 （九州大学 IMI / JST CREST ） Alexandre Derouet-Jourdan (OLM Digital Inc. / JST CREST) 2015.9.17 @TPP2015

2 Abstract 2 我々は今回 Coq を用いて， Wang Tiling を行う ためのプログラムを実装した． Coq … 証明支援システムの一つ． Wang Tiling … のちほど説明． これを使えば， Wang Tiling の一種である “Brick Corner Wang Tiling” の解が簡単に求まる． このプログラムから求まる解は， Coq によって 常に正しいものであることが証明される．

3 Wang Tiling とは 3 無限に広がる平面に，正方形のタイルを敷き詰 めて （ Tiling して）いくという問題 (Wang 1961) ． 各タイルの 4 つの辺には，色が塗られている． 右図のような感じ． （画像は Wikipedia 英語版 “Wang tile” より） 隣接するタイルの共有辺の色は同じでなければ ならない． つまり， のような並びはいいが， はダメ．

4 Wang Tiling とは 4 こんな感じで敷き詰める． 縦横の線がタイルの 境界である． 問題によっては， 使用可能なタイルの 種類が制限される こともある． この図も， 1 つ前の スライドで出てきた 13 種類の タイルだけで敷き詰められている．

5 Wang Tiling の関連研究 5 論理学的側面からの検証 予想 1 : 使用可能なタイルの集合が与えられたとき， 予想 1 : それらを使って無限に広がる平面を Tiling 予想 1 : できるかどうか判定するアルゴリズムが存在 する． → NO! (Berger 1966) チューリングマシンの停止性の問題と等価になるた め． 予想 2 : もし有限種類のタイルで無限に広がる平面を 予想 2 : Tiling できたなら，その Tiling は周期性がある． → NO! (Berger 1966, Culik 1996, Kari 1996) 最も少ないものでは， 13 種類のタイルだけで非周期 的な Tiling を実現できる (Culik 1996) ．

6 Wang Tiling の関連研究 6 論文 2. より， Wang Tiling を使った ヒマワリ畑の CG CG への応用 1.Aperiodic texture mapping (Stam 1997) 2.Wang Tiles for Image and Texture Generation (Cohen 2003) 3.Recursive Wang Tiles for Real-Time Blue Noise (Kopf 2006)

7 Brick Corner Wang Tiling とは 7 Wang Tiling 問題の一種． 使うことができるタイルは，以下の 2 パターン のみ． ① 上辺と下辺の色が等しく，左辺と右辺の色が異なる もの ② 上辺と下辺の色が異なり，左辺と右辺の色が等しい もの つまり， （ ① に該当）や （ ② に該当） は使えるが， や ， などは使うことはできない． もちろん のような「上下左右が全部同じ色」 の タイルも使うことはできない．

8 Brick Corner Wang Tiling の応用 8 例えば色の集合の代わりに，数の集合である {0.2, 0.4, 0.6, 0.8} を使ってみる． その上で，以下のようにタイルを生成する． 例：左＝右＝ 0.6 ，上＝ 0.8 ，下＝ 0.4 のとき 左＝右なので，まず左辺の座標 (0, 0.6) の点から， 右辺の座標 (1, 0.6) の点へ直線を引く． （上＝下のときは，先に上辺の点と下辺の点をつなぐ） 次に上辺の座標 (0.8, 1) の点と，下辺の座標 (0.4, 0) の点から 先程の直線に垂線をおろす． するとこんな感じのタイルができる →

9 Brick Corner Wang Tiling の応用 9 これをつなぎ合わせていくと，このようになる． 赤線部に注目すると， 大きさの異なる レンガ（ brick ）を 積み重ねたような 模様になっている． → レンガの CG にも 応用できる（らしい）．

10 Tiling プログラムの概要 10 3 × 4 の境界条件の例 → ここからは，今回我々が実装した Tiling プログラ ム について説明する． まず当然ながら，平面が無限大のままでは Tiling の プログラムは作成できない． そのため Tiling する領域は n × m （ n, m は自然 数） の長方形の中だけとする． 代わりに， Tiling する領域には 「境界条件」が与えられている ものとする．

11 Tiling プログラムの概要 11 また前提条件として，以下の 2 つを仮定する． ①Tiling に使える色は 3 色以上あるものとする． 1 色（全部 ）では，当然 Brick Corner Wang Tiling は実現 不可． 2 色でも，境界条件次第で Tiling できないものがある． ②Tiling 領域の長方形のサイズは 2 × 2 以上とする． n × 1 や 1 × m では，境界条件次第で Tiling できないものがあ る． 使用可能な色には，あらかじめ 0, 1, 2,... の番号 が 割り振ってあるものとする． つまり少なくとも， 0, 1, 2 の 3 色は使用可能とする．

12 Tiling プログラムの概要 12 プログラムの引数 長方形の縦の長さ n ，横の長さ m （型はいずれも nat ） nat … “ ” 境界条件 b （型は nat -> nat -> nat ） nat -> nat -> nat … “nat × nat → nat” とほぼ同義 プログラムの返り値 「横エッジ関数」 e （型は nat -> nat -> nat ） 「縦エッジ関数」 e’ （型は nat -> nat -> nat ） この 2 つについては，定義は後ほど．

13 タイルと辺のデータ構造 13 TILE EDGE Wang Tiling では，隣接する 2 つのタイルは同じ 色の 辺同士を共有する． ならばタイルではなく，共有している「辺 （エッジ）」の 方に着目してもいいのでは？ イメージとしてはこんな感じ．

14 タイルと辺のデータ構造 14 その上で各辺に，このように名前を付けていく． 横エッジは辺 h (0, 1) から辺 h (n, m) まで， 縦エッジは辺 v (1, 0) から辺 v (n, m) まで存在する．

15 タイルと辺のデータ構造 15 これを踏まえて，横エッジ関数 e ，縦エッジ関 数 e’ を以下のように定義する； e (i, j) := “ 辺 h (i, j) の色 ” ， e’ (i, j) := “ 辺 v (i, j) の 色 ” e や e’ の引数は nat なので， n や m を超える値も代入 できるが，返り値は意味を持たない． 逆に言えば， e と e’ が分かってしまえば，それ を もとに辺の色，すなわちタイルの配置を決定で きる． 今回我々が作ったのも，この e と e’ を求めるプログ ラム．

16 境界条件のデータ構造 16 境界条件 b も，辺の座標情報から辺の色を求め る という点では， e や e’ と同じ． 具体的には，以下のように境界を指定する． すなわち， e (0, j) = b (0, j) ， e (n, j) = b (n+1, j) ， e’ (i, 0) = b (i, 0) ， e’ (i, m) = b (i, m+1) ということになる．

17 境界条件のデータ構造 17 図で表すとこうなる． b の番号と h, v の 番号に若干ズレが あるので注意． 辺 h (n, m) と 辺 v (n, m) が共に 長方形の境界をなすため． 番号をずらさなければ，図中でいえば b (2, 3) が， 辺 h (2, 3) と辺 v (2, 3) のどちらに対応するのか 分からなくなる．

18 Tiling のアルゴリズム 18 for 文を使ってざっくり説明すると，こうなる． for ( i = n; i > 2; i -- ){ i × m の Tiling 領域の 1 行目にタイルを m 枚置いて， Tiling 領域を (i - 1) × m に狭める } for ( j = m; j > 2; j -- ){ 2 × j の Tiling 領域の 1 列目にタイルを 2 枚置いて， Tiling 領域を 2 × (j - 1) に狭める } 2 × 2 の Tiling 問題を頑張って解く

19 やっていることを，図で分かりやすく示す． Tiling のアルゴリズム 19 ← 1 行目を Tiling ↑ 1 列目を Tiling あとは 適当に 埋める ※適当に埋めるのが， 意外と難しいんだけどね …

20 プログラムの計算結果 20 このプログラムで Tiling の解を求めるときは， “ Compute (tiling_nm n m b). ” のように入力する． n : 縦の長さ， m : 横の長さ， b : 境界条件 例えば， n = m = 4 とし， b として “ (fun i j => match i with 0 => 2 | 3 => match j with 0 => 5 | _ => 1 end | _ => match j with 1 => 3 | _ => 4 end end) ” を使うと …

21 プログラムの計算結果 21 = (^ :: 2 :: ^ :: 2 :: ^ :: 2 :: ^ :: 2 :: ^ :: nil) :: (4 :: # :: 0 :: # :: 4 :: # :: 4 :: # :: 4 :: nil) :: (^ :: 2 :: ^ :: 2 :: ^ :: 0 :: ^ :: 0 :: ^ :: nil) :: (4 :: # :: 0 :: # :: 4 :: # :: 4 :: # :: 4 :: nil) :: (^ :: 2 :: ^ :: 2 :: ^ :: 1 :: ^ :: 1 :: ^ :: nil) :: (5 :: # :: 5 :: # :: 5 :: # :: 5 :: # :: 1 :: nil) :: (^ :: 0 :: ^ :: 0 :: ^ :: 0 :: ^ :: 1 :: ^ :: nil) :: (4 :: # :: 4 :: # :: 4 :: # :: 4 :: # :: 4 :: nil) :: (^ :: 3 :: ^ :: 4 :: ^ :: 4 :: ^ :: 4 :: ^ :: nil) :: nil : list (list nat) このように表示される（インデントは勝手に調 整）． 数字が色を， # がタイルの中心を， ^ が隅を表す． Coq では，本格的な図が描けない（たぶん）． → 他のプログラム言語に出力してみたい！ →Java や Mathematica に移植してみたい！

22 プログラムの正確性の証明 22 Coq で実装したプログラムの最大の利点は， プログラムに誤りがないことを証明できること． このプログラムでも正確性を証明した．手順は以下 の通り． ①2 × 2 の Tiling を，任意の境界条件に対して正確に求められ る ことを示す（ 408 行，やっぱりこれが一番大変）． ② 上の ① から m に関する帰納法で，任意の m > 1 に対して， 2 × m の Tiling を，任意の境界条件に対して正確に求められ る ことを示す（ 109 行）． ③ 上の ② から n に関する帰納法で，任意の n > 1 に対して， n × m の Tiling を，任意の境界条件に対して正確に求められ る ことを示す（ 117 行）．

23 簡潔に言えば，サイズ n × m の境界条件を， … という感じで 2 × 2 まで落とし込め，というこ と． プログラムの正確性の証明 23 ← 1 〜 (n - 2) 行目を Tiling ↑ 1 〜 (m - 2) 列目を Tiling ← 2 × 2 は常に Tiling 可能！

24 プログラムの正確性の証明 24 ↑ 正確性の 3 条件のソースコード ちなみに，「解が正確である」ことの条件は， ① 左端，右端のエッジが境界条件を満たしていること （ Boundary_i ） ② 上端，下端のエッジが境界条件を満たしていること （ Boundary_j ） ③ 各タイルが Brick Corner の条件を満たしていること （ Brick ） の 3 つの論理積 で与えている．

25 プログラムの正確性の証明 25 2 × 2 以上の領域を 3 色以上で Tiling する場合， プログラムの計算結果が正しいと証明できた． これを使えば，任意の 2 × 2 以上の領域は 3 色で Tiling できるという事実が系として得られる． Tiling できるということは，すなわち「前スライドの 3 条件を 満たすエッジ関数が存在する」ことである． Coq では exists e e’ : edge,... のように書かれる． 今回はこのプログラムの計算結果が「 3 条件を満たす エッジ関数」になるため，この命題は正しいと言え る．

26 まとめと今後の課題 26 これまでにできたこと 3 色以上， 2 × 2 以上での Tiling プログラムの実装 プログラムの出力結果に誤りがないことの証明 3 色以上， 2 × 2 以上なら Tiling が可能であることの証 明 これからやりたいこと 出力される Tiling 結果の改善 ランダム性向上，特定のタイルを多く使う， etc... 他言語への移植と図形描画による可視化 Tiling 領域が長方形でない場合のプログラムの作成

27 参考文献 27 Proving theorems by pattern recognition—II, H. Wang, 1961 The undecidability of the domino problem, R. Berger, 1966 An aperiodic set of 13 Wang tiles, K. Culik, 1996 A small aperiodic set of Wang tiles, J. Kari, 1996 Aperiodic texture mapping, J. Stam, 1997 Wang Tiles for Image and Texture Generation, M. F. Cohen, J. Shade, S. Hiller, O. Deussen, 2003 Recursive Wang Tiles for Real-Time Blue Noise, J. Kopf, D. Cohen, O. Deussen, D. Lischinski, 2006 Wang Tiles Modeling of Wall Patterns, A. D.-Jourdan, Y. Mizoguchi, M. Salvati, 2015 （ MEIS2015 にて発表予 定）

28 28 ご清聴ありがとう ございました！ Thank you for listening!