λx.x K S K @ はてな このページをアンテナに追加 RSSフィード

2015年12月13日

[][] TRICK 2015 に入賞しました

TRICK というのは Transcendental Ruby Imbroglio Contest for rubyKaigi の略で, Ruby を使って狂ったプログラムを書くというコンテストで,今回が 2 回めだそうです. 今年の 9 月の FTD 2015 (日本ソフトウェア科学会大会の併設イベント) で TRICK 2015 のことを知り, 遠藤さんから「なにかネタがあったら投稿しませんか」というお話をいただいたので,参加させていただきました. 思いついたネタとしては 3 つほどあって, 実は 3 つとも投稿できる状態にはなっていたのですが, 1 つは完成度的にいまいちだったので投稿を断念し,残りの 2 つを投稿しました. どちらか一方でも審査員の目に留まれば…と思っていたのですが, なんと 2 位と 5 位という非常にありがたい評価をいただきました. ただ,企業の大合併とは違うので 2 位と 5 位を合わせたからといって 1 位に勝ることはありません. 実際,1 位の作品には到底及ばなそうです.

入賞された皆さんが続々と自分の作品を解説記事を公開しているので,私も自分の 2 作品について解説しておきます. とはいっても,言いたいことはすべて remarks.markdown の中にあるので, 詳しく知りたい方はそちらをご覧ください (各作品へのリンク先にあります).

第 5 位 最短 SAT ソルバ

SAT 問題は,「¬A ∧ (B∨A)」のような論理式に対し,それを真にする変数A, Bの真偽値割当て (この論理式なら A=偽, B=真) を見つける問題で, その問題の難しさは変数の個数に対して NP 完全であることが知られています. 奇しくも,第 4 位の作品が NP 完全の問題の一つである数独を解くプログラムになっていますが, この作品は見た目も面白くて確かにこれには負けるなぁという感じです.

で,その SAT 問題を解くプログラムは SAT ソルバと呼ばれ,さまざまな分野に応用されています (元々は 定理の自動証明が目的 だったようです). その求解速度を競う SAT Competition という世界大会が毎年開催されています. 今回提出した作品のこだわりの 1 つは,この世界大会にも参加できるような入出力仕様に則って作成したところです. もちろん,性能的には既存のプログラムに太刀打ちできるものではありませんが….

入力は連言標準形 (CNF) という「論理和の内側には論理積が現れない形」の論理式に限定されていて, SAT Competition では以下のような DIMACS CNF 形式で与えられます:

c
c This is a sample input file.
c
p cnf 3 5
 1 -2  3 0
-1  2 0
-2 -3 0
 1  2 -3 0
 1  3 0
この入力は,論理式
(L1 ∨ ¬L2 ∨ L3) ∧ (¬L1 ∨ L2) ∧ (¬L2 ∨ ¬L3) ∧ (L1 ∨ L2 ∨ ¬L3) ∧ (L1 ∨ L3)
に相当します. c で始まる行はコメントで,p cnf 3 5変数が 3 つ, 論理和で繋げられた式 (以下,節とよぶ) が 5 つであることを表します. 0 は節の終わり,1 以上の整数変数- は否定を表します. この論理式を真にする真偽値割当ては,L1=真,L2=真,L3=偽なので,
s SATISFIABLE
v 1 2 -3
を出力することが,SATソルバに求められていることです. 複数の解がある場合はそのうちの 1 つを出力するだけでかまいません. 解が存在しない場合は,
s UNSATISFIABLE
と出力します. 既存の SAT ソルバの中には,minisat や nanosat や picosat というそのプログラムの小ささも売りにしたものがありますが, 今回 TRICK に提出した作品は外部ライブラリも一切使わず 194 バイトという大きさで実現することに成功しました. 名付けて yoctosat といったところでしょうか.

さて,その SAT ソルバは以下の一行プログラムで, DIMACS CNF 形式の文書をそのまま(拡張された)正規表現へ変換することで実現しています:

