https://twitter.com/kinaba のログ (twilog の方が便利です。)
| http://homepage1.nifty.com/herumi/diary/0904.html#29 もとの僕のコードはiをシーケンシャルになめているけど、コンパイラがあれをiをシーケンシャルになめるコードにコンパイルする必要はどこにもないので、それは問題にならないかなあと | |
| 現時点でも順序非依存に実行して良いことは(maxの結合則から)十分推論可能ですし、100年後の超絶賢いコンパイラなら本当にまったく問題ないと思ってます、というか100年後でなくて1億年後でもいいのそのレベルの賢さを想定すると言うことで… | |
| 「殆ど定義の同義語に戻る」のが(超絶賢い)処理系にとっては一番楽だけど、プログラマにとってそれは決して楽ではないと思うのでそれを避けたい、というのがたぶんほとんどの人に同意されないけれど僕が思っていることで、 | |
| 現行のアルゴリズム記述の何か延長線上にあって、なおかつ、定義と論理的には同値な記述を可能にするプリミティブが欲しいなあ、という。（非決定性なしでは論理的に同値な記述はできないし、逆にあれば可能だし、論理的に同値なら超絶賢いコンパイラは元々の定義を書いたのとどうように最適化しうる） | |
| うーむむ | |
| 四色問題といえばどなたか [PDF] research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf を3行とは言わない3ページで頼む | |
| @camlspotter おおーそんなつながりが＞Gonthier。 | |
| 途中で眠くなって読むのに挫折している論文リストとか作るか。なかなか思い出せんけど | |
| mokehehe さんが LT されるとか http://atnd.org/events/580 。楽しみだ。なんか自分も後に続きたくなったけど何もネタがないというか、この慢性アウトプットできるネタのなさはそろそろやばいので死んで反省すべき。 | |
| Purely Logical Data Structures は面白そうだなあ | |
| Unranked Zipper in LP というか http://arxiv.org/abs/cs.PL/0406014 に僕の卒論が丸かぶってたことにしばらく前に気づいてびびったぜひゃっほーシラネーみたいな話はある | |
| @dangoyasan maxという特定の例はそれでよいかもしれないんですが、例えば次のエントリで例に出したマージソートや、http://twitter.com/kinaba/status/1637259471 で上げたトポロジカルソートはどうでしょう？ | |
| @dangoyasan 世界に存在する全ての問題に対してランタイム関数を用意するわけにはいかないので、どこかで必ず汎用のプリミティブが必要になると思います。（もし、（僕のように）、非決定性が欲しいならば） | |
| そのためのプリミティブとして最適なのは、配列/リスト/集合に対する非決定的な任意要素取り出しだったり巡回だったりである、ということはおおいにありうると思います（というか、いただいたレスポンスはだいたいそれでした。僕がひとり納得できていないだけ、という） | |
| 光成さんに整理していただいた不満点 http://homepage1.nifty.com/herumi/diary/0904.html#30 はまさにその通りです多謝 | |
| @ikegami__ 「AはBをソートしたリスト」って定義をちゃんと書くのって至難の業だと思うんですよ。いや、至難ってほどでもないですけど、選択ソートやクイックソートという具体的なアルゴリズムなら20秒あれば書けるのと比較するとかなりしんどいと思う。安定ソートとかもっとキツい | |
| それでこの差はわりと本質的なような気がしている←いまここ | |
| もちろん(constructiveな)whatはhowと解釈できるしhowはそのままwhatと解釈できるので、何が"定義"で何が"アルゴリズム"かはわりと曖昧なんですが、そこはなんとなくそれっぽく適当に分別を | |
| アルゴリズムに非決定性をいれられれば＆超絶賢いコンパイラを仮定すれば、たとえソートの定義を書かなくても、選択ソート（あるいはもっと頭使わないで思いつけるすごいお馬鹿で自明なソート方式）から最速のコードが出せる（非決定性が無ければどんな神コンパイラでも無理）てことを最近考えてた |