https://twitter.com/kinaba のログ (twilog の方が便利です。)
| しかし、SAT/SMTソルバ屋さんが猛烈に頑張ってて高速なので俺は問題をencodeしてブラックボックスとしてソルバに突っ込めば終わりだぜ、という解き方は面白みがないなーという感想を抱いてしまうところがなくはないので | |
| 最先端のソルバの使っているヒューリスティックスを言語機能として猛烈に簡単に表現できるようにした、対NP困難問題最終兵器みたいなDSL、SMTよりもっと低水準なの、を作ることで、エンコードを経由せずに直接的に速いアルゴリズムを表現できるようにならないか、みたいなことを妄想している | |
| つまり僕はSATソルバひとり勉強会をさっさと再開するべきであり | |
| stomach.isEmpty | |
| 査読キューを明日までに0にしなければならないがやる気が出ないので神保町をさまよいに行くか | |
| boolを定義するには、trueとは何であってfalseとは何であるか教えて貰えれば定義できるので、「それ(t と f)を引数に渡して教えてくれたら定義してやるぜ」 というのが TRUE=λtf.t FALSE=λtf.f http://www.kt.rim.or.jp/~kbk/zakkicho/11/zakkicho1101c.html#D20110121-2 。 | |
| ペアを定義するには、ペアを作る関数make_pairをく教えてくれれば定義できるので、それ(m)を引数に貰って PAIR(x, y)=λm. mxy。リストならnilとconsを貰えればわかるから NIL=λnc.n CONS(a,d)=λnc.cad。自然数ならゼロと+1を… | |
| 要は 「そのデータ型の値を全部作り出せるようなプリミティブ（true, false, nil, cons, 0, +1, ... など） を引数として渡したら、それを使って値を実際に作ってくれるようなファクトリ関数」 のことを、「値」と見なしてλ計算の中で使うスタイル | |
| [1,2,3] というリストは λnc. (c 1 (c 2 (c 3 n))) みたいな。 | |
| 「CONS(a,d)=λnc.cad」これ嘘だ。λnc.ca(dnc)だな | |
| ああそうか。面白い。 http://cstheory.stackexchange.com/questions/4473/techniques-for-reversing-the-order-of-quantiers "In fact, compactness is at the heart of quantifier reversal." こういう風に色んな概念を消化したい | |
| また貼るURLを間違えた… | |
| 「なぜ我々 complexity theorists が ACC^0 ≠ NEXP という結果にこんなにも萌え転がっているのか (意訳)」 みたいな解説記事を見かけたような見なかったような記憶があるんだけど、どこだっけ。 | |
| 見つけた。これだ。 http://blog.computationalcomplexity.org/2010/11/is-ryans-theorem-only-interesting-to.html | |
| ねむい、ねむむい、ねむむむむむい。 | |
| @finalfusion 難しく言うと、http://en.wikipedia.org/wiki/Initial_algebra です。"bool型の値とは「2個選択肢があるうちの、選択肢の１つ」というシチュエーションを一番抽象化して表現したもの、なのである！！" と考える派閥 |