ぼくもしゅうしょくしないと

金曜日ぐらいから採用試験の問題を考えていたのですが、自分のPCに溜め込んでいてもどうにもならないので折角だから書いてみます。

いやそれよりも、MacBookさんの容量が大変です・・・どうしてこうなった。
あとプリンスオブペルシャのPS3版はちょっとうーんな感じでしたけど面白いんじゃないでしょうか。テレポートの存在に気付かなかったので終盤までずっと浄化したエリアまでも自力で移動していたのですがテレポートやばい・・・。すごいなー。

まずC++を使って

最初書いたもの

#include <iostream>
#include <string>
#include <boost/array.hpp>
using namespace std;
using namespace boost;

const int WIDTH = 26;
const int HEIGHT = 13;
const int BLOCK = 123456;
const int FREE = -2;
const int GOAL = -1;

typedef array<array<int,WIDTH>,HEIGHT> MAP_t;

array<string,HEIGHT> MAP = {
    "**************************",
    "*S* *                    *",
    "* * *  *  *************  *",
    "* *   *    ************  *",
    "*    *                   *",
    "************** ***********",
    "*                        *",
    "** ***********************",
    "*      *              G  *",
    "*  *      *********** *  *",
    "*    *        ******* *  *",
    "*       *                *",
    "**************************"
};

void print_map(const MAP_t& m)
{
    for(int y=0;y<HEIGHT;++y)
    {
	for(int x=0;x<WIDTH;++x)
	{
	    switch(m[y][x])
	    {
	    case BLOCK:
		printf(" ＊");break;
	    case 0:
		printf(" 始");break;
	    case FREE:
		printf(" 　");break;
	    case GOAL:
		printf(" 終");break;
	    default:
		printf("%3d",m[y][x]);break;
	    }
	}
	puts("");
    }
}

int update(MAP_t &m,const int &x,const int &y)
{
    int res = 0;
    int dxy[4][2] = {
	{1,0},//→
	{-1,0},//←
	{0,1},//↓
	{0,-1},//↑
    };
    for(int i=0;i<4;++i)
    {
	int now_x = x + dxy[i][0];
	int now_y = y + dxy[i][1];
	if(0 <= now_x && now_x < WIDTH && 0 <= now_y && now_y < HEIGHT && (m[now_y][now_x] == GOAL || m[now_y][now_x] == FREE))
	{
	    m[now_y][now_x] = m[y][x] + 1;
	    ++res;
	}
    }
    return res;
}

MAP_t fix(MAP_t m)
{
    for(int iter=0;;++iter)
    {
	int change=0;
	for(int y=0;y<HEIGHT;++y)
	{
	    for(int x=0;x<WIDTH;++x)
	    {
		if(m[y][x] == iter)
		{
		    change += update(m,x,y);
		}
	    }
	}
	if(change == 0)return m;
    }
}

int main()
{
    MAP_t init;
    for(int y=0;y<HEIGHT;++y)
	for(int x=0;x<WIDTH;++x)
	    switch(MAP[y][x])
	    {
	    case '*':
		init[y][x] = BLOCK;break;
	    case 'S':
		init[y][x] = 0;break;
	    case ' ':
		init[y][x] = FREE;break;
	    case 'G':
		init[y][x] = GOAL;break;
	    }
    MAP_t fixpoint = fix(init);

    print_map(fixpoint);

    return 0;
}

面倒臭いのでパスは求めてませんが、終点から逆に辿ればすぐにでるのでそういう事にしておいてください...(でないとこの後の証明が悲しい)

おい直に埋め込んでんなみたいな感じでごめんなさいもうなにもかもごめんなさいな感じですがもうごめんなさいマンでお願いしますごめんなさい・・・。

これ自体は20分もあれば十分なので良いとして、後2時間40分で証明を書かなければならない。

取りあえず頭の中でAgda2さんがワシの力を使えと言っているので取りあえず力を借りたいなーって事で次の形にプログラムを書き直す。

次に書いたもの

#include <iostream>
#include <string>
#include <utility>
#include <boost/array.hpp>
using namespace std;
using namespace boost;

const int WIDTH = 26;
const int HEIGHT = 13;
const int BLOCK = 123456;
const int FREE = -2;
const int GOAL = -1;

