週に一回は書きますよ 月に4つ記事を書けばノルマは満たされます。
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

唐突にcoqで圏論の会に参加表明して行ってきました。 Thanks to mr_konnさん。

<余談>...ツイートリストを修飾するタグが欲しいなぁ。</余談>

実は半年あたり前にちょろっとだけCoqを勉強していたので、そのちょうどいい復習として行ってきました。圏論の知識はあまりありませんでしたがなんとかなった、はずです。

皆で使用していた圏論のライブラリ ConCaT が曲者で、なかなかみんな苦労していました。皆おおよそCategory.vやそこから引用されているMap2.v, Setoid.v などを眺め、書き換えたり写経したりして学習していました。

結果はtogetter「Coqで圏論の会」をご覧ください。

私の成果物は以下のとおり。

1. 要素のない圏

すでにライブラリに要素が一つしかない圏 ONE.v が書かれていたため、それを写経すればおおよそできます。そのため、練習問題として多くの人が書いていました。

私の証明には、なるべくcontradictionを使うようにしています。「異議あり! そもそも前提が狂っている!」と。ZERO.vの定義は以下の行で、要素が何も無いことを宣言するところから始まります。

Inductive Zero_ob : Type :=.

Inductive Zero_mor : Zero_ob -> Zero_ob -> Type :=.

この「何も無い」定義が Falseの定義 と同じだったので、せっかくだからFalseと同じであることをアピールしておきました。

2. Epic Monicに関する練習問題

  • EpicやMonicの合成もまたEpicやMonicである
  • 射の合成がEpic/Monicなら、合成元の射の片方もまたEpic/Monicである。どちらの片方かはEpic/Monicで逆になる。

教科書に載っている簡単な問題です。時間内には結局前半のEpicの側だけ終えました。上のリンクはその後に全部終えたものです。

はまりどころが大量にありました。Zero.vと違い殆ど写経出来なかったのでCoq力が試されたといったところです。

  • =_Sは等式じゃないからrewriteできない。かわりに直接transivitiyことTransをapplyする。
  • f o gf: a-->b, g: b-->c から a-->c を作る。普通の o 演算子と逆。
  • Epic a ba --> b なのにたいし、Monic a ba --> b と逆。

課題と関係なく感心したことを一つ。ONE.v の合成演算子結合則 Comp_One_mor はやることの割に長くて微妙な定義です。ここをもっと簡単にCoqらしく書く方法として、次のように結果の型だけ宣言してしまい、内容は証明で書くという方法があります。

Definition Comp_One_mor (a b c : One_ob) (f: One_mor_setoid a b) (g: One_mor_setoid b c) : One_mor_setoid a c.
Proof.
(省略)
Qed.

こちらのほうが試行錯誤や高度なtacticsの適用を使えるので楽です。このあたり、証明器を補助にプログラムが書けるのはCoqの便利なところだと改めて思うのでした。Coqでプログラムを書くことそのものはかなりの苦行ですが。

スポンサーサイト

(この記事は Functional Ikamusume Advent Calendar jp 2010 の為に書かれました)

手続き型を支配するチャンスでゲソ!今日こそギャフンと言わせてやるでゲソ!

#include <iostream>
#include <string>

using namespace std;

int main(void) {
  string s = "イカ娘!";
  for (int i = 0; i < 6; ++i)
    s = "侵略!" + s;
  cout << s << endl;
}


ループを再帰にするでゲソ。

#include <iostream>
#include <string>
using namespace std;
string f(int i) {return i?"侵略!"+f(i-1):"イカ娘!";}
int main(void) {cout << f(6) << endl;}


さらに再帰を末尾再帰にするでゲソ。

#include <iostream>
#include <string>
using namespace std;
string f(int i, const string& s) {return i?f(i-1,s+"侵略!"):s+"イカ娘!";}
int main(void) {cout << f(6,"") << endl;}


C++にはfoldがあるじゃなイカ。手で再帰を書く必要はないでゲソ。

#include <iostream>
#include <numeric>
#include <string>
#include <vector>

using namespace std;

int main(void) {
  const string s = "イカ娘!";
  const vector<string> v(6, "侵略!");
  cout << accumulate(v.begin(), v.end(), s) << endl;
}

間違ってなイカ? 順序が逆でゲソ。

#include <iostream>
#include <numeric>
#include <string>
#include <vector>

using namespace std;

string rev(const string& lhs, const string& rhs) {
  return rhs + lhs;
}