_='s %sSATISFIABLE';puts eval$<.read.gsub(/.*p.*?(\d+).*?$|\d+/m){$1?%w[?-* +'=-'=~/#{'(-?)'* }-*=(?=]*$1:$&>?0?"\\#$&$|":'$)(?='}+')/x?[_%p%i=0,[*$~].map{|x|x>?-?:v:eval(x+?1)*i-=1}*" "]:_%:UN'
具体的には,上の入力例に対しては以下のような Ruby プログラムが生成されます:
  '-'*3+'=-' =~ 
  /#{'(-?)'*3}-*=(?=
   \1$| -\2$|  \3$| $)(?=
  -\1$|  \2$| $)(?=
  -\2$| -\3$| $)(?=
   \1$|  \2$| -\3$| $)(?=
   \1$|  \3$| $)(?=
  )/x
=~ の左辺の文字列は,---=-変数の個数分の -=- から成ります. 右辺の正規表現(-?)(-?)(-?)-*= で始まっているため, 後方参照として使用される \1, \2, \3 はそれぞれ - か空文字列のどちらかを表すことになり,それが変数の真偽値割当てに対応します. それに続く正規表現は,左辺の残りの - (ハイフン) 1 文字にマッチしなければいけません. (?=\1$|-\2$|\3$) がマッチするには,
  • \1-
  • \2が 空文字列
  • \3-
のいずれかが成り立っている必要があります. これは,L1∨¬L2∨L3 が真となるためには,
  • L1 が真
  • L2 が偽
  • L3 が真
のいずれかが成り立つ必要があることに対応します. DIMACS CNF 形式の変数名が数値であることや否定が - で表現されていることをうまく利用して, 正規表現への変換を簡単にしています. また,上の正規表現には x フラグが付いているために空白や改行が無視されることもポイントです. 各節の最後にある |$ はあってもなくても結果は変わりませんが, 正規表現への変換を簡単にするために追加されています. さらに,(?=...)は先読み正規表現でマッチした文字列を消費しないため, それ以降のすべての (?=...)- にマッチする必要があります. これは,すべての節が真になるような真偽値割当てを見つけなければならないことと一致するわけです. なお,このアイデアは Abigailさんによる Perl での正規表現 を元にしていますが, DIMACS CNF 形式に合わせるための工夫や先読み正規表現を利用している点が異なります. 今回の Ruby による SAT ソルバはコードの短縮が主な目的なので,このような細かい工夫が必要でした. 他のゴルファーと力を合わせればきっともっと短いコードが実現できたかもしれませんが, 私には 194 バイトが限界でした.

この作品は「役に立ってはいけない」という TRICK が満たすべき条件に反しているのではないかと不安だったのですが, 実際のところあまり役に立ちません. 理由が 2 つあります. 1 つは Ruby正規表現における制約です. 変数が 200 個を超える場合,正規表現\200 のような後方参照が必要になりますが, Ruby ではこの正規表現\200 という 1 文字にマッチしてしまいます. ただし,3 桁でも 8 以上の数字が混じっている場合には後方参照として機能します. これは \ddd が 1 文字と認識されるのは ddd が 8 進数で 3 桁の数値だけであるためです. ちなみに,最初の桁が 1 の場合にも後方参照として機能するようです. 詳細は remarks.markdown をご覧ください. もう 1 つの理由は,変数が 30 個くらいになっただけで現実的な時間で解が求まらないという致命的な点です. こちらの方が実用的な SAT ソルバとしては問題ですね. つまり,変数が 3 桁以上で問題になるような上述の制約についてそもそも気にする必要はなかったわけです. 全然役に立たない SAT ソルバを作ってしまってすみません. ところで,上の制約って Ruby の仕様として知られていることなんでしょうか…?

第 2 位 コラッツ列生成プログラム

コラッツの予想とは,どんな非負整数も HOTPO 操作を繰り返すといずれ 1 にたどりつくというものです. HOTPO は Half-Or-Triple-Plus-One の略で,「偶数なら半分にする,奇数なら 3 倍して 1 を足す」という操作のことです. その昔,ポカリスエットのホットで Hot Po という商品がありましたが,それとは全く関係ありません. 260 ぐらいまでの整数に対しては正しいことが計算によって確かめられているそうですが, 現在も未解決の問題の 1 つです.角谷問題とか,シラキュース問題とか,いろんな名前がついている有名な問題です. 3 から始めると,

3 → 10 → 5 → 16 → 8 → 4 → 2 → 1
27 から始めると,
27 → 82 → 41 → 124 → 62 → 31 → 94 → 47 → 142 → 71 → 214 → 107 → 322 → 161 → 484 → 242 → 121 → 364 → 182 → 91 → 274 → 137 → 412 → 206 → 103 → 310 → 155 → 466 → 233 → 700 → 350 → 175 → 526 → 263 → 790 → 395 → 1186 → 593 → 1780 → 890 → 445 → 1336 → 668 → 334 → 167 → 502 → 251 → 754 → 377 → 1132 → 566 → 283 → 850 → 425 → 1276 → 638 → 319 → 958 → 479 → 1438 → 719 → 2158 → 1079 → 3238 → 1619 → 4858 → 2429 → 7288 → 3644 → 1822 → 911 → 2734 → 1367 → 4102 → 2051 → 6154 → 3077 → 9232 → 4616 → 2308 → 1154 → 577 → 1732 → 866 → 433 → 1300 → 650 → 325 → 976 → 488 → 244 → 122 → 61 → 184 → 92 → 46 → 23 → 70 → 35 → 106 → 53 → 160 → 80 → 40 → 20 → 10 → 5 → 16 → 8 → 4 → 2 → 1
このように HOTPO 操作を繰り返して得られる数列はコラッツ列と呼ばれ, 予想の付かない数列で 1 にたどりつくことから,プログラミング教育の現場でも while 文の練習として使われることもあるようです. Ruby の場合 (教科書的に書くなら)
x = ARGV[0].to_i
puts x
while x > 1
  if x % 2 == 0 then
    x = x / 2
  else
    x = 3 * x + 1
  end
  puts x
end
となりますが,今回 TRICK に提出したプログラムはこれと同等のものです.

実際に提出したプログラムがこちらです:

%%%while eval '_=%%r%%(.)...\1=%%=~[%%%%,,,,,%%%s  ?=]*%%%%%%#"]*%%%%3x+1?%%'.% %%",%*p(_||=eval($**%%%))
何が評価されたか本当のところは審査員の皆様に尋ねてみないと分かりませんが, 算術演算を一切使わずに文字列処理によって HOTPO 操作を実現したところでしょうか. % がやたらと多いですが, これは文字列リテラル正規表現リテラル% 記法 (%%...%%r%...%) を多用しているためです. 慣れれば読むことは難しくありません (たぶん). このプログラムを作成する際,
この % 記法% 演算子を列べれば % だけからなる式が作れるんではないだろうか…? しかも,% の個数が 4 * k + 3 のときだけ意味のある式になる! これは大発見だ! TRICK に使えるかも!
などと浮かれていたのですが,いろいろ調べてみたらそんなことは既に知られていて前回の TRICK に使われていたようです. TRICK の投稿規定にも過去の入賞作品をよく調べろって書いてありましたね. 危うく二番煎じとなるところでした. と,話が逸れましたが,上述のプログラムの基本的なアイデアは 「ある文字列を偶数回繰り返すのと奇数回繰り返すのとでは意味の違う式を作る」 というもので,その「ある文字列」というのが ", です. 具体的には,「n が偶数なら半分に,奇数なら 3*n+1 に」という HOTPO 操作を,
n = (/(.)...\1=/ =~ eval('[",,,,,"'+ '",'*n + '  ?=].join#"].join("3x+1?")'))
という式で実現しています (上のプログラムはこれを読みにくくしたものです). eval 式で生成された文字列に対して正規表現 /(.)...\1=/ でマッチングを行い, マッチした位置が n に代入されます. " が偶数個か奇数個かによって最後の " が文字列の終了を表すか開始を表すかという意味が変わるため, この結果 eval 式が返す文字列が変わるというカラクリです. n が偶数のときは,上の eval 式の引数
'[",,,,,"'+ '",' + '",' + '",' + ... + '",' + '  ?=].join#...''[",,,,,"",",",...",  ?=].join#...'
と評価され,最後の " は文字列の終了を表します. ここで,",,,,,""," の部分に違和感を感じる方がいらっしゃるかもしれません. 私もこのプログラムを作成する前は知らなかったのですが, Ruby ではダブルクオートやシングルクオートによる文字列リテラルを列べて書いてもよいようで, "ab""cd""abcd" と同等だそうです. したがって,",,,,,"","",,,,,," を表します. join の後ろの #以降はコメントとして eval の際には無視されます. ",n 個連結すると ",", が n/2 個続くことになるので, 上の式の評価結果は ",,,,,...,=" となります. 先頭の ",,,,," を含めると , の個数は 5 + n/2 となり, 正規表現 /(.)...\1=/ がマッチするのは末尾の ,,,,,= ですので, その位置は n/2 番めとなるわけです.

n が奇数のときはどうでしょう. eval 式の引数

'[",,,,,"'+ '",' + '",' + '",' + '",' + ... + '",' + '  ?=].join#"].join("3x+1?")''[",,,,,"",",",",...,",  ?=].join#"].join("3x+1?")'
と評価され,最後の ", は文字列の開始になるため, ...join#" までの文字列が配列の最後の要素になります. この文字列の配列を 3x+1? という文字列を結合するので,最終的には
",,,,,,3x+1?,3x+1?,...,3x+1?,  ?=].join#"
という文字列になります. 配列の要素は (n+1)/2 個なので,eval によって間に3x+1? が (n-1)/2 個入った文字列が得られます. この文字列に,正規表現 /(.)...\1=/ がマッチするのは末尾の方にある ?, ?= であり, その前には先頭の ,,,,,, が (n+1)/2 個と 3x+1? が (n-1)/2 個 (このうち最後の1個の末尾の ? はマッチの開始位置) あるので, マッチする位置は 5+(n+1)/2+(n-1)/2*5-1 = 3*n+1 となるわけです. ただし,これは n が 3 以上の奇数の場合です. n = 1 のときは配列の要素が 1 つであり 3x+1? が入らないため, 正規表現 /(.)...\1=/ にはマッチしません. その結果,n が nil となり while 文が終了するわけです.

ここまでの説明を呼んでお気づきになった方もいらっしゃると思いますが, このプログラムに出てくる 3x+1 は基本的にはどんな文字列でもかまいません (= が含まれるとややこしくなりますが). 今回の作品で 3x+1 という文字列を選んだのは,コラッツ予想が 3x+1 問題とも呼ばれるためです. 実はここに自分のハンドル名でも入れようとか思っていたのですが,投稿規定に反するということでやめました (この規定に反してしまった人(主催者?)もいたようですが…).

おわりに

説明を書いてみたら remarks.markdown とほとんど同じことを書いてしまった気がします. 日本語で読む人も多いと思いますので,一応意味はあるのかもしれません. もちろん TRICK の性質上,こんなものを読んでも何も得られないわけで,意味なんてないはずですが,話のネタにでもなれば幸いです. 今回初めての参加でしたが,次回もネタがあれば参加してみたいですね. 何としても 3 連覇は阻止しないといけませんから.

2013年12月25日

[] 推移律はいらない? ─比較ソートの正当性に必要な比較関数の性質─

この記事は Theorem Prover Advent Calendar 2013 最終日 (25日目)*1の記事です. 元々このネタは, 後学期の3年生向けの実験でCoqを教える際に提示した 「挿入ソートの正当性を示す」という最終課題の模範解答を作成する際に気づいたことです. このため,ここで紹介するプログラムや証明は, タクティクの種類やライブラリの利用が必要最低限に絞られているので, もしかしたら Coq 初心者の方にも参考になるかもしれません (各タクティクの作用を明確に理解してもらうため,敢えて auto も使いませんでした). Coq 上級者には冗長な証明が気になるかもしれませんが,その点は予めご了承ください.

はじめに

比較関数を利用して整列するアルゴリズムは比較ソートと呼ばれ, クイックソートマージソートをはじめとする多くの整列アルゴリズムがこれに属します (逆に比較ソートでない整列アルゴリズムとしては,基数ソートやバケツソートなどがあります). 比較関数は「2つの要素を引数を取り,真偽値 (true または false) を返す関数」として与えたり, 「2つの要素を引数を取り,比較値 (LessThan, EqualTo, GreaterThan) を返す関数」として与えたりしますが, この記事では簡単のため前者を扱うことにします. 具体的には,ここでの比較関数は第1要素が第2要素より真に大きければ真, 第1要素が第2要素と等しいか小さければ偽を返すものとし, 比較ソートは入力を昇順に整列したものを出力することを想定しています.

比較ソートは,比較関数を入れ替えることで様々な指標で整列させることができるという反面, 与える比較関数が正しくないとそのアルゴリズムは意味を成しません. 例えば,どんな2つの要素を受け取っても必ず真を返すという関数を比較関数とすると, どんな比較ソートでも正しく整列してくれません. 整列アルゴリズムは,整列する要素の順序関係が強全順序を成すことを前提としています*2. つまり,比較関数 cmp

  • (1) [決定可能性] 全ての要素 a, b に対して,(cmp a b = true) ∨ (cmp a b = false)
  • (2) [非反射律] 全ての要素 a に対して,cmp a a = false
  • (3) [推移律] 全ての要素 a, b, c に対して,(cmp a b = true) ∧ (cmp b c = true) ならば cmp a c = true
を満たしていることが必要であると考えられます. (1) は強全順序の定義以前の問題ですが,比較関数の計算が停止しない場合を排除するための条件です. ちなみに,(1), (2), (3) から
  • (4) [非対称律] 全ての要素 a, b に対して,cmp a b = true ならば cmp b a = false
が導けますが,「挿入ソートの正当性は (1) と (4) だけで証明ができてしまう???」というのがこの記事の主題です. 一般には,(1), (4) だけでは (3) が成り立つとは限らないのですが,後に示すように挿入ソートの正当性の証明には不要です. また,(2) は (1), (4) から簡単に導けます. つまり,挿入ソートが正当な結果を返すことを確認するためには, 与える比較関数について (2) や (3) は考えなくてよいということになりますが, これはどういうことでしょうか.

Coqによる定式化

まずは簡単な準備から.

(* List ライブラリをインポート. 使うライブラリはこれだけ. *)
Require Import List.
(* 要素の型を A に固定. *)
Parameter A : Set.
(* 比較関数 cmp を宣言. 2つの要素を引数に取って真偽値を返すので,A -> A -> bool 型 . *)
Parameter cmp : A -> A -> bool.

Coq では,この cmp に関する宣言だけで (1) の決定可能性を仮定したことになります. これは bool 型が帰納的に定義されているためで,実際に (1) を証明することも可能です.

(* cmp の決定可能性 *)
Lemma cmp_dec :
  forall (x y:A), cmp x y = true \/ cmp x y = false.
Proof.
intros x y.
destruct (cmp x y); [left|right]; reflexivity.
Qed.

さらに,(4) に相当する cmp に関する非対称律を仮定します.

(* 非対称律を仮定 *)
Parameter cmp_asym :
  forall (x y:A), cmp x y = true -> cmp y x = false.

(1) と (4) だけで正当性を証明すると言う目的のため,(2) と (3) は仮定しません.

さて,挿入ソートを定義しましょう. まず,既に整列されているリストに要素を1つ挿入する関数 insert を定義してから, 挿入ソートを行う主たる関数 insertion_sort を実装します. 幸いにしてどちらもリスト上の単純な再帰関数で定義できるので, 整礎性の問題に苦しむこと無く簡単に定義することができます (これは講義でこの問題を採用した大きな理由の一つです). cmp x y を x > y と読み替えて, 昇順に列べる整列をイメージすれば読みやすいと思います.

(* 1つの要素を挿入する関数 *)
Fixpoint insert (x:A) (xs:list A) :=
  match xs with
    | nil => x :: nil
    | y :: ys =>
      if cmp x y then y :: insert x ys
                 else x :: y :: ys
  end.
(* 挿入ソート関数 *)
Fixpoint insertion_sort (xs:list A) : list A :=
  match xs with
    | nil => nil
    | y :: ys => insert y (insertion_sort ys)
  end.

さらに,整列アルゴリズムが正しいことを示す性質を定義しておきましょう. まず,順序よく列んでいることを表す述語 Sorted を定義します.

(* Sorted xs := リスト xs が昇順に整列されている *)
Inductive Sorted : list A -> Prop :=
| Sorted_nil : Sorted nil
| Sorted_singleton : forall x:A, Sorted (x :: nil)
| Sorted_conscons : forall (x y:A) (xs:list A),
  cmp x y = false -> Sorted (y :: xs) -> Sorted (x :: y :: xs).

ここでも,cmp x y を x > y と読み替える,すなわち cmp x y=false を x ≦ y と読み替えれば理解しやすいでしょう. 整列アルゴリズムが正しいことを示すためには,Sorted だけでは不十分です. たとえば,どんなリストが入力されても空リストを返す関数を考えると, この関数は常に整列されたリストを返しますが,正しく整列したとは言えません. 出力されたリストが入力されたリストの並べ替えであるということを示す必要があります. そこで,2つのリストが互いに並べ替えであることを表す述語 Permutation を定義します (同等のものが Coq の Sorting ライブラリにもあります).

(* Permutation xs1 xs2 := 2つのリスト xs1 と xs2 が互いに並べ替えの関係である *)
Inductive Permutation : list A -> list A -> Prop :=
| Perm_nil : Permutation nil nil
| Perm_skip : 
  forall (x:A) (xs ys:list A),
    Permutation xs ys -> Permutation (x :: xs) (x :: ys)
| Perm_swap : 
  forall (x y:A) (xs:list A),
    Permutation (x :: y :: xs) (y :: x :: xs)
| Perm_trans : 
  forall (xs ys zs:list A),
    Permutation xs ys -> Permutation ys zs -> Permutation xs zs.

これで準備が完了です.

挿入ソートの正当性の証明

ここからが証明のお話です. まず,証明したい定理を先に見ておきましょう.

(* insertion_sort の正当性 *)
Theorem insertion_sort_correctness :
  forall xs:list A,  Sorted (insertion_sort xs) /\ Permutation xs (insertion_sort xs).

任意のリストに対して,insertion_sortSorted なリストを返し, 元のリストと Permutation の関係になっていることを表しています. まず,補助関数である insert について, Sorted に関わる性質を証明します.

(* 整列されているリストであればどんな要素を挿入しても整列される *)
Lemma insert_sorted :
  forall (x:A) (xs:list A), Sorted xs -> Sorted (insert x xs).
Proof.
intros x xs Hxs.
induction Hxs.
(* Sorted_nil *) constructor.
(* Sorted_singleton *) simpl.
  destruct (cmp_dec x x0) as [Hcmp1|Hcmp1]; rewrite Hcmp1.
  (* cmp x x0 = true *)
    apply cmp_asym in Hcmp1. constructor; [assumption|constructor].
  (* cmp x x0 = false *) constructor; [assumption|constructor].
(* Sorted_conscons *) simpl in *.
  destruct (cmp_dec x x0) as [Hcmp1|Hcmp1]; rewrite Hcmp1.
  (* cmp x x0 = true *) 
    apply cmp_asym in Hcmp1.
    destruct (cmp_dec x y) as [Hcmp2|Hcmp2]; rewrite Hcmp2 in *.
    (* cmp x y = true *) constructor; assumption.
    (* cmp x y = false *) constructor; [|constructor]; assumption.
  (* cmp x x0 = false *)
  constructor; [|constructor]; assumption.
Qed.

また,Permutation に関わる性質を証明します.

(* 先頭に要素を追加したものと insert関数により要素を挿入したものは並べ替えの関係になっている *)
Lemma insert_perm :
  forall (x:A) (xs:list A), Permutation (x :: xs) (insert x xs).
Proof.
intros x xs; induction xs; simpl.
(* nil *)
  constructor; constructor.
(* cons *)
  destruct (cmp_dec x a) as [Hcmp1|Hcmp1]; rewrite Hcmp1 in *.
  (* cmp x a = true *)
    apply Perm_trans with (a :: x :: xs);
      [constructor|constructor;assumption].
  (* cmp x a = false *)
    clear.
    constructor; constructor.
    induction xs.
    (* nil *) constructor.
    (* cons *) constructor; assumption.
Qed.

これらの insert 関数の性質を使えば, insertion_sort も簡単な帰納法で証明することができます.

(* 挿入ソートの正当性 *)
Theorem insertion_sort_correctness :
  forall xs:list A,
    Sorted (insertion_sort xs) /\ Permutation xs (insertion_sort xs).
Proof.
induction xs.
(* nil *) simpl; split; constructor.
(* cons *) simpl; split; destruct IHxs.
  (* Sorted *) apply insert_sorted, H.
  (* Permutation *) apply Perm_trans with (a :: insertion_sort xs).
    constructor; assumption.
    apply insert_perm.
Qed.

これで証明が終わりです. 着目してほしいのは, 「挿入ソートの正当性を示すこの証明に使われている仮定は (1) と (4) だけで, (2) と (3) は仮定していない」という点です. このことから,比較関数に必要な性質として (3) の推移律はいらないのではないかという疑いが生じます. しかし,推移律が成り立たないじゃんけんのような3者関係があれば整列できないことは明らかです. それでは,比較関数が推移律を満たすことを仮定せずに挿入ソートの正当性が証明できてしまったことは何を意味しているのでしょうか.

種明かし

ここで,種明かしです. 「比較関数は推移律を満たさなくてもよい」と結論付けるには2つの問題があります. 1つめの問題は,隣り合った要素が順序通り列んでいればよいという Soreted の定義に関連します. 「(2) と (3) は一切使っていない」というのは真実ですが,これは Sorted の定義に強く依存します. ここで使った定義は Coq の Sorting ライブラリにおける LocallySorted に相当していて, 隣り合った要素だけを見て整列しているかどうかを判定していますが, 「整列されている」という述語の定義は他にも考えられます. たとえば,リストのどの2つの要素も順序通り列んでいるという定義 (Sorting ライブラリStronglySorted に相当するもの) を考えてみましょう.

(* CmpAll x ys := リスト ys のどの要素 y に対しても cmp x y = false (x≦y) が成り立つ. *)
Inductive CmpAll : A -> list A -> Prop :=
| CmpAll_nil : forall x:A, CmpAll x nil
| CmpAll_cons : forall (x y:A) (ys:list A),
  cmp x y = false -> CmpAll x ys -> CmpAll x (y::ys).

(* StronglySorted xs := リスト xs のどの2つの要素についても x が y より前に現れるなら cmp x y = false が成り立つ. *)
Inductive StronglySorted : list A -> Prop :=
| StronglySorted_nil : StronglySorted nil
| StronglySorted_cons : forall (x:A) (xs:list A),
  CmpAll x xs -> StronglySorted xs -> StronglySorted (x :: xs).

どんなリスト xs に対しても,明らかに StronglySorted xs ならば Sorted xs が導けますが, 逆は成り立ちません. 逆を示すためには,(3) に似た否定推移律 (3)' が必要になります*3

  • (3)' [否定推移律] 全ての要素 a, b, c に対して,(cmp a b = false) ∧ (cmp b c = false) ならば cmp a c = false
実際, 「整列されている」という述語として StronglySorted を選んでしまうと, 挿入ソートの正当性を示すためには (3)' が必要になってしまいます. つまり,「隣り合った要素の順序しか確認しなくてよい」という定義をした時点で,推移律の仮定を使っているわけです.

2つめの問題も Sorted の定義に関連することですが, 「比較関数が推移律を満たすことを確認しなくてよい」と結論づけてはいけないことを示すより根本的な問題です. 比較関数 cmp そのものを Sorted の定義の一部に使ってしまっては, 比較関数の正しさに関して何も論じられないのです. たとえば,S, T, U の 3種類しかないデータを要素とするリストの整列を考えてみましょう. 比較関数 cmp の定義を

Definition cmp (x y:A) := match (x, y) with
  | (S, T) => true
  | (T, U) => true
  | (_, _) => false
end.
とすると,この定義は (4) を満たしますが,(3) や (3)' は満たしません. この比較関数を基準に整列すると, S::U::T::nilU::T::S::nilT::S::U::nilS::U::T::nil になり得ますが, S::T::nilT::S::nil にしかなりません. つまり,U があるかないかで順序が変わってしまうような妙な結果が得られます. 非対称律が成り立っていても,推移律が成り立っていなければ整列として意味をなさないのです.

おわりに

結果的には「比較関数は推移律を満たさなくてもよい」というのは正しくありませんでしたが, 整列するアルゴリズムの正当性を示すには比較関数の推移律を必要としないというのは面白い結果ではないでしょうか. 実際,クイックソートマージソートなどの別の比較ソートのアルゴリズムの場合も (4) だけで正当性が証明できます. 今回は,挿入ソート・クイックソートマージソートについてしか確認していませんが, 上述のような Sorted の定義を考えている限り,推移律は必要にはならないような気がします. では,比較関数の推移律を仮定しないと正当性が示せないような比較ソートアルゴリズムが存在しないことは証明できるでしょうか. これは,あまり簡単ではないかもしれませんね.

*1:Advent Calendarって本来は24日で終わりではないのかという話もありますがここでは気にしないことにします.

*2:弱全順序を前提としてもかまいませんが,弱全順序を考えると反対称律を考慮する必要があり,要素の等価性の扱いなどの議論が面倒になるので,ここでは強全順序を仮定しています. 弱全順序を考える場合に同様の議論をすると,「反射律は不要であるが,「完全性 (cmp a b = true または cmp b a = true)」が必要になることになります.

*3: 実は (3)' と (4) から (3) が導けます.

2012年05月25日

[] 8.2 と 8.3 の互換性

久しぶりに Coq を触ったら, 昔書いた Coq のソースプログラムが通らなくなっていました. いろいろ原因を探ってみたところ, Coq 8.2 と Coq 8.3 で, 証明の開始時点での goal の形式が変わったためのようです. たとえば,

Theorem eq_diff_0 (n m: nat) : n = m -> n - m = 0.
という定理を証明しようとすると,8.2 では
============================
   forall n m : nat, n = m -> n - m = 0
で開始されますが,8.3 では
   n : nat
   m : nat
============================
   n = m -> n - m = 0
で開始されてしまいます.

互換性に関する公式の情報によると, -compat 8.2 というオプションを追加すると動作するらしいのですが, 新しいプログラムに混ぜて再利用するときには不都合なので, とりあえず,

Ltac gen_clear := repeat (match goal with [x:_|-_] => generalize x; clear x end).
という tactic を定義して, 動作しなくなった全ての証明の始めのところに gen_clear を追加することで解決できました. こういう仕様変更って,ユーザは困らないのかなぁ….