停止性問題は決定不能→バグのないソフトウェアは作れない？ - sumiiのブログ
「チューリングマシンの停止性問題が決定不能だから、バグのないソフトウェアは作れない」という説を（アカデミックな人からも）よく聞く*1のですが、（結論はともかく）論理が理解できません。「停止性問題が決定不能 → Completeな自動検証器は実装不能 → バグのないソフトウェアは作れない」の２番目の矢印が成り立たないと思うのですが、別の意味？（もちろん、今のCoqやCharityですべての業務プログラムを記述しろ:-)とか言うつもりはありませんが） P.S. bonotakeさんからコメントをいただきましたが他の方のために：「Completeな」（バグがあれば必ずyesと答え、バグがなければ必ずnoと答える）という限定条件もついているので注意が必要です。バグの種類にもよりますが、単にsound（バグがあればyesと答える＝noと答えたらバグはない）とか、「十分に近似」とかであれば、実装可能な
論文データベースによる研究室選び - sumiiのブログ
分野によると思いますが、いわゆる計算機科学（コンピュータサイエンス）の場合、 Google Scholar (http://scholar.google.co.jp/) DBLP (http://www.informatik.uni-trier.de/~ley/db/) CiteSeer (http://citeseer.ist.psu.edu/) などの論文データベースに教員の氏名を入力して（もちろんローマ字で）、どういう学会にどういう論文を書いているか見る、という方法が研究室選びの一つの目安になると思います（マジメに研究したい人にとっては）。論文の内容や学会の名前はわからなくても、大雑把な雰囲気がわかるかもしれません。Google Scholarの「引用件数」は、その論文がどれぐらい「有名」かの目安にもなります（あくまで素朴な数値なので、いろいろと賛否や弊害もありますが）。 ただし、以
純粋関数型言語で定義できない純粋な関数 - sumiiのブログ
並列論理和の続きで真のエキスパート氏から教えていただいた話（の劣化コピー）。並列論理和は、逐次言語では定義できないけど「計算可能」な（並列言語では定義でき、領域理論でも連続になる）関数でしたが、その親戚というか兄弟です。 MLで（実はHaskellでも良いのですが）、unit→unit型の純粋な（＝副作用のない）関数は、 let f1 () = () let rec f2 () = f2 () の2つがあります。ただし、たとえ内部の実装が異なっても、外部から観察できる振る舞いが同じ関数は同じとみなします。たとえば let f1' () = try (raise E) with E -> () なるf1'はf1と同じ（かつ純粋）とみなします。 以下、「関数」としてデフォルトでは「振る舞いが純粋な関数」だけを考えることにします。すると、上と同様に、(unit→unit)→unit型の関数は l
まつもと ゆきひろ さん講演＠東大CS - sumiiのブログ
コンピュータ科学専攻 講演会 まつもと ゆきひろ 「未来の言語に大切なこと 〜動的言語の復権と将来〜」 概要：近年注目を集める言語はLispの機能を取り込みつつある。時代は1958年を再発見しつつあるのか。なぜ、今Lispなのか。あるいはなぜ今はLispではないのか。また、プログラミング言語の(近)未来はどうなるのか。Ruby開発者が独断と偏見にみちた予想(あるいは嘘八百)を語る。 日時：2006年6月13日 13:30ー14:30 場所：東京大学 理学部 新1号館 小柴ホール 連絡先：米澤 明憲 (yonezawa アットマーク is．s．u-tokyo．ac．jp) だそうです。転載に問題があったらいってください。＞御関係者
callccによる排中律の証明 - sumiiのブログ
Wadlerのパクリ。というか劣化コピー。 悪魔：「あなたが私と契約してくれたら、(A)『私があなたに一億円をあげる』、(B)『あなたが私に一億円をくれたら、どんな願いでもかなえてあげる』のどちらかをして差し上げます。(A)と(B)のどちらにするかは、私が決めます。」 人間：「どちらにせよ害はなさそうなので、じゃあ契約します。」 悪魔：「はい、では私は(B)を選びます。」 人間：「やっぱりそう来るか。でも一億円なんて持ってないし、まあいいや。」 （十年後） 人間：「気になってしょうがないので、悪いことをして一億円を集めました。だから願いをかなえてください。」 悪魔：「そりゃどうも（と一億円を受け取る）。では私は(A)を選びます。はいどうぞ（と一億円を返す）。」 ICFP 2003の会場ではWadlerとShiversが壇上で寸劇をやりました（本当）。λ式で書くと callcc(λk:¬(T
関数型言語マニアのための論文紹介５：あなたのスクリプトは「常に」正しいHTMLを生成しますか？ - sumiiのブログ
Static Approximation of Dynamically Generated Web Pages. Yasuhiko Minamide. WWW 2005. http://www.score.cs.tsukuba.ac.jp/~minamide/www05.pdf 実装はこちら↓（おそらく研究目的のプロトタイプですが、用途によっては実用にもなるかも？）。勝手に紹介してすみません。＞Mさん http://www.score.is.tsukuba.ac.jp/~minamide/phpsa/ PerlなりPHPなりで、HTMLを生成するスクリプトを書いていて、「タグが閉じてないー」とか「入れ子が合わないー」とか困らないでしょうか（クロスサイトスクリプティングは言うに及ばず）。特に、そういうバグが特殊な条件でしか起こらないときは、テストで発見するのも無理だったりします。 そこで、ス
関数型言語マニアのための論文紹介２：Packrat Parsing - sumiiのブログ
Packrat Parsing: Simple, Powerful, Lazy, Linear Time. Bryan Ford. ICFP 2002. http://pdos.csail.mit.edu/~baford/packrat/icfp02/ 「設定ファイルや専用言語のparserをYACCで書こうと思ったけど、conflictだらけになってわけがわからない」という経験はないでしょうか。それはLALR(1)という構文解析アルゴリズムがややこしいからいけないのです。packrat parsingは、すごく単純で効率のよい構文解析アルゴリズムです。大ざっぱに言うと「再帰＋バックトラッキング＋dynamic programming」だけ。YACCみたいな自動生成器もあるようですが、関数型言語なら手書きしてもno problemなぐらい楽みたいです。（Y研の卒論でC++パーザを手書きした
関数型言語マニアのための論文紹介１：Excelは関数型言語 - sumiiのブログ
Improving the world's most popular functional language: user-defined functions in Excel. Simon Peyton Jones, Margaret Burnett, and Alan Blackwell. ICFP 2003. http://research.microsoft.com/~simonpj/Papers/excel/index.htm 要約すると「Excelは関数型言語」ということです（わりと本当）。私を含め、ICFP 2003（関数型言語に関する国際会議）のプログラム委員たちを爆笑困惑させました（やや本当）。 こんな感じで「ポインタ＋一言」で論文紹介（というほどでもないですが）を続けてみようかと。英語が苦手でなければ1本30分ぐらいで斜め読みできると思いますが、別に「読め」というつもりで
思いて学ばざれば則ち殆うし - sumiiのブログ
あるところに同じようなことを（ほとんど成り行きで）書いたのですが、重要な問題のような気がしてきたので、こっちにも書いてみる。 一般に、関数型言語やプログラミング言語（および計算機科学、ないし任意の専門）についての情報は、 一般書・一般誌、Webやメーリングリストやブログ 教科書・専門書 論文 口頭での議論（学会発表や質疑応答、グループのミーティング、部屋での会話） などで交換されます。 で、一般に情報の「ディープさ」は上から下へ行くほど濃くなると思うのです（少なくとも僕の専門分野ではそう）。そのごく一部である1.だけ（しかも日本語onlyで）「勉強」していろいろと議論するのは、（何もしないよりは良いのかもしれませんが）非常に危険です。その危険をちゃんと意識していればno problemですが。「高速道路」の話と同じことかも。 たとえば、日本のネット(?)では今になって妙に持ち上げられている
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