int main(void) {
  const string s = "イカ娘!";
  const vector<string> v(6, "侵略!");
  cout << accumulate(v.begin(), v.end(), s, rev) << endl;
}

これで正しいんじゃなイカ?


さらに無名関数を使うでゲソ。

#include <iostream>
#include <numeric>
#include <string>
#include <vector>
#include <boost/lambda/lambda.hpp>

using namespace std;
using namespace boost::lambda;

int main(void) {
  const string s = "イカ娘!";
  const vector<string> v(6, "侵略!");
  cout << accumulate(v.begin(), v.end(), s, _2 + _1) << endl;
}


accumulateがfoldlなので、foldrを定義するでゲソ。

練習問題: ここを埋めなイカ。


コンパイル中に文字列を構築するでゲソ。

#define BOOST_MPL_LIMIT_STRING_SIZE 150
#include <iostream>
#include <string>
#include <boost/mpl/char.hpp>
#include <boost/mpl/fold.hpp>
#include <boost/mpl/placeholders.hpp>
#include <boost/mpl/range_c.hpp>
#include <boost/mpl/string.hpp>

using namespace std;
using namespace boost::mpl;

template <typename T1, typename T2>
struct concatenate : public fold<T2, T1, push_back<_1, _2> > {};

int main(void) {
  cout << c_str<fold<
      range_c<int, 0, 3>,
      boost::mpl::string<'イ','カ','娘','!'>,
      lambda<concatenate<boost::mpl::string<'侵','略','!'>, _1> > >::type
    >::value << endl;
}

6つだそうとしたらマシンが反応しなくなったでゲソ。貧弱じゃなイカ?

ICFP contest チームぴゅあぴゅあこーどで私が作った車は、非常に簡単なものでした。しかしなぜかほとんど解けません。なぜ解けないのかは自分でも理解していませんが、何を作ったかを簡単に解説します。

問題の解説

まず問題を簡単に説明します。やるべきことは「車」と、それを動かす「燃料」を提出することです。車はそれにあった特定の燃料しか受け付けません。他のチームからは提出された車だけが見えていて、それを動かす燃料を推測することになります。車を提出したチームは、それを動かす燃料を他のチームが出さない限りは、その車からすべての収益をまるまる手に入れることができます。一方その車を動かす燃料が他のたくさんのチームから提出されてしまうと、車からの収益はそれらのチームと折半することになってしまうので、非常に美味しくありません。なので、車を提出するチームは、なるべくそれを動かす燃料を推測されにくい車を提出する必要があります。

「車」は条件式N個の集まりで、各条件式は次のような形をしています;

  • 例1: ABBCBABCABB - ABCBABCBABCABCB (≥) 0.
  • 例2: BABBEBC - AFDBCBDBEBFBC (>) 0.
    • A から FはN x N 行列が入る変数。たかだか6種。
    • (≥) 0 は「行列の要素全てが0以上」という不等式。
    • (>) 0 は (≥) 0 かつ行列の(1,1)要素が正であるという不等式。
    • つまり、たくさんの行列の積二つの差分が、すべて非負である、という条件。

行列を使った不等式です。ただし、車には行列の要素数は指定されていません。

「燃料」は、非負の整数からなるNxN行列 k個で表現されます。ただし行列の(1,1)要素はすべて正である必要があります。燃料の行列をk個を車の変数に代入して、車の持つ条件式をすべて同時に満たすことができるなら、その車はその燃料で動かすことができます。

車が要求する変数の数は固定なので、燃料はそれと同じ数の変数を提供する必要があります。一方、行列の次元は指定されていないので、燃料を作る側は自由に大きな行列を使うことができます。1x1次元の行列を考えて車をデザインしても、2x2以上の行列を持ってくると容易に解けたりします。

pure pure code ++の車

pure pure code ++のアイデアは以下のもので全部です。最初のものはyuizumiさんのアイデア、真ん中のはソルバ班chunのアイデアだったと思います。

  • 燃料を与えて、それを受け取る車をランダムに生成する。
  • 条件式を厳しいものだけ採用する。
  • 焼きなまし法で解けない車だけ採用する。

まず答えとなる燃料を用意します。次に条件式をランダムに生成して、そのうち設定した燃料が満たす条件式だけ採用します。これを決められた数だけ集めて車を作ります。基本はこれだけです。

条件式は最終的には99本いれていましたが、車を生成するときにはもっと多く作っていて、そのうち一部だけを入れてあります。具体的には、条件式をその左辺の行列の要素の最小値でソートして、小さい方から取っています。これで選ばれる条件式は、与えられた行列でギリギリ満たせるような厳しい条件です。左辺の要素がすべて大きいゆるい条件は採用から外れます。こういう条件だけを採用することで、条件全体を満たす解空間を狭めているつもりです。これは、解きにくい車の条件として、ソルバ班chunから教えてもらったものです。

さらに、得られた車をチームの車ソルバにかけて、解が見つからないものだけを頑丈な車として選んでいます。ソルバにかけた車の1/3がソルバに解かれています。

ここまでが車の作り方です。上の記述では入力として与えられている燃料も、実際にはランダムに生成しています。必要なパラメータは次の通り。

  • chamberの数は2000作って99だけ採用。
  • 各chamberは上下各20個のsectionを持つ。
  • 答えの燃料は変数2--6種、行列の次元は2x2か3x3、要素の値は平均12の指数分布。
    • 今から考えるともっと大きい方が良かったかも。よくこれで全探査を回避できたものです。
  • ソルバは焼きなまし2種類を3分ずつ。

なぜこんな簡単な方法で、非常に強いソルバで1/3しか落とせない問題が出来たのかはよく理解していません。ただ、この問題は車制作の方が自由に難しい問題を作れて圧倒的に有利なので、そもそもあまり解けなくても問題はないのかもしれません。

最遅ですがレポート提出。総勢6人で"pure pure code ++"で参加していました。

他の参加者は以下のとおりです。

問題は以下により熟知のこと。

私はおおよそ車を作っていました。作るのがあまり早くなかったのでどれだけ貢献できたか。速いチームは非常に早くから超堅牢な車を作っていたので。車については別途記事を作るとして、まずはタイムラインをどうぞ。

6/14.

ICFPCのチーム計画ML上にて、チーム名の話題が上がったとき「ぴゅあぴゅあこーど...... いえ、なんでもないです」

6/19.

この日はskype上で参加していました。問題には「仕様は推測してくれ」という謎仕様。問題以外からヒントを得ようとアカウントを作るもこちらも謎。燃料が投げられるようになるものの、燃料を供給する先の車をクリックすると、車のコードが"122000010" と出力される。これに対し、燃料を未だ解読出来ていない記法で記述して送る、と。かなり高レベルの禅問答です。

回路の部分が入り口であることをおおよそみなで把握。phoenix氏が一時間で回路を解読。graphviz化. 何人かで回路を解読。私は車や燃料の記述を翻訳していました。目が疲れたので早めに就寝。

6/20.

朝起きたら回路の解読が完了し、回路からの任意の数列の出力ができるようになっていました。すごい。

この日はなんか目が異様に疲れてパフォーマンスが悪かった覚えが。チームは燃料と車の符号形式を解読していましたが、私は少し外れて車の仕様を見ていたりしました。あとtanakhさんのHaskellを解読とか、難しい車の妄想とか。2x2行列でAB-BAを使おうと思ったりとか不可能問題をいろいろ作っていました。時間の無駄かと思いきや、行列の勘を取り戻していたのかもしれません。

確かこの日の夕方辺りから適当に車の生成ルーチンに着手しました。このあたりで燃料の焼きなまし生成が完成していて、 1x1行列である程度難しく作った車が焼きなまし法で2次元解で一瞬で解かれるのは非常に衝撃的でした。

解かれてもいいので提出しようとしたのですが、生憎正規化ルーチンが不足していたので提出もかなわず。結局車は提出せずにlightningを終了。

6/21

昼あたりまでに車の正規化も完了。あと一次元の車は解けてしまうということで二次元以上の車を出すことにして昼あたりから徐々に車を提出。始めに数台試験的に出した車は予想どおり解かれてしまいましたが、その後20台ほど出した車は解かれないことを確認。車の生成を半自動にして、深夜寝ている最中に40台の車を生成。

6/22

有給。全部の車を出荷。その後は焼きなましを手伝ってみたり個別スクリプトを手伝ってみたり。

車は結局本気仕様3台を含む6台が解かれて、残り66台は放置されていました。素晴らしい、のは私のスクリプトよりむしろ、tanakhさんの焼きなましです。

前の配列→vector変換の記事に、配列にこだわらなければコンテナの初期化は「それboostでできるよ」のつっこみがありました。

ありました。

ちなみに前に調べたときは見つからなかったんですよ。絶対あるとは思っていたのですが。

上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。