証明を書こう!

この記事はCompetitive Programming (その2) Advent Calendar 2016 - Adventarの記事として書きました.

この記事に,技術的に有用なことはありません. 「証明を書こう!」という話です.

何か月か前に,とある方から次のような質問をされました.

競技プログラミングをやっていて,こういうのがあったらいいなあってものてある?

僕は「ちゃんとした解法の証明がほしい!」と答えました.その後に理由を長々としゃべりましたが,大体次のようなものだったと思います.

  1. 解説では解法の方針がざっくりと説明されているだけだから.
  2. (僕の研究室では)重要なスキルの一つに証明を書くことがあるから.(この質問の前に 「競プロって研究の役に立ってる?」 という質問をされていた.)
  3. (僕は証明無しでアルゴリズムについて話をするとうちの先生方に説教を食らうのに,みんなサボってずるい!)

1つ目の理由は,ざっくりとした説明だけではわかった"つもり"にしかなれないと思っているからです. 特に,最近は競プロの問題の難易度がどんどん上がってきていて,「本当にそれでうまくいくの?」と思うような解法がたまにあります. 牛ゲーとか,高難易度の貪欲とか「証明があったらうれしいなあ」と思うことがよくあります. なぜその解法でうまくいくのかを確認するには,やっぱり証明を追わないと.

2つ目の理由は,僕の所属している研究室の研究内容に大きく依存しています. 僕はアルゴリズム関係の研究室に所属しています. 研究室仲間がやっている研究は様々で,マッチングをやっている人もいるし,乱択数え上げをやっている人もいるし,分散アルゴリズムをやっている人もいます. 僕らに共通して必要なスキルは"証明を書くこと"です.だから,証明を書く練習がしたいし,そのお手本があったらうれしいというわけです.

ちなみに,この会話の最後に「お前がやればいいんだよ!」というツッコミをいただきました. アドベントカレンダーを書くまでに,問題の証明を書こうと思っていましたが,残念ながら間に合いませんでした. 今後,時間が空いたときに何かしら書いていこうと思います.

以上「(僕が)証明を書こう!」という話でした. 最後までお付き合いくださった方,ありがとうございます.