typedef array<array<int,WIDTH>,HEIGHT> MAP_t;

array<string,HEIGHT> MAP = {
    "**************************",
    "*S* *                    *",
    "* * *  *  *************  *",
    "* *   *    ************  *",
    "*    *                   *",
    "************** ***********",
    "*                        *",
    "** ***********************",
    "*      *              G  *",
    "*  *      *********** *  *",
    "*    *        ******* *  *",
    "*       *                *",
    "**************************"
};

void print_map(const MAP_t& m)
{
    for(int y=0;y<HEIGHT;++y)
    {
	for(int x=0;x<WIDTH;++x)
	{
	    switch(m[y][x])
	    {
	    case BLOCK:
		printf(" ＊");break;
	    case 0:
		printf(" 始");break;
	    case FREE:
		printf(" 　");break;
	    case GOAL:
		printf(" 終");break;
	    default:
		printf("%3d",m[y][x]);break;
	    }
	}
	puts("");
    }
}

int update(MAP_t &m,const int x,const int y)
{
    int res = 0;
    int dxy[4][2] = {
	{1,0},//→
	{-1,0},//←
	{0,1},//↓
	{0,-1},//↑
    };
    for(int i=0;i<4;++i)
    {
	int now_x = x + dxy[i][0];
	int now_y = y + dxy[i][1];
	if(0 <= now_x && now_x < WIDTH && 0 <= now_y && now_y < HEIGHT && (m[now_y][now_x] == GOAL || m[now_y][now_x] == FREE))
	{
	    m[now_y][now_x] = m[y][x] + 1;
	    ++res;
	}
    }
    return res;
}

pair<MAP_t,bool> fix(const int n,const array<string,HEIGHT> &m)
{
    if(n == 0)
    {
	MAP_t init;
	for(int y=0;y<HEIGHT;++y)
	    for(int x=0;x<WIDTH;++x)
		switch(MAP[y][x])
		{
		case '*':
		    init[y][x] = BLOCK;break;
		case 'S':
		    init[y][x] = 0;break;
		case ' ':
		    init[y][x] = FREE;break;
		case 'G':
		    init[y][x] = GOAL;break;
		}

	return make_pair(init,false);
    }
    else //∃m>=0.n = m+1
    {
	int change=0;
	pair<MAP_t,bool> pre = fix(n-1,m);
	MAP_t map = pre.first;
	bool is_fixpoint = pre.second;

	if(is_fixpoint == true)return pre;

	for(int y=0;y<HEIGHT;++y)
	{
	    for(int x=0;x<WIDTH;++x)
	    {
		if(map[y][x] == n-1)
		{
		    change += update(map,x,y);
		}
	    }
	}
	//mapが不動点だった時
	if(change == 0)return make_pair(map,true);
	else return make_pair(map,false);
    }
}

int main()
{
    pair<MAP_t,bool> fixpoint = fix(WIDTH*HEIGHT,MAP);
    print_map(fixpoint.first);
    return 0;
}

ここまで来たら証明とか余裕じゃないっすか！！あと2時間30分ぐらい。

この再帰関数を書く時に「頭の中で仮定していた」何か達を片っ端から示せば良くてそれは多分このアルゴリズム全体の証明になる。うおおおおおおおおおおお。

証明

次の定理を証明したい。

定理 : このアルゴリズムは、各ステップnでn-距離集合の要素を全て見つける事が出来る。
証明 : 帰納法を用いる。

その前に中で適当に使っている用語の説明。
ここで　ステップn というのは、関数fixの引数がnである事を表している。(再帰で潜った帰りを表す感じ)
n-距離というのは、ある点の始点からの最短距離がnであるという事。
n-距離集合というのは、その要素が全てn距離である事を表す。
ある点が未束縛というのは、その点がどんなn-距離集合にも属さない事を表す。

ステップ0では、始点のみを含む単一集合を作れば良い。

ステップn+1について、ステップnでn-距離集合の要素を全て見つけていると仮定する。

いま、アルゴリズムが作用し、ステップn+1が終了したとする。この段階で、n+1-距離集合の要素を全て見つけていないとしよう。
すなわち、本来はn+1-距離集合に含まれるべきある点(Aとする)が存在するが、n+1-距離集合に含まれていない。

このAに到達する為にはあるn-距離集合の要素を経なければならない。補題1でそれを証明する。

