無限ストリームで幅優先探索

Coq

参考：http://d.hatena.ne.jp/yoshihiro503/20100119#p1

証明すげー。
あと、幅優先探索で見つけたパスを無限ストリームで並べているのを見てこれは面白いと思った。枝刈り付きBFSとゴールの発見手続きを独立に書けているのか。なるほど！ ストリームを使ったプログラミングはHaskellでもよくあるし、モジュール性を向上させるというのもどこかで読んだけど、実際に目の当たりにするととても面白い。そしてストリームで書いたことによるプログラムの独立性が証明の簡潔さにつながっている(たぶん)のはとても興味深い。いや私はアルゴリズム苦手だし、関数型プログラムでパズルを解く人たちにはストリームなんて当然のことなのかもしれない。でもとにかく、感銘を受けたのでちょっとアルゴリズムを勉強しなおそうと思った。プログラムのエレガントさは、きっと証明のしやすさに影響するのだ。
一方、ストリームを作るときにaccessibles関数が何度も長さ

(* Solve.v の途中から *)
Require Streams.

CoFixpoint accessibles_aux (p : list path) : Streams.Stream (list path) :=
    let p' := div_equiv path_equiv_dec @@ (flat_map expand p) in
    Streams.Cons p (accessibles_aux p').

Definition accessibles_st (x : node) : Streams.Stream (list path) := accessibles_aux (cons (PUnit x) nil).

この無限ストリームaccessibles_st xはn番目に長さnの(xからはじまる)パスのリストをもつ。各パスの計算はひとつ短いパスを利用してなされる(上でいうメモ化)。今ふと思ったけど制限は長さnというだけなのでパスは戻ったりしているものも含んでいるような気がする。ただパスのリストのうち終端が同じものが複数あってもそれらは同一視(path_equiv_dec)され枝刈りされる(div_equiv)のでストリームのある位置におけるパスの個数は高々マス目個に抑えられる。あまりアルゴリズム一般に明るくない私からしてみればそういうざっくりした枝刈りもあるのかという感じだ。これもプログラムの簡潔さに寄与していると思う(勘)。 もちろん戻っているパスを除いたりすればより枝を刈れるだろうけど、証明の複雑さに影響するかもしれない。

soundnessのまえに、次のinductive predicate Exists を導入する．

Inductive Exists : path -> Streams.Stream (list path) -> nat -> Prop :=
  | Here : forall p ps ss, In p ps -> Exists p (Streams.Cons ps ss) 0
  | Further : forall p n ss, Exists p (Streams.tl ss) n -> Exists p ss (S n)
.

Exists p st n で、ストリームstのn番目の要素にパスpが含まれることを表す。

soundness定理は次のようになる。

Theorem soundness_st : forall x n p, Exists p (accessibles_st x) n -> Path x p /\ plength p = n.

ある物体がaccessibles_st x の n番目に入っていたら、そいつはちゃんとxからのパスになっており、そいつの長さはnだ、という定理。
これを証明したいところだが、私のCoq力はまだとても低くて証明できそうにない。

(論文が書けたら続きをやります)