https://twitter.com/kinaba のログ (twilog の方が便利です。)
| えっMac版のCoqIDEはこんなニワトリ右上に出るのか！バージョンの違いかな http://www.iij-ii.co.jp/lab/techdoc/coqt/ #coqt | |
| 実は @akane_magica さんのid変化に全く気づいてなかったのだが http://twitter.com/#!/Cryolite/status/54909528478715905 この文脈に出現するid名が僕の想像と違うなーと思ったら違ってなかった、という気づき方をした | |
| 僕の脳内に存在する「λ計算とか型推論とか名前はなんとなく聞いたことがあるような気がする」「定理証明とかいいからプログラミングの話をしろ」辺りのゾーン向けに、dependent typeとは何であるか読んだ人が茶飲み話1回の小ネタにできるレベルの普及を試みる、という原稿を書いている | |
| と表明することでプレッシャーをかける試みですが進みませんひー | |
| @pi8027 がんばりますん | |
| 『煙滅』 http://amzn.to/8DwDsF 読んでる。"e"の字を使わないというフランス語の原著を「い」の段を使わないという日本語に訳しているという翻訳なのだけど、突然群論の話をし出して長々と並べた等式の最後の右辺がない物が書いてあるという場面で、でもこれ単位元になる式 | |
| なので消えているのは単位元を表すのに通常よく使われるeのはずで、右辺を消すのは誤訳じゃないかなあ、というか、そもそもここは複素数の話かなんかに丸ごと置き換えるのが正攻法なのでは、とかそういうところを気にしながら読んでいるけど結構おもしろい。 | |
| @pi8027 すみませんeが消えました。ありがとうございます！今修正しました。 | |
| @ratbeta 残像に口紅を、ですね。面白いですオススメ。使える文字が減っていくという無駄に縛りをかけた状態でなお物語として語るべきものは何かとかメタな話をバカらしくしている辺りとかが好きですが、他にもいろいろ楽しいです。 | |
| http://twitter.com/#!/kikx/status/54821462065938433 これ気になってた。自分の体感覚としてどうだろうと考えると、視覚に依っているせいで眼球/視界の後ろに意識があるような気分になっている気はするんだけど、これは先天的な感覚なのか否か | |
| @eomole http://dx.doi.org/10.1145/244795.244798 計算モデルにもよりますがlog n倍のオーダで遅くならざるを得ないという結果が。二分木っぽい構造で配列(とメモリ管理＆ポインタ)を全て置き換えれば機械的にlog n下げで止められそう | |
| @cocoatomo それが http://en.wikipedia.org/wiki/Heavy_legs とか、"肩こり"もそうなんですかね、我々が既にそういう概念を持っているから引きずられてそういう器官だと考えやすくなってしまった後なのか、難しいところかもなあとか |