補題1

補題1:
n+1-距離集合の要素に辿り着く為には、最後にn-距離集合のある要素を経なければならない。
証明:
最短距離は、周囲4マスまでの最短距離+1のうちで最も小さいものから決定される。よって明らか。

補題1の後

今現在n-距離集合の全ての点に対し、その点から辿り着ける全てのn+1-距離集合の要素を求めていることを証明する

補題2

補題2 : n-距離集合の全ての点に対し、その点から辿り着ける全てのn+1-距離集合の要素を求めている
証明 :
nステップ目で作ったn-距離集合の要素全てに操作をしているのは明らかであるので、ある要素から辿り着ける全てのn+1-距離集合の要素を見つけている事を証明したい。

まず全てを見つけているかどうかについてだが、このアルゴリズムでは他の距離集合に属している隣接する点を書き換える事はしない。(これは既に、適切な距離集合の要素として見つかっているということ。)
次に隣接する未束縛の点をn+1-距離集合にしてしまう。隣接する点は、束縛されているか、未束縛かのどちらかであるので点の状態パタンは全てカバーしている。
また今回は上下左右で4つという有限な方向しか調べない事から、明らかに全ての要素を見つける事が出来ると言える。

次にこの未束縛の点をn+1-距離集合の要素にしてしまうという操作が、確かに適切なものであるかを次の補題3で示す。

補題3

補題3:
n-距離集合に隣接する未束縛の点をn+1-距離集合の要素にしてしまう操作は、
確かにn+1-距離集合の要素を求めている。

証明:
n-距離集合のある要素に隣接する点が未束縛というのは次の図のような状態の事である。

(ここでは、ある要素の右に未束縛の点があることを表す。というよりブラウン(??)色が未束縛。)

この未束縛の点への距離は、周囲4点の始点からの距離+1のうち最も小さいものになるのであるから、
間違いなくn+1が最も小さい。
(この時点で未束縛であるということは、この点の始点からの距離がn以下ではありえない事は帰納法の仮定[ステップnでn-距離集合の要素を全て見つける事が出来る]ことより明らか)
かつ、n-距離集合のある点からこの点へ移動可能であるのだからそのパスを選べばこの点の始点からの距離はn+1となる。
よって補題3が示された。

補題3のあと

補題3を用い、補題2を示す事が即座に出来る。

補題2のあと

ところが補題2によって、見つかっていないというのならば、ステップnの作ったn-距離集合が完全で無かった事に成る。

しかしそれは仮定と矛盾。従ってそのような点は存在しない。すなわち、ステップn+1ではn+1-距離集合の要素を全て求める事が出来る。

よって帰納法より、このアルゴリズムはnステップ目でn-距離集合の要素を全て求められる事が分かった。

出来たか？？

分かりません・・・。ただ構成的じゃないのと、問題なのはこれをAgda2に落とす事は出来ないにゃーーーーーーーーー！！！！！！！！！！！！！！

ただ停止性に関しては今回C++の中でも書いてますが、WIDTH * HEIGHTステップ計算すれば十分なので簡単に言えますね。

各証明はプログラムのこの部分に対応するよね？みたいな事を書くべきなんでしょうけどまぁ面倒臭いしLv2以上の人沢山いるっぽいっていうのはブクマ見てて分かったので早く定理証明系使った最短性出てこないかなぁみたいな・・・。

私のやり方が不味いのは、

プログラム言語・OSは自由

という制約で、証明をプログラム言語で書けていないというのが一番まずくて、日本語を証明に使っても良いなら良かったのですが、書いてない。
ということはこれではLv2なので取りあえず就職は出来ないんだなーっていう事が分かった。アホだ・・・やばいどっとこむ

追記

だいくすとらさんさいたんけいろあるごりずむでやる人には、恐らく
http://www.cs.utexas.edu/~moore/publications/dijkstra/index.html
が参考になると思います。ACL2はLisperでは有名でみんなLispを使うっぽいので良いと思いますし私はLispを知らないしACL2も全然知らないのでLisp使う人は教えてください・・・。

これとは関係無いですがProof Pearlは色々面白い話題があって("The power of higher-order encodings in the logical framework LF"とか"A Practical Fixed Point Combinator for Type Theory"です！！)、英語です…