https://twitter.com/kinaba のログ (twilog の方が便利です。)
| VLDBの時きいた発表で「俺はふつうの"辞書式順序"とはちょっと違う辞書式順序を使うぜ」と言ってる発表があって理由は省略だったんだけど、今ふと #anarchyproof に使えそうな問題を思いついて3分で脳内で反証したおかげで理由がわかった。普通のは稠密にならないせいだ。ほへー | |
| HiNa 先生はリアルでもちゃんと ＞u＜ という顔をしていていただかないと忘れる | |
| @pokarim (0|1)* の文字列の辞書順で、普通は w ＜ w0... ＜ w1... （prefixになってると辞書順で先に来る）ですけど、そうではなく w0... ＜ w ＜ w1... とするそうな。 | |
| 重要なことなのですが、ペプシの新作の情報よりも新しいトマト飲料の情報の方が128倍重要ですので皆様は "〈CR134〉トマト飲料の受容性を探る女性・若年層の潜在ニーズ開拓に向けて" http://www.tpc-osaka.com/detail.php?prod_code=cr0100134 を購入して僕にレポートするべき | |
| ペプシトマト というのはどうだろう | |
| @itimasan 一日一杯のトマトジュース代を節約すれば、たったの5, 6年分で買えますよ！ | |
| 長いこと積んでいた Handbook of Satisfiability やっと読み始めた。おもしろいなー。2章の、まずそもそも問題を命題論理式やCNF、3-CNFに落とすエンコード方法にも色々あるぜというお話から始まる。 | |
| 聞けば当たり前なんだけど、ソルバによって「問題をどうSATにエンコードすると効率的か」は違う。けど、みんな無意識に主流のDPLL系のソルバを念頭に置いてエンコードしちゃうのか、作られたCNFは全然違う新しい方式には辛いものになっちゃてて、別のエンコードにするだけで全然違う事例等 | |
| CodeJam Tシャツ来てた。かっこいい。http://www.kmonos.net/wlog/sub/gcj10.jpg | |
| 左から C++, Python, Erlang, Pascal?, Java, ECMAScript, ??, PostScript?, Prolog?, Perl かな。比較が .ne. ってなるのってなんだろ。 | |
| @finalfusion @debiru Fortran ですか！なるほど。ありがとうございます。 / あと１個抜けてた。→ECMAScript→Basic→Fortran→PostScript→... か。 | |
| @gnue 左から4番目と右端は複数の解釈がありそうかなあという気がしています。右から2番目は少なくとも Prolog としてはif-thenリストとunify、として読めますけど、他にこのコード片が通る言語ってあります？ | |
| これ自分もよくハマるのだけどどうすればいいのかわからない。fixを1段だけほどきたい。#coq RT [たすけて] Coqで関数適用できなくなった http://gyazo.com/4fb3a6369023878bbe15e768a85e7093.png (via @qnighy_ 25269901031) | |
| destruct t2 して引数を全部コンストラクタ式にすれば進むから、そうすればいいのかな | |
| 書いてあった。 http://www.lix.polytechnique.fr/coq/refman/Reference-Manual006.html#toc28 "when aki starts with a constructor" なので、最後の引数がコンストラクタ式な時に限りιが進む。というわけで（無駄でも）destruct t2 が必要っぽいです @qnighy_ #coq | |
| ICFP行く準備始めてる。引出し漁って$をかき集めてて毎度思うのだけど、コインにはone dimeとかquarterじゃなく10セント25セントとでっかく書いといて下さいよアメリカさんは…（硬貨はとっさに額がわからずつい紙幣で払ってしまうために単調増加するお釣りコインの山を見つつ | |
| @heppoko_maid ふむー。そうしてみるか。 | |
| 『ギャルゲヱの世界よ、ようこそ！』予想外に面白かた。http://twitter.com/Dubhead/status/18671610633 で@Dubhead さんに教えて頂いた物。「選択肢で選ばれなかったヒロインはえらい不幸になってるよねこれ」って古典的問題があるから"現実"化した時に容易に異様な捻れが作れるんだな。ほへー | |
| だましてないよ！w http://hibari.2ch.net/test/read.cgi/tech/1281826764/165n と、それはともかく、デザインはいいから中身の翻訳早く追いつかないとなあ。Phobosの増強が速すぎてヤバい | |
| Estpolis 2 Ending Theme Vocal Arrange Version http://www.youtube.com/watch?v=7lf82I421Gg というのを知った。よいなあ。このボーカル自体はオフィシャルなものなんだろうか二次創作なんだろか。 | |
| @dark_yoshi_hpp "参加者"はいろいろじゃないですかねえ。上位には割と東大の人が多いですけども | |
| @tmiya_ fixについては結局 http://twitter.com/kinaba/status/25274942850 最後の引数を崩してやらないといけないようでした。cofixだと実際１段ほどくLemma作れというのがチュートリアル等に必ずでてきますね | |
| 今まで自分より仕事のできない人間に会ったことがないので、こう「ダメな同僚」の愚痴が書かれているのを見ると、どうも責められてる側の気分しかわからなくて、ディスプレイの前ですみませんすみませんと謝ってしまう。みんなすごいよなあ | |
| @ranha destruct x as [|[|x]]. | |
| @ranha 僕はリファレンス http://www.lix.polytechnique.fr/coq/refman/tactic-index.html をくまなく眺めて把握しました。もっと解説っぽい文書では何かあったけか…ちょっと記憶にないです。 | |
| @TKinugasa @redboltz @shnsk 自分のダメ人間度合いをネット上で覆い隠す技能についてだけは多少自信がありますよ！ |