AtCoder Regular Contest 097 F

問題文: ARC097 F Monochrome Cat

問題概要

N頂点の木が与えられる。各頂点には0または1が書かれている。好きな頂点を選び、そこに行き、以降以下の1.または2.の操作のいずれかを何回か行う。

  1. 隣接する頂点を一つ選び、移動し、移動先の頂点の数字を1->0または0->1に変更する。
  2. 現在いる頂点の数字を、1->0または0->1に変更する。

操作は任意の地点から始めることができ、また任意の地点で終えることができる。
全ての頂点に書かれた数字を0にしたい。操作回数の最小値を求めよ。

制約

N <= 100000

想定*誤答*

1が書かれた頂点だけを考えれば良い。操作の始点・終点は、1が書かれた頂点同士の間でもっとも遠いペアにすれば良い。それさえ決まれば、dfsでできる。

正解

まず、0が書かれた葉は関係ないので、全て削除する (queueで簡単)。この時残っている頂点のリストを作ると良い。
求める操作列は、Euler tour から単純パスを引いたものである。Euler tourについての操作列の長さは簡単。どのような単純パスを引けばいいかを考える。頂点vに書かれた数をc[v]とすると、単純パスを引くことによる操作回数への効用は、2 * #{v | c[v] xor (deg[v] % 2) } である(この値だけ操作回数が少なくなる)。これを最大化すればよい。最大化は木の直径を計算するのと同じアルゴリズムで、O(N)でできる。

感想

こういう難しい問題でも、数学的な分析ができるようになりたい。最初解く時に、始点と終点は最遠点同士だと決め打ちしたが、これにはなんの根拠もない。このような考察ミスをなくすのが大切。

おまけ

誤答 Submission #2531853 - AtCoder Regular Contest 097 は、c[v] = 0となる葉の削除にも手間取っている。「DFS をやってみて、c[v] = 1となる頂点に出会う前に元の頂点に戻ったら、そこより先はなかった扱いにする」ということをやっているが、これはやってはいけない。

解説をみた後の正答:
Submission #2532111 - AtCoder Regular Contest 097

チェス 2018/05/13

同じ相手と白黒入れ替えて2局指した。
少しチェスをやらない期間があると、すぐにblunderの鬼になってしまう…。

チェス 2018/05/08

kobaは黒。全体的に動きが良くないが、特に31手目から壊滅しているので、自戒のために。

Daily Chess 2018/05/04

chess.comでdaily chessをやった。kobaは黒を持った。12...Nxe4がひどいblunderだったが咎められず、その後も最後まで白がはっきり有利だと思ったが、後で評価してみるとそうでもないようだった。

Lean Proverのuniverse polymorphismの罠

このようなコードをLean Proverで検査しようとすると、補題test2でエラーが出る。1

gist.github.com

いくら考えても原因がわからなかったのでGitHubのレポジトリにバグとして報告したところ、バグではなく仕様である、という返答を頂いた。 github.com

ここに書いてあることを要約する。constant t: Sort uと宣言すると、宇宙uごとに型t.{u}: Sort uができ、constant f: t -> tという宣言によって、 宇宙のペアu,vそれぞれに対しf.{u v}: t.{u} -> t.{v}ができる。

この状態でf x = f xという式の型付けおよび型検査を行うと、もっとも一般的な型付けは@eq.{v} t.{v} (f.{u1 v} x.{u1}) (f.{u2 v} x.{u2})である(v,u1,u2は宇宙、返答にあるものとは名前を変えている)。等式の左右で型が等しいという条件はあるが、中身の関数およびその引数の型が等しいという条件はないことに注意。変数f, xのパラメータとなる宇宙が違うため、両辺が構文的に等しくなくなってしまい、reflexivity tacticが失敗したのである。(補題testではreflexivityが成功するが、これはx = xの型付けを行うと@eq.{u} t.{u} x.{u} x.{u}となるためである。)

この問題の解決法は2種類ある。1つ目はissueの返答にも書いてあるように、universe polymorphismを使うのをやめ、t: Typeと宣言することである。もう一つは、universe polymorphismを使うが、問題となる全ての変数について、それのパラメータとなっている宇宙を指定することである。例えば以下のコードは正しく検査される。 gist.github.com

なお、この手の問題を解決するには、pretty printingの設定を変えるのが有効である。set_option pp.all trueを実行すれば、エラーメッセージやgoalの表示などで詳細な情報を表示してくれる。


  1. 実はlemmaではなくexampleとして証明するとエラーが出ない。原因は不明である。set_option pp.all trueを使ってもよく分からない。

Lean Proverのinaccessible termについて

最近Lean Prover (Lean 3)で原始再帰的関数について証明を書いているので、それによって得られた知見を一つ紹介する。

gist.github.com


inaccessible termとは何か

".(項)"の形のパターンはinaccesible termと呼ばれ、パターンマッチを行う際に、この部分はパターンとしてではなく、項として一致するかどうかの検査が行われる。(つまり、パターン以外の項が書ける。)
項の部分は同じパターン内ですでに定義されている変数でなければならない。項の内部で新しい変数を導入することはできない。

使用例

埋め込んだコードのprim_evalの定義(ll. 36-48)でパターンマッチを行なっているが、これのl.40, l.42で使用されている。
典型的な使用例として、同じ値が複数個出現することがわかっているパターンマッチ(l.40のマッチングではmが2回登場する)で使用できる。(パターン内で同じ変数名を複数回使うことはできない。)
また単にパターンが複雑になってしまったり、マッチさせなくても自動で推論できる場合にマッチを省略する目的でも使用できる。(l.42のマッチングでは".(_)"というパターンがあるが、これはprim_evalの第一引数はk + 1であることが推論できるため合法である。)

なお、ここでの本題とは外れるが、l.40のパターンに含まれている"@prim_rec.prec"の"@"は、@演算子と呼ばれ、implicit parameter (l.5のkとm)を陽に引数にとる、という効果を持つ。これがないとkをパターンマッチさせることができず、この場合はfの型が推論できないというエラーが出る。

参考文献

Theorem Proving in Leanの8.5 Inaccessible Terms (inaccessible terms), 2.9 Implicit Arguments, 6.8 Displaying Information (@演算子)