迷路の試験問題を解いてみた

参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。
Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。

まず、accessiblesという関数を定義し、以下の性質を証明した。
ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。

Fixpoint accessibles (start : node) (len : nat) : list path :=
  match len with
  | O => (PUnit start) :: nil
  | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n')
  end.

この関数はstartから始まってlenの長さのパスが到達できる点(を終点とするパス)全体を返す関数を表現している。

Theorem soundness : forall x n p,
  In p (accessibles x n) -> Path x p /\ plength p = n.

この定理は「リスト(accesibles x n)のすべての元pはPath x pかつ長さがnである。」ということを言っている。

Theorem completeness : forall x p,
  Path x p -> exists p0,
    endof p = endof p0 /\ plength p = plength p0 /\ In p0 (accessibles x (plength p)).

これは「xからのパスpが存在するならば、pと同じ終点にたどり着き、pと同じ長さであるようなp0が(accesibles x (plength p))の中に存在する。」ということ。

停止しない処理をCoqで記述できないため、結果を無限リストとして定義し、OCamlに渡した。OCaml側では無限リストを順番に見ていき、解があれば出力する。

上記の定理より、パスの長さに関して同一視するとすべてのゴールへたどるパスは得られる無限リストに含まれており、無限リストは短い順に並んでいる。よって無限リストを順番にみた結果見つかった解が最短であることが保証される。

ソースコード全体は以下。
http://bitbucket.org/yoshihiro503/maze_solver/src/

実行結果

$ cat input.txt 
**************************
*S* *                    *
* * *  *  *************  *
* *   *    ************  *
*    *                   *
************** ***********
*                        *
** ***********************
*      *              G  *
*  *      *********** *  *
*    *        ******* *  *
*       *                *
**************************

$ time ./run < input.txt 
**************************
*S* *$$$$$               *
*$* *$ * $*************  *
*$*$$$*  $$************  *
*$$$ *    $$$$$          *
**************$***********
* $$$$$$$$$$$$$          *
**$***********************
* $$$$$*$$$$$$$$$$$$$$G  *
*  *  $$$ *********** *  *
*    *        ******* *  *
*       *                *
**************************

real	0m0.129s
user	0m0.124s
sys	0m0.000s