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 という商品がありましたが，それとは全く関係ありません． 2⁶⁰ ぐらいまでの整数に対しては正しいことが計算によって確かめられているそうですが， 現在も未解決の問題の 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 連覇は阻止しないといけませんから．

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

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

はじめに

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

比較ソートは，比較関数を入れ替えることで様々な指標で整列させることができるという反面， 与える比較関数が正しくないとそのアルゴリズムは意味を成しません． 例えば，どんな2つの要素を受け取っても必ず真を返すという関数を比較関数とすると， どんな比較ソートでも正しく整列してくれません． 整列アルゴリズムは，整列する要素の順序関係が強全順序を成すことを前提としています((弱全順序を前提としてもかまいませんが，弱全順序を考えると反対称律を考慮する必要があり，要素の等価性の扱いなどの議論が面倒になるので，ここでは強全順序を仮定しています． 弱全順序を考える場合に同様の議論をすると，「反射律は不要であるが，「完全性 (cmp a b = true または cmp b a = true)」が必要になることになります．))． つまり，比較関数 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_sort は Sorted なリストを返し， 元のリストと 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)' が必要になります*2．

• (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::nil は U::T::S::nil や T::S::U::nil や S::U::T::nil になり得ますが， S::T::nil は T::S::nil にしかなりません． つまり，U があるかないかで順序が変わってしまうような妙な結果が得られます． 非対称律が成り立っていても，推移律が成り立っていなければ整列として意味をなさないのです．

おわりに

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

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

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

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 を追加することで解決できました． こういう仕様変更って，ユーザは困らないのかなぁ…．

あけましておめでとうございます．

今年もアンビグラムというほどのものではありませんが， それに近いものを作成してみました． これまでのもの ( 2008年 / 2009年 / 2010年 ) に比べるとわかりやすすぎますね． 昨年は全く更新しないという体たらくでしたが， 今年はこれで少なくとも一回は更新できました． 今年もよろしくお願い致します．

クワインとフェルマーの最終定理

(更新を滞るとずっと侵略されているように見えてしまうので，むりヤリ記事をひねり出すことにしました)

さて，今年も 12 月 25 日が近づいてまいりました．皆さんご存知の「ク」で始まるあの日です． そう，クワイン (W. V. Quine) の命日ですね． ということで，今回はクワインの話です．プログラミングを嗜む人であれば，クワインというと，

を二度書け！ を二度書け！

のような「実行すると自分自身を出力するプログラム」を思い浮かべますが， 今回はそういう話ではありません． 彼が残した短い記事を紹介します． といってもだいぶアレンジしているので，興味のある人は元の文献 *1 を読んでください．

もうすぐお正月．初詣ではおみくじでその年の運勢を占ったりしますが， みくじ棒の入った筒を振って出た数字から大吉やら凶やらが書かれた紙と交換することがあります． みくじ棒を再利用できるように中から出ないようになっているものもありますね． 今回考える問題は，そんな「再利用できるみくじ棒の入った筒」に関するものです． 簡単のため，数字ではなくて大吉や凶が直接書かれたみくじ棒を想像してください．

問題

大吉，吉，凶の 3 種類のみくじ棒が入った筒があります． 3 回以上このおみくじを引くとき， 「大吉と吉が両方 (1回以上) 出る確率」と「凶しか出ない確率」が等しくなるためには， どんな割合で大吉，吉，凶を入れて，何回引けばよいでしょうか？

2 回しか引かないのなら，大吉 1 本，吉 2 本，凶 2 本 入れれば， 大吉と吉が出る確率が 1/5 × 2/5 + 2/5 × 1/5 = 4/25， 凶しか出ない確率が 2/5 × 2/5 = 4/25 なので等しくなります． 3 回以上の場合はどうでしょう？

*1: W. V. Quine, "Fermat's Last Theorem in Combinatorial Form", American Mathematical Monthly, Vol.95, no. 7 (August-September 1988), p.636. 元の記事では，青い瓶と赤い瓶と無色の瓶に n 個のボールを入れる組み合わせの数として書かれています．今回の記事ではなるべくイメージをしやすいように書き換えました．

3 進数を侵略しようではなイカ

この記事は Functional Ikamusume Advent Calendar jp 2010 によって侵略されたでゲソ．

2 進数の国の関数型イカ娘 *1 が 3 進数を侵略するという話をしようではなイカ．

イカの国にはメスとオスがいるでゲソ． イカのメスとオスは，胴の斑点が丸状か線状かで見分けられるから， メスは =0> ，オスは =1> と書こうではなイカ．

メスは戦闘タイプで，オスはとても弱いでゲソ． たとえば，3 進数のキャラ 0, 1, 2 ( 0 が一番弱くて 2 が一番強い) が現れたら，

• メスは強いので相手を 1 つ弱くするでゲソ ( 0 はそのまま )．
• オスはバカなので相手を 1 つ強くしてしまうでゲソ ( 2 はそのまま )．

というルールで戦闘するでゲソ． でも，戦闘相手が 1 の時は我々は性転換してしまうという特徴があるでゲソ． そして，一度闘った相手は背後に回るので，後続の仲間に闘ってもらうでゲソ． つまり，我々が左から右に攻めるとするなら，イカのようなルールで闘うことになるのではなイカ？

1. =0> 0 なら，0 =0> ( 0 なのでそのままではなイカ．相手は背後 (左) に回るでゲソ．)
2. =0> 1 なら，0 =1> ( 1 なので 1 つ弱くして 0 にするけど，性転換してオスになるでゲソ．)
3. =0> 2 なら，1 =0> ( 2 なので 1 つ弱くして 1 にするでゲソ．)
4. =1> 0 なら，1 =1> ( 0 なので 1 つ強くして 2 にするでゲソ．)
5. =1> 1 なら，2 =0> ( 1 なので 1 つ強くして 2 にするけど，性転換してメスになるでゲソ．)
6. =1> 2 なら，2 =1> ( 2 なのでそのままではなイカ．)

0 は無害だから，3 進数のキャラを全部 0 にしたら侵略成功でゲソ． でも，やっぱりオスはバカだから相手が 0 でも目の前にいたら闘ってしまって，相手を強くしてしまうでゲソ． だから，なるべくメスが闘うことにしようではなイカ．

何言ってるか分からなイカもしれなイカら，実際に 1102 という 3 進数を侵略してみるでゲソ．

まずメスが闘うでゲソ．
=0> 1 1 0 2
上のルールに従って闘うでゲソ．
0 =1> 1 0 2
目の前の相手にダメージを与えたけど，相手が 1 なのでオスになったではなイカ．
バカなオスが闘うでゲソ．
0 2 =0> 0 2
相手を強くしてしまったではなイカ．でも相手が 1 だったのでメスになったでゲソ．
背後に回った敵は後続の仲間が闘ってくれるでゲソ．いないときはメスが出てきてくれるでゲソ．
=0> 0 2 =0> 0 2
それぞれのイカが闘うでゲソ．
0 =0> 2 0 =0> 2
0 1 =0> 0 1 =0>
1 が背後に回ってしまったのでメスをつイカ．
それぞれ闘うでゲソ．
=0> 0 1 =0> 0 1 =0>
0 =0> 1 0 =0> 1 =0>
0 0 =1> 0 0 =1> =0>
0 0 1 =1> 0 =1> =0>
せっかく全部 0 にしたのに，バカなオスが目の前の 0 を 1 にしてしまったではなイカ．
1 が背後に回ってしまったのでメスをつイカして闘いを続けるでゲソ．
=0> 0 0 1 =1> 0 =1> =0>
0 =0> 0 1 1 =1> =1> =0>
0 0 =0> 1 1 =1> =1> =0>
0 0 0 =1> 1 =1> =1> =0>
0 0 0 2 =0> =1> =1> =0>
オスが相手を 2 にしてしまったでゲソ．メスをつイカして闘うでゲソ．
=0> 0 0 0 2 =0> =1> =1> =0>
0 =0> 0 0 2 =0> =1> =1> =0>
0 0 =0> 0 2 =0> =1> =1> =0>
0 0 0 =0> 2 =0> =1> =1> =0>
0 0 0 1 =0> =0> =1> =1> =0>
1 が背後に回ってしまったのでメスをつイカ．
=0> 0 0 0 1 =0> =0> =1> =1> =0>
0 =0> 0 0 1 =0> =0> =1> =1> =0>
0 0 =0> 0 1 =0> =0> =1> =1> =0>
0 0 0 =0> 1 =0> =0> =1> =1> =0>
0 0 0 0 =1> =0> =0> =1> =1> =0>

これ以上メスをつイカしても 0 以外は増えなイカら，これで侵略成功でゲソ． 戦闘を終えてみたら我々は 1 0 0 1 1 0 と列んでいるでゲソ． これは 3 進数の 1102 の 2 進表記ではなイカ！ イカなる 3 進数と闘っても同じことが言えるでゲソ！

どこが関数型なのかってのは，戦闘ルールの適用の仕方にあるでゲソ． それぞれのイカがイカなる順序で目の前の敵と闘っても同じ結果になることが分からなイカ？ たとえば，先頭のイカが相手がいなくなるまで先に闘っても， 後ろのイカが先に闘っても，上の例のように同時に闘っても， 結果は同じになるのでゲソ． 評価順序によらなイカら関数型ではなイカ (むりヤリ)！ m 進数の国のイカが n 進数を侵略するときも同じようにルールを作れることが既に分かっているでゲソ．

余談だけど 3 進数の後ろに X というキャラが次から次へ追加されるような戦闘だと面白いことが分かるでゲソ． 相手が X の場合，メスでは太刀打ちできないが， オスなら何故か 2 に変更させることができて，自分はメスになるでゲソ． つまり，イカのルールがつイカされることになるのではなイカ．

1. =0> X なら，X =0>
2. =1> X なら，2 =0>

このルールで闘うと，イカなる 3 進数でも 1 と 2 が 1 つずつ残って，オスが一匹だけいる形にたどり着くのではなイカ？ この問題は，人間界では 3n+1 問題とかコラッツ予想とか角谷予想とかシラキュース予想とか言われているでゲソ． [twitter:@ksknac] の背景に潜んでいるジグソーパズルはそれを図示したものだとかいうではなイカ． たぶん小さすぎて分からないでゲソ．( 12/19 追記 : つイカしたルールに間違いがあったので修正したでゲソ )

*1:実はよくわかっていないので偽物のイカ娘かもしれないでゲソ．取りあえず，語尾にゲソとかイカとかつけて侵略という言葉をちりばめればそれっぽくなると解釈したでゲソ．

OCaml Golf 最速マスター

OCaml Meeting 2010 の 3 日前である本日 14:30 から，OCaml Golf Competition が開催されます．
テクニックの紹介を連載すると言いながら，全然できていなくてすみません．昨年のスライドを修正した内容を掲載します．

ユーザ定義関数・変数は1文字で

これはゴルフでは当たり前ですね．

空白・括弧の省略

バイト数を短くするには，空白の除去は必須です．除去してよいか迷ったときは「とりあえず省略して動かしてみる」というのが原則です．

if i>1then i*2else 6

のように，キーワードの直前の空白は大抵省略可能です．意外な空白も省略できるので，取りあえず消してみましょう．また，括弧についても「取りあえず消してみる」というのが有効です．

;; (ダブルセミコロン) の省略

OCaml では，文と文の間に「;;」というセパレータを入れることがありますが，これは全て省略可能です．

let f x=x+1
let g x=x*2
let()=print_int(f(g 3))

ただし，大抵のプログラムの最後の文は式の実行だけなので let 文でなく式を直書きしますが，この際には「;;」が必要です．

let f x=x+1
let g x=x*2;;print_int(f(g 3))

式同士は「;」で繋ぐので，プログラム全体で「;;」が現れるのは高々 1 回になります．また，式の中で let による束縛が必要になる場合は let ... in を使いましょう．

よく使うモジュールは open

文字列系の問題の場合，String モジュールの関数を何度も利用することがあるかもしれません．関数を2箇所以上使っていたら open するようにしましょう．

let x=... String.make ... String.sub ...

を

open String
let x=... make ... sub ...

とすれば，2Bほど稼げます．ただし，List モジュールなどのように短いモジュール名の場合は open しない方が短いこともあるので注意しましょう．また，ダブルセミコロンが増えたりして短くならない場合もあります．

原則的には if 式は禁止

返り値を必要としない if 式は，& 演算子によって短く書くことができます．

if x>0then print_string"positive"
if x=0then print_char 'O'else print_int x

は，それぞれ

x>0&()=print_string"positive"
x=0&()=print_char 'O'||()=print_int x

と書けます．& 演算子の引数は bool 型なので，unit 型の () と比較することで型を合わせています．else 節には || を使いましょう．

返り値を必要とする場合には bool 型では困るので，このテクニックは使えません．

let rec f x=if x>0then x*f(x-1)else 1;;print_int(f 10)

ただし，返り値を使う側 (上の例では print_int) の部分を関数定義に組み込んでしまえば，if 式が省略できることがあります．

let rec f x y=x>0&f(x-1)(x*y)||()=print_int y;;f 10 1

なお，else 節の部分を実行した後にエラーなどで終了してしまう場合に || が不要になることがあります．

配列を使って

if n mod 2=0then f(n/2)else f(n*3+1)

を

f[|n/2;n*3+1|].(n mod 2)

のように if 式を代用する方法もありますが非常に稀です．ただ，配列の場合は全ての要素が評価されてしまうので，

let rec f n=if n mod 2=0then f(n/2)else n*3+1

という else 節を再帰させたくない場合に，

let rec f n=[|f(n/2);n*3+1|].(n mod 2)

のようには書けないことに注意してください．

let rec は一つで十分

OCaml では相互再帰関数を let rec と and で表現できますが，相互再帰でなくても and で繋いでしまいましょう

let rec f x=...
let rec g x=...
let rec h x=...

なら

let rec f x=...
and g x=...
and h x=...

と書けます．f と g の順序を変えることで短くなることもあります．

let rec f x=...1 and g x=...();;f 3
let rec g x=...()and f x=...1;;f 3

let も節約

let による変数定義短くできる場合があります．

let x=...
let y=...

なら

let x,y=...,...

と書けます．ただし，y が x に依存する場合はこのような変更はできません．

Printf, Scanf の利用

文字列の扱いに弱い (ゴルフ的にコード量が多い) 言語である OCaml において，入出力の際にさまざまな処理ができる Printf, Scanf モジュールが有効です．マニュアルをざっと眺めておくとよいでしょう．

中置演算子のユーザ定義の利用

このテクニックは多くの問題で有効です．OCaml では，一部の記号 (列) を中置演算子として利用することができますが，ゴルフでは重要な機能の一つです．先ほど定義した階乗を計算して表示する関数なら，

let rec($)x y=x>0&x-1$x*y||()=print_int y;;10$1

となり，括弧や空白が省略できて 6B も少なくなります．この例では ($) を使いましたが，(@) や (^) が使われることも多いようです．OCaml では先頭の記号によって優先順位が決まるので，問題ごとに使い分けるとよいと思います．ちなみに，優先順位は高い方から順に以下のようになっています．

! や ~ などの前置演算子 
関数適用     (L)
コンストラクタ
-, -.
**           (R)
*, /, %, mod (L)
+,-          (L)
::           (R)
@, ^         (R)
=, <, >, $   (L)
not
&, &&        (L)
or, ||       (L)
,
<-, :=       (R)
if
;            (R)

L や R は左優先か右優先かを表しますが，ゴルフではこれも重要だったりします．他のところで使わない演算子であれば，(+)だろうと(-)だろうと何でも上書きしてしまいましょう．

また，(!) を使った前置演算子が有効な場合もあります．たとえば

let(!)=Char.chr;;Printf.printf"%c%c%c"!107!115!107

は，

let f=Char.chr;;Printf.printf"%c%c%c"(f 107)(f 115)(f 107)

と比べると，括弧も空白も省略できて大幅にバイト数を減らせることがよくわかります．

なお，前置演算子を 2 引数関数に利用したり，中置演算子を 3 引数関数に利用したりすることで短くなることもあります．

let f x y z=x+y+z;;f 1 2 3
let($)x y z=x+y+z;;(1$2)3

再帰 vs. ループ

OCaml では繰り返しの処理を let rec や for / while ループで表現できますが，原則的には以下のように使い分けができます．

• 記憶する変数が多いときには let rec
• 繰り返し回数が決まっていれば for
• (エラーが出るまで) 無限に繰り返したい場合は while

といった具合です．ただし，これはあくまで「原則」なので，とりあえず試してみて短いものを選ぶのがよいと思います．let rec を使った場合には中置演算子の利用を考慮できることを忘れずに．

また，再帰やループの終了条件を書く代わりにエラーを利用して強制的に終了させるテクニックも有効です．

let rec f x=print_int x;x>0&f(x-1)
let rec f i=print_char"hoge".[i];x>0&f(x-1)

は，それぞれ，

let rec f x=print_int x;f(x-x/x)
let rec f i=print_char"hoge".[i];f(x-1)

と書けます．1 つめは 0 除算によるエラー，2 つめは文字列への不正アクセスによるエラーを利用して終了しています．また，標準入力に対する eof エラーによる強制終了も有効です．

while 0=0do print_endline(read_line())done

オプショナル引数の利用

オプショナル引数はゴルフのために OLabl に取り込まれ，その後 OCaml に追加されました．というのは嘘ですが，そういっても過言ではないくらい重要なテクニックの一つです．関数内でローカル変数を定義したい場合に有効です．たとえば，

let f x=let y=read_int()in ...

という関数定義は，

let f?(y=read_int())x=...

と書けます．y が x に依存する場合は，

let f x?(y=read_int())_=...

のように無理矢理 2 引数関数にしてしまうと短くなるかもしれません．さらに，f を中置演算子にできる余地も出てくるでしょう．

その他のテクニック

手抜きですみませんが，その他のテクニックについては昨年の OCaml Meeting で発表した スライド が参考になれば幸いです．

さいごに

これは，あくまでゴルフ向けのテクニックです．OCaml で普通のプログラミングをしたいときにこれらを使うのは絶対にやめましょう．複数人でのプロジェクトなどで多用すると間違いなく嫌がられるのでご注意を．