七不思議ハードオオイカリパッチ深遠100F到達しました。
やった！ （→ リプレイファイル）
サブ剣に 日本刀[封必－脱封守]+17。盾は深層で[潰][爆][祓]を順次追い出して左のスクリーンショットが最終形。 [冷]も消してよかったな。保存の壺フィーバーが来たのでなんとかクリアできた感じでした。 普通の引きだと70F前後で大抵力尽きる。
普通にバランスのとれてるノーマル版に、 ・シレンで言うところのカンガルー３種を投入し ・主人公LVアップ時のHPと攻撃力の上昇量を減らし ・床落ちアイテム数を減らし敵のドロップ率も減らし、 たらどうなるでしょうかというパッチ。このゲーム4倍速まで上がるのでオオイカリ状態がより一層ヤバい。 代わりに幾つかの印の効果が強化されてて、レアアイテム出現率がやや上がっているので、 その辺りを鍵に頑張ることになります。 トルネコとかシレンとか好きで難易度の高いダンジョンに潜りたい人には超おすすめ。 自分の感覚では万歩の次くらいにハードでした。
ふと気がついたら 読書メーター に記録付け始めて１年が過ぎてました。
コメント読み返すと…よくわからないものが多い。 感想を直に書いているので、今見直してもとっさにどういう話だったか思い出せなくなってるものが多い。 もう少し内容まとめ的なものを書いた方が、後で読み返すときには楽しいかもしれないなあ。
ranha さんが面白そうなことをやっていたのでちょっかいを出してみました。 1+1 = 2 を「証明」してみる。C++ で。
まず準備。
class zero {};
template<typename N> class succ {};
template<typename N, typename M> class add {};
型で自然数をエンコードするいつものやり方です。zero という型が 0 を表して、
succ<zero> が 1 で、succ< succ<zero> > が 2 で、
…という雰囲気です。add<N, M> が N+M のつもり。足し算の定義はあとでします。
template<typename N, typename M>
class eq
{
private:
eq() {}
friend class axiom;
};
eq<N, M> が N=M のつもり。ただし、eq のコンストラクタは private です。
タダでは eq オブジェクトを作らせません。今から、N = M の証明があるときだけ、
eq<N, M> 型のオブジェクトが作れるようにしてやるつもりです。こうだ！
class axiom
{
public:
template<typename X>
static eq<X, X> reflexive() { return eq<X, X>(); }
どんな数 X でも X=X であることは反射律により証明できます。
なので、関数 axiom::reflexive<X>() を呼び出すと
eq<X, X> 型のオブジェクトが作れるようにしました。
axiom クラスは friend なので好き勝手に eq を作れます。
template<typename X, typename Y>
static eq<X, Y> symmetric( eq<Y, X> ) { return eq<X, Y>(); }
対称律。既に eq<Y, X> 型のオブジェクトがあるなら、つまり別の言い方をすると、
Y=X が証明できてるなら、それを引数にして axiom::symmetric( ... ) を呼び出せば
eq<X, Y> 型のオブジェクトが作れます。
template<typename X, typename Y, typename Z>
static eq<X, Z> transitive( eq<X, Y>, eq<Y, Z> ) { return eq<X, Z>(); }
同様に、推移律。X=Y かつ Y=Z が証明済みなら、X=Z がそこから証明されます、ね。
template<typename X, typename Y>
static eq< succ<X>, succ<Y> > suc( eq<X, Y> ) { return eq< succ<X>, succ<Y> >(); }
X=Y なら、Xの次の数=Yの次の数。
template<typename Y>
static eq< add<zero,Y>, Y > zero_plus() { return eq< add<zero,Y>, Y >(); }
template<typename X, typename Y>
static eq< add<succ<X>,Y>, succ< add<X,Y> > > succ_plus()
{ return eq< add<succ<X>,Y>, succ< add<X,Y> > >(); }
};
最後は、足し算に関する規則です。0+Y=Y と、(Xの次の数)+Y = (X+Y)の次の数 は、 常に成り立つので、無条件で、つまりゼロ引数関数で、作れます。
準備完了。
さてさて、一体何をやってたんでしたっけ。もう一度繰り返します。
「N=M の証明があるときだけ、eq<N,M>
型のオブジェクトが作れる」ように頑張りました。
本当にそうなっていることは…ええと、信じて下さい。
この部分は誰かが機械的に保証してくれる部分ではないので、
じっと睨んでそうなっているなあと納得するしかない部分です。
専門用語で "trusted base" などと言うらしい。
ここまでの構成の正しささえ認めることにすると、後は、「証明」の正しさは C++ コンパイラが保証してくれます。
上の段落の強調した部分を逆に言うと、
eq<N,M> 型のオブジェクトが作れたなら…eq<N,M>
型のオブジェクトを作るコードがprivateのアクセス制御違反に引っかからずにコンパイル通ったなら、
それはもう、N=M が証明できているということです。1+1=2 を証明するには、なんとかして
eq< add< succ<zero>, succ<zero> >, succ< succ<zero> > >
型のオブジェクトを作ってやればいい！
int main()
{
eq< add< succ<zero>, succ<zero> >, succ< add< zero, succ<zero> > > > p1
= axiom::succ_plus< zero, succ<zero> >();
eq< add< zero, succ<zero> >, succ<zero> > p2
= axiom::zero_plus< succ<zero> >();
eq< succ< add< zero, succ<zero> > >, succ< succ<zero> > > p3
= axiom::suc( p2 );
eq< add< succ<zero>, succ<zero> >, succ< succ<zero> > > proof_of_1_plus_1_is_2
= axiom::transitive( p1, p3 );
}
できました。これがC++による証明です。コンパイル通ります。なので、1+1=2 は確かに証明できることがわかります。
逆に、証明できないはずのもの…最近リバイバルブームの 2=1 型のオブジェクトを作ってみようとしてみてください。できないはずです （※ ただし自分でeqを特殊化する、reinterpret_cast するなどの裏技は禁止でお願いします…）。 引き算とか割り算とかは定義していないので元々リンク先のような"証明"は書けないのですが、 お暇な方はその辺り全部正しく定義して遊んでみると面白いんじゃないかと思います。すごく面倒いですが。
関連リンク集 ・Proof Party.JP ← ranhaさんが何か今週末にこういうこと関連のイベントを開くらしい。 ・Curry-Howard Isomorphism
つづきます。
ranha さんの元々の記事は、 「全ての自然数aについて、a+0=0+a である」というもっと一般的な定理を証明しようとしてました。 真似しましょう。こういう、自然数全部の性質に関する証明は、「数学的帰納法」で示すものらしいです。 つまり、「a=0 の場合の証明」と、「a=nの場合が証明できたと仮定した時の a=n+1の場合の証明」の２つができれば、 全ての a について証明できた、となるのが数学的帰納法です。これをC++で表現してみます。
template<typename X, typename PROP>
class forall
{
private:
forall() {}
forall<X, PROP> で、全ての自然数Xについて、PROPである、という主張を表すことにします。
forall< X, eq<X,X> > とかです。
もちろん、証明できるときだけ、この型のオブジェクトが作れる状況を目指します。
とりあえずデフォルトコンストラクタよさらば。そして…
typedef typename fresh<PROP>::type N;
public:
forall(
typename replace< PROP, X, zero >::type,
typename replace< PROP, X, succ<N> >::type (*)( typename replace<PROP, X, N>::type )
) {}
};
// freshとreplaceはユーティリティ。実装は気にしなくていいです。
// - fresh<PROP> は PROP で使われていない新しい型を適当に返す型レベル関数
// - replace<PROP,X,T> はPROPの中のXをTに書き換えた新しい型を返す型レベル関数
// 気になる人はソース全体をどうぞ。
２引数のコンストラクタを定義します。これを使ったときだけ、forall 型のオブジェクトが作れます。 第１引数は PROP の X を zero に置き換えた型です。この型のオブジェクトを渡すことができたら、 つまり、X=0 の場合を証明できたら初めて、forall が作れるようになるわけです。 第２引数は、帰納法のややこしい方の場合に当たります。この引数は関数ポインタで、 「X=Nの場合の証明(があることを保証するオブジェクト)を 受け取ったらX=N+1の場合の証明(があることを保証するオブジェクト)を返せる」、そんな関数です。 帰納法っぽいですね。この２つを作れたら、forallが証明できると認めることにしましょう。trusted base。
では証明。
// forall X. X+0=0+X の X=0 の場合の証明
eq< add<zero,zero>, add<zero,zero> > case_zero()
{
return axiom::reflexive< add<zero,zero> >();
}
// forall X. X+0=0+X の帰納法ステップの証明
template<typename N>
eq< add<succ<N>,zero>, add< zero,succ<N> > > case_step( eq< add<N,zero>, add<zero,N> > indhyp )
{
eq< add<zero,N> , N > p1 = axiom::zero_plus<N>();
eq< add<N,zero> , N > p2 = axiom::transitive( indhyp, p1 );
eq< succ< add<N,zero> > , succ<N> > p3 = axiom::suc( p2 );
eq< add<succ<N>,zero> , succ< add<N,zero> > > p4 = axiom::succ_plus<N,zero>();
eq< add<succ<N>,zero> , succ<N> > p5 = axiom::transitive( p4, p3 );
eq< add< zero,succ<N> > , succ<N> > p6 = axiom::zero_plus< succ<N> >();
eq< succ<N> , add< zero,succ<N> > > p7 = axiom::symmetric( p6 );
eq< add<succ<N>,zero> , add< zero,succ<N> > > p8 = axiom::transitive( p5, p7 );
return p8;
}
class X {};
int main()
{
// forall X. X+0=0+X 型のオブジェクトが作れた！
forall< X, eq< add<X,zero>, add<zero,X> > > proof( case_zero(), &case_step );
}
できました。なんだか長いですが、順を追っていけば確かに必要な型のオブジェクトを作っていることがわかると思います。 「証明」を間違えて変な型の関数を適用するとコンパイラが怒ってくれるので、 証明を書くときはコンパイラに頼りながら書いてます。
帰納法ステップの「Nの場合が証明できたと仮定してN+1の場合が証明できればOK」というのを、 今回は関数で表現しました。実はこのやり方は幾つか落とし穴があって、コンパイラを通った程度では、 本当は、証明の正しさの保証にはなりません。今回のは気分だけなんちゃって証明です。
まず、forall のコンストラクタは関数ポインタを受け取るだけ受け取って、
型が合っていることを見たら満足して他になにもしていないので、
forall<...> proof( case_zero(), 0 );、
とヌルポインタを渡してもオブジェクト作れてしまいます。
これはまずい。ぬるぽでは「Nの場合の証明オブジェクトからN+1の場合の証明オブジェクトを作れる」
ことの証拠にはなりません。
これは幸い回避することができて、
私のオリジナルのコード
はそうなってたのですが、forallには構造体を渡して、中でメンバ関数のアドレスをとっています。
これなら 0 にはできない。今回は説明が面倒だったので簡単な方に逃げてしまいました。
もう一つの、型だけしか見てないことの問題は、
template<typename N>
eq< add<succ<N>,zero>, add< zero,succ<N> > > case_step( eq< add<N,zero>, add<zero,N> > indhyp )
{
return case_step(indhyp);
}
再帰を使うと、返値型のオブジェクトを決して作れないにも関わらず、怪しげなキャストなどもせず、 コンパイルを通せてしまうのです。これもまずい。まずいので、世の中の証明記述に特化した証明用言語では、 再帰をするときは必ず再帰が停止することをまず証明しないといけないようになっています。 停止さえすれば、型があってれば、正しくその型の証明証拠オブジェクトを作れるはずなのでOKです。 C++はそういうための言語ではないので、これは、割とどうしようもないですね。 C++で無理矢理証明記述をするときの限界です。
最後の問題は、C++の場合、インスタンス化しないとテンプレート関数の型検査をできないので、
fresh<PROP>::type のようなダミー型を与えないとcase_step関数テンプレートの
型検査（＝証明検査）ができないところです。
freshな変数でおきかえて証明できたらforallは証明できたとしてよい、というのは正しいはずなので、
この１つの証明だけ見る分には、これでもなんとかなってます。ただ、forall
の証明オブジェクトを使い回すような更に複雑な証明（forall X,Y: X+Y=Y+X の証明など）
をしようとすると、ここら辺マジメにできないと困ることがだんだんわかってきます。
こちらは何かトリックでどうにか回避できそうな気がしているので、ちょっと考えてみたい。
素直にやるなら、C++よりもJavaやC#のようなGenericsを使った方が、これはストレートに表現できると思います。
まとめというほどでもないんですが、自分で eq とか forall を実装して C++ で証明を書いてみると、やっと、 Coq や Agda のような証明記述言語がなんでああなっているのか、細かいところが色々感覚でわかってきました。 今までもわかっているつもりでいたんですけど、やっぱり、自分でやってみると違うなあ。
というわけで、なかなか新鮮で面白かったので、みなさんも自前でやってみると面白いと思います。
"CFG⊆PEG?" Proofathon なるものを開催します！
概要はリンク先に書いてある通りで、ちょっと前にプチブームだった PEG のお話です。「PEG では書けないけど普通の文脈自由文法(CFG)では書けるような、そんな言語は存在するか？ はたまた、どんな文脈自由文法もPEGに書き直せちゃったりするのか？」という、 私の知る限り未解決の面白そうな問題がありまして、ちょっと集中して考えてみようか、という会です。
※ ちなみに、大方のひとの予想は「PEGでは書けない文脈自由言語がある」の方で、というのは、 PEG はわりと簡単に O(n) で parse 可能ですが、CFG は50年の研究の歴史があっても O(n^2) すら切れていないので、まあ O(n) になっちゃうようなことはあり得ないでしょう…という理由ですね。 私もそう思うので、そっちを証明しようと企んでいます。
そもそも日程すらちゃんと決まってないアヤフヤさですし、 何を発表を用意するとかではなくて、チャットルーム一つ用意するから後はみんな好きに駄弁ってくれ、 という適当極まりないスタイルですが、興味のある方はぜひぜひ。
