2009年世界大学ランキング by Times Higher Education/QS - sumiiのブログ
ちょっと遅いですが、 http://www.timeshighereducation.co.uk/WorldUniversityRankings.html (目次) http://www.timeshighereducation.co.uk/Rankings2009-Top200.html (総合) http://www.timeshighereducation.co.uk/Rankings2009-Top50-IT.html (工学 & IT) (via いろいろなところ) 人間による評価なので(?)多少の疑問はあるかもしれませんが、ほぼ実感と一致しているように思います。（分類が大きすぎるので、可能であればもっと細かくわけてほしいところですが）
クレタ人のパラドックス - sumiiのブログ
ある理由で「論理学」（野矢茂樹著）*1を（時間的余裕がなかったので極めて速く）読んだ／眺めたのですが、その161ページに なお，流布した誤解に，「あるクレタ人曰く，『クレタ人はみんな嘘つきだ』，この発言は矛盾している」というものがある．しかし，これは別に矛盾ではない．（検討されたし．） （強調筆者）とあり、なるほどと思いました。（有名事実なのかもしれませんが、私は恥ずかしながら考えたことがありませんでした。あるいは聞いたことがあるのかもしれませんが、覚えていませんでした。） P.S. 同じ著者の「論理トレーニング」も良い本でした。 *1:専門書ではなく（素晴らしい）入門書ということになっていますが、このように（私にとっては）自分自身の良い勉強にもなりました
第２回プログラム等価性クイズ - sumiiのブログ
たまには自分の研究に関係がある（かつ専門家以外にもわかる）話題ということで、プログラム等価性(program equivalence)に関して書いてみます。プログラム等価性というのは「二つ（ないし二つ以上）のプログラムが等価」という性質のことで（そのまんまやんけ！）、「等価」の粒度によって様々な「プログラム等価性」があります。その中でも 任意の文脈（プログラムの「使い方」や「呼び出し方」のようなもの）Cにおいて、C[P]（文脈CにおいてプログラムPを実行する計算）が停止するならば、C[Q]も停止するし、逆も成り立つ というプログラム等価性を文脈等価性(contextual equivalence)と呼ぶことがあります。 例えばJavascript風*1の命令型言語で、 function f1(g) { var x = 1; g(); return x+1; } という関数f1と、 func
操作的意味論 vs 表示的意味論 - sumiiのブログ
http://d.hatena.ne.jp/ranha/20090615 (via http://d.hatena.ne.jp/yad-EL/20090615/p2) 「諸君らの愛した表示的意味論(R5RS)は死んだ。なぜだ?」 う、これは私も（というか私ごときでは）迂闊に発言できないテーマです…。Scheme (R5RS → R6RS)に固有の事情は知らないので、（もしあれば）メーリングリストなどでの議論を検索したほうが詳しいかもしれません。追記：R5RSの操作的意味論と、その表示的意味論に対するメリットに関しては論文があるようです。 迂闊に発言すると、（一般論としては）「操作的意味論のほうが理論が簡単だから」だと思います。要するにプログラムの「意味」というより「動作」を状態遷移（式の書き換え）で表しているだけなので…。歴史的には、操作的意味論も（仮想機械やインタプリタによる定義から）項
「コンピュータソフトウェア」誌 ソフトウェア論文＆小論文 - sumiiのブログ
「面白い研究をしているのだが論文（業績）にならなくて困る」という声を立て続けに*1耳にしたので、コンピュータソフトウェア誌の「ソフトウェア論文」と「小論文」カテゴリを（しつこく）宣伝します。掲載は有料ですが、発刊数ヵ月後にはオンラインで無償公開されます。 http://www.jssst.or.jp/prod/software-papers.html ソフトウェア論文は従来の研究論文と異なり，どのようなソフトウェアについてどのような観点から論文を執筆すれば学術論文として認められるかに関して十分な社会的合意があるわけではなく，このことがソフトウェア開発の論文化の妨げとなってきました． 本「ソフトウェア論文」特集はこの問題を打破すべく企画したものです．優れたソフトウェア成果を積極的に論文化してご投稿いただき，編集委員会での議論と査読・改訂のプロセスを経ることによって，「良いソフトウェア論文」に
ケータイ小説 計算機科学入門 第2話 - sumiiのブログ
定義だけなら サルでもできる 理論は例と定理が命 有限状態オートマトンの例 入力として 0と1の列を考える 自然数nを2進数で 大きい桁から順に書いた列よ nが3の倍数かどうか 「計算」するオートマトンを作るわ 状態集合Qは{q_0, q_1, q_2} つまり状態はq_0, q_1, q_2の3つ 現在の状態がq_iだったら それまでの入力列が表す自然数nを 3で割った余りはiになる そうなるように 遷移を定義するの 例えば現在の状態がq_2のとき それまでのnを3で割った余りは2 そこに入力0が来たら 2進数の下一桁に0を付け加えるのだから nは2nに変化する nを3で割った余りが2ならば 2nを3で割った余りは1だから 状態はq_1に変化する つまり q_2 ---0---> q_1 状態q_2に 入力1が来たら nは2n+1に変化する nを3で割った余りが2ならば 2n+1を3で割
ケータイ小説 計算機科学入門 第1話 - sumiiのブログ
なんでこんなキモい話書くの？ 計算機科学（コンピュータサイエンス）にも「常識」があるンだけど 現代人は忙しいし ましてや技術者はデスマーチ （研究者でもいるけど） 大学の授業受けたり 教科書とか読む暇ないでしょ（書く暇も） 情報とか計算機（コンピュータ）とか Computer = 日本語では計算機だけど 1+2=3みたいな計算だけじゃない 「情報」を処理することはみんな「計算」 情報って何、とか言い始めると哲学になっちゃうけど 知識の表現ってことにしておいて だから文字や文章はもちろん 画像とか音声・音楽とかも情報 計算モデル 「計算機科学」だから 計算機（っていうか「計算」そのもの）について「科学」するんだけど いちいち電子回路から考えてたら大変だし 古来、「計算（機）」は電子回路だけじゃないの 本質を明確にしたいから抽象化＝一般化して 数学的なモデルを考えるわ 有限状態オートマトン 一
停止性問題は決定不能→バグのないソフトウェアは作れない？ - sumiiのブログ
「チューリングマシンの停止性問題が決定不能だから、バグのないソフトウェアは作れない」という説を（アカデミックな人からも）よく聞く*1のですが、（結論はともかく）論理が理解できません。「停止性問題が決定不能 → Completeな自動検証器は実装不能 → バグのないソフトウェアは作れない」の２番目の矢印が成り立たないと思うのですが、別の意味？（もちろん、今のCoqやCharityですべての業務プログラムを記述しろ:-)とか言うつもりはありませんが） P.S. bonotakeさんからコメントをいただきましたが他の方のために：「Completeな」（バグがあれば必ずyesと答え、バグがなければ必ずnoと答える）という限定条件もついているので注意が必要です。バグの種類にもよりますが、単にsound（バグがあればyesと答える＝noと答えたらバグはない）とか、「十分に近似」とかであれば、実装可能な
クリスマスプレゼント？ - sumiiのブログ
長男がなぜかロボットを怖がる。ついこの間もディズニーストアに展示されていたWALL-○を見て硬直。「○ALL-EかわいいよW○LL-E」と動かして見せようとしても、遠巻きにするばかりで近づこうとしない。しまいにはイタズラや悪いことをしたときに「良い子にしないとWA○L-E買ってくるよ？」と言ったら「良い子にする！」と態度が一変する始末。「ゴーリーどこ？（まだウォが言えない） いない？」と気が気でない様子。
論文 - sumiiのブログ
久しぶりにfirst authorというか単著の論文が通りました。幸い今回はexpertにreviewしてもらえたようで、「現代のプログラミングにfreeは不要」*1とか「簡単すぎる」*2とか「プログラム例がSchemeなので読めない」*3とかいった妙なコメントもなく、最高の評価をいただきました*4。と自画自賛。 http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/non-mono.pdf We develop a general method of proving contextual properties---including (but not limited to) observational equivalence, space improvement, and memory safety \emph{under arbitrary contex
定理証明支援器「Coq」によるプログラミング言語理論の定式化チュートリアル - sumiiのブログ
http://www.cis.upenn.edu/~plclub/popl08-tutorial/ POPLに併設されていたので参加しました。CoqでTAPL序盤（単純型つきλ計算まで）の理論を定義・証明する、という内容。主催者（PennのPLClubの人たち）に聞いたら、先週金曜のカウントで参加登録者67名とのこと。予想は30名程度だったそうなので盛況のようです。 いつも偉そうなことを言っておいてアレなのですが、Coqは話を聞くばかりで、実は触ったことがなかった(!)ので、非常に勉強になりました。隣のA氏（エキスパート）からいろいろと教わりながら聞けたので、さらにナイスでした。:-) さすがに時間不足で説明は駆け足でしたが、ホテルに帰ってから最後（型安全性の証明）まで練習問題をやってみました。カリー・ハワード同型とTAPL序盤程度の知識があれば、上のURLにあるソースコード(coq-tu
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
エルドス数計算サービス - sumiiのブログ