むやみやたらと夢に出てくるような人は信用できない。
どうでもいいがオモロシイメールがきタ:
なんじゃこりゃ? 「オラゆうすけ」だと? ハテな、オラホウじゃ“オラ”なんて一人称は使わねえんだけんよ。 これはなにかの間違げえだすけ。(←オットこりゃ新潟弁だ。)Date: Sun, 31 Oct 2004 08:27:21 +0000 From: yusuke <yusuke@cs. . > Subject: ola yusuke como vc esta To: yusuke <yusuke@cs. . >
予告どおり、帰りは WTC 駅を使った。Broadway をずっと下っていくと、 やはりところどころに莫迦者がいた。 ああいうのはさあ、小学生ぐらいのガキが「ちゅっかちー!」 ("trick or treat" を舌足らずふうに言うとこう聞こえる) とかいってる程度が いいんであって、いい歳したオトナがやっててもおかしいだけだぜ。 しかしさすがに Canal St. より南へいくとそういう人は少なくなる。 っていうか、そもそも人自体が少なくなるのだが。それに道も暗くなるし。 WTC 駅へ着いたら、これがあの同じ駅とは思えないほどに閑散としていて、 これでも日中は必ずフェンスごしに焼け跡(?)の写真をとってる 観光客がいるはずだが、ほとんど誰ぁ〜れもいない状態になってた。 もともとただでさえ構内がスカスカしてるのに。おまけに全部コンクリートっぽい 配色のために、ほかの場所よりもいっそう閑散として見える。 しかし、おかげさまで電車はラクに座れる程度。 ほんとーはチャイナタウンでメシを食おうかと思ったのだが、 いまだにマックで腹がもたれているので食欲なし。うげー、こりゃほんとに毒だは。 これはなんかお腹をイタワル物を食わねば…
というか、halloween みたいな仮装のなにがイヤかっていうと、 その味の薄さである。たしかにコスプレの中には 手間かけたようなのもあったが、基本的にみんな何の思想もない。 ただ、なんか目立つ服装しているだけって感じが、どうにもムカつく。 結局こういうのを喜んでやるのはアメリカ人って感じがする。 大味っつうか。連中の調味料はじつに限られている。 ようするに量が多けりゃそれでいいと思ってるのだ。
ちょっとttoおもってみただけでsuuu-----〜〜〜
ぼくのせえjaaaaありませeeee--〜〜〜n
ああ、それはあれだ、さしずめあれだ、
いかん、影響さえrすぎだ。
ホーチキ? (じつはなんとなく語感がよいので気に行っている会社名)
パレードはあったのかどうかわからんが、あまり混雑はなかった。 駅にはあいかわらずアホな格好をした莫迦者 --- この言葉を使うとなぜかなんともいえない アホらしき笑いがこみあげてくるのを禁じ得ない、なぜならここには「オレこそが常識人の代表だ」 みたいな響きがあるからだ、まあ、実際にはオレも別の種類の莫迦者にすぎないので、 ここからは「自分のことを棚にあげて好き放題いう」って態度が見えかくれし、つまりそれは 墓穴掘りだ、オレはそういうのが好きである --- が数人から数十人のレベルでいたが、
…書いてるうちに書くこと忘れたのでここで打ちきるのであります。 まあ、これぞ、インクリメンタル (漸進的) ど忘れ、ということで、あの、
テビレ (=てれび) を買いましたのです。といっても買ったのはテレビ受像機じゃない。 PCI カードである。とくに見たい番組があるわけでもないのだが (Aqua Teen と South Park ぐらい、あと Weather Channel)、 comcast のテレビ代を払っているので、見なきゃもったいないかな、と思って。 Amazon で $30 ドル (?どる 30 どるって?) ちょっとだった。 箱テレビを買ってしまうと置き場を考えねばならないが、カードならつっこんどきゃいいわけだから、いい。 説明書も読まずに適当につっこむ。どうやって使うか? video4linux をインストールするのである。Windows がないので、 正規のドライバで動くかどうか試すことはできない。いきなりカーネルの再コンパイルから始まる。 そのご xawtv。おい、チャンネルがおかしいぞ? と思ったら、PAL だった。 設定ファイルを書く。しかし、いつまでたっても音がでないので、おっかしーなー、 alsalib は enable したはずだし、mixer も音量上げてあるのに…。web をみても何も 情報が見つからない。と思ったら、じつは TV カードには音声をキャプチャーする能力がなく、 この背後から出ているオーディオ出力をサウンドカードのライン入力に つないでやらねば音は出るはずないのだった (ケーブルは付属している)。 新山はさいしょ、tv キャプチャーカードが音声もデジタイズしてくれるのかと思ったのだが、 それはサウンドカードの仕事ってわけね。しかしオレは今世紀最大のアホである (まだ 04年なのに! もう! すでに今世紀最大の月蝕!)。こんなこたぁーセットアップ説明書を 読めばすぐにわかることなのに。説明書よまない君 (くん)。 ちなみにアプリケーションはただ tv カードにコマンドを送っている だけらしいので、まったく CPU を食わない。X のなんたら extension を使うのかと思ったら、 画面上に直接レンダリングしてるらしい。だから suspend しても動画は動いている。 音声はずっとたれ流しで、xawtv を終了してもまだ続いているので (今どこのチャンネルを見ているか、 といった情報はカードが保持しているらっし)、手動で入切せねばならない。結局、shellscriptを書いた。 しかししかしとにかくすごい! これぞ今はやりのマルメディア! 多媒体電脳ですよ! ナウいね! しかも中にヒトが入って、絵が動いてる!! どういう仕組みだ?? すごいのは自動チャンネルスキャンやら何やらの機能があることと、 録画機能があることだが、それ自体はあんまり興味ない。むしろオレ的にすごいと思ったのは ntsc-cc というプログラムで、これを使うと closed caption を標準出力から出せるのである! これを使えばテキストいっぱいとれそうだな。こんなんをいじっていたので昨日の夜中は 他のことがまったく手につかず。
それはそれはそれはそう。
と自分がこうだから、他の人もこうにちがいない。 そうに決まっている。 こう考えない奴などこの世の中に存在するはずがない。
では、自分はこうだけど、他の人は絶対違うだろう。 そうに決まっている。 こう考える奴など自分以外に存在するはずがない。
前者のほうがはるかに穏健で礼儀正しくかつ安全な考え方だろう。 オレはあとのほうだけど。
(「ふつうは『アメリカ白人』というよね」などとツっこまないあなたは、もちろんいい人)
(Ohta) FUKUI-SAN, THE IRON CHEF
HAS NOW ADDED OCTOPUS
TO ONE OF HIS DISHES,
AND IF YOU'RE WONDERING
WHETHER THAT GOES WELL
WITH PUMPKIN, HE SAYS,
きのう、またセキネさんと不毛な (でもないが…これまでの経緯じたいにかなりムダがあったような木がするので、 それが終了したのは有意義というべきだが…) 議論をして、とりあえず評価方法については 一定の結論がでた。いまの今までなにをブーたれていたかというと、「言い換えの定義」についてである。 「言い換え」というのは、文字どおり表現を入れ換えても意味がたいして変わらないような日本語 (あるいは英語) 表現 (の対) のことだが、この「たいして」というところに大きな穴があり、たとえば米軍がイラクに 物理的に“移動”した (これ自体はほとんど疑いがない) ことをさして、 「イラクの侵略」と呼ぶのと、 「イラクの解放」と呼ぶのは、はたして本当に言い換えなのか? といった問題がある。で、言語学者はこれらの差異をいろいろなタイプ (価値判断が入るか否かとか) に 分類しているのだが、そこまで考えだすともう手のつけようがないので、やらない。 とすると「言い換え」をうまいこと定義をせばめて、もっと厳密な判断ができるように してやる必要がある。さて、ここにもうひとつの問題があって、いまの新山の研究テーマでは、 言い換え表現を最終的に情報抽出に役立てるべし、という縛りがある。そして現在の情報抽出の 主要な問題というのは、どうやって対応できる記事の種類 (「ドメイン」と呼ばれている) を増やすか、 ということで、当然ながら新山の研究もその目的に貢献しなければならない。そうすると 「言い換えの定義」というのは、あまりに狭すぎてもダメなわけで…。 「情報抽出に役立つような言い換え表現」をどうやって定義するんだ、ということで、 いままでさんざ悩んでいたのだった。おまけに、これらは数値評価できるようなものが望ましい。 そうするとなんでも数字を比べりゃいいので簡単だから (もちろん、個人的にはこんな手法は敗北だとわかりきっているが、論文書くためと割りきっているので)。 で、さらにいうと評価は自動的にできるようなものが望ましい。これは、実験をするたびに 毎回人間が結果 (何百ページとある場合だってある) を検査しなけりゃいけないのはイヤだってこと。 そうするともう、ああやってもダメ、こうやってもダメで…。 ドメインをある程度限定すれば、きっちりいうことはできるのである。 しかしニュースの種類は (潜在的には) ほぼ無限にあるということで、それを否定すると うちのプロジェクト自体が成立しなくなるのでこれまたダメなのだ。どすりゃいいの?
で、きのう出た結論は「言い換え表現というものは、クラスタ化するはずだ」というものであった。 つまりある程度の「よく似た表現の集合」というものがあり、それが情報抽出に役立つかどうかを 調べればよい、ということである。でも「情報抽出に役立つかどうか」は、獲得した表現から 人手で判定するしかなく、これだと完全に自動的に評価できるわけではない (クラシックな統計的手法というのは、あらかじめ決められた基準でつくられた 「正解データ」がすでにあって、実験の精度はそれと結果をくらべるだけ、というもの、ラクでいいんだわ、これが)。 しかし「表現の種類は無限にある」という仮定をしている以上これよりうまくはできそうにない、 という意見になった。まあ、どっちの変数を固定するかって話だけど。 ということで評価方法についてあれこれ悩むのはやめて、結論は「とりあえず実験してみて、 それから考える」ってのと似たような話になったわけだな。はあ。
原因は、iTMS で音楽を買いすぎたためである (といってもまだ 4曲だけ)。 これ PowerBook 以外の場所でも聴きたいよなあ、と思いはじめると、 iPod を買うしかない。 したがって、べつに「写真つき」のが欲しいわけではない。別に mini である必要もない。 フルいやつでいいのだ (あ、でも mini のほうが安いのか、いまはもう品薄じゃないのかな?)。 でもそういって、結局は買わずに我慢してしまうことのほうが多いのだがオレは…
todo: はあう゛茶きらした。かうこと
(追記) てくるで、きょうの competition もまた負けたが、じつは 20分ぐらいしかプログラムに費やしてない (ほとんどランダム) んだから当たり前だ。かわりに来週のアーキテクチャのプレゼンをした。 そしたらみんなヘンな顔をしていた。なぜなら新山は通信プロトコルをマルコフっぽい確率過程として モデル化していたからである。まあ、だいたいオッケーということにはなったが、 先生からは「いかにも自然言語屋らしい」と言われてしまった。ふつう計算機屋は何もかも離散的として 考えたがる傾向があるらしい。それはあるかもね。しかし、オレもずいぶん“統計的”手法に 影響されてきたということであろうか。こういう統計的なモデルは、それ自体ではべつに 嫌いじゃないのだが、言語処理 (とりわけ低レベルな形態素解析とか) に応用するのは あきらかに狂っているという確信がある。もちろんこれに対する人々の答えは 「役に立つ (=性能が上がる) からいーじゃん」というものであるが、この手の解析性能をあげたところで 実生活にはなんの役にも立たない (その先に使えるものができていないので) ということは誰も言わない。 しかしまあ、これは株価のくだらない予測方法を「役に立つ (=儲かる) からいーじゃん」といってる 人々と同じ現象と考える。聞いたところによると、テクニカル分析もべつにたいした理論が 背後にあるわけではないそうな。世の中、アタマが余っているんだね…
夢の中で、なにやらガッカリすることがあった。 そんな人じゃないと思ってたのに…。demo、Dare dattanokaOboEtehainai. おまけにそいつの何に対してガッカリしたのかも今となっては謎である。 ただ「ガッカリした」という記憶、感触のようなものだけが残ったのだ。
まあ、あるいはそれはもしかするとオレ地震なのかもしれないが。
つまんないんだよ!
語数を多くしてもつまらんものはつまらん。むしろむやみに長いほうが 面白い部分が薄められて平均的つまらな度が上がる。だから、。
てくるで、「〜がものを言う」とか「〜にものを言わせて…」という 言いまわしは英語でもあるんだろうか? きょう "money talks (世の中、カネがものを言う)" という表現をみてちょっと思った。
http://ll4.ai.mit.edu/
http://www.python.org/~jeremy/weblog/041010b.html
ボストんの YH 予約しとっか。しかし今年は 12月かよオイオイ寒そうだなあああ
そういえば今晩は皆既月食があった。東海岸一帯で見えたようだ。 帰りぎわに 5av. + 9st. の交差点で、あらぬ方向 (上のほう) を眺めて立ちどまっている おじさんがいたので、一瞬ビル火災かなにかかな? と思ったら、そのおじさんは月を見ているのだった。 ちょうど半分ぐらい欠けたところだが、月食だということはすぐにわかった。 なぜなら、ふつうの月の満ち欠けと違い、影になっている部分もうっすらと月の灰色の輪郭が 見えていたからである。ふーん、と思って、そのご Journal Square に帰ってきてみたら、 駅を出たところの広場にも 10人以上の人々が立って空を見ていた。 もう 7/8 ぐらい隠れたところだ。そのご、ゆっくり歩いてきて、アパートの前で 全部隠れるまで見届けてから部屋に入る。皆既になってからも月はぼんやりと見えていた。 薄雲がかかっているときの月に似ているが、色が赤い。 暗いので月面の模様がいつもより目立つようだ。
月食も eclipse っていうのかな? 地球は月よりずっとデカイので、月食は日食よりも起こりやすいのだろう。
ふと検索でひっかかったどうでもよさそうな日記を読み、 「なんてイタい日記だ!」と思った。
ところがその後自分の書いた日記 (↓これ↑) を読んでみたら、
大してかわらない口調だったのでガッカリしてしまった。
というか、オレは爆発した口調じゃないと自分で読み返しても面白くないものになる。
というか、というか、この 2、3日あまり爆発した日記を書けていないような気のするは、
これは、忙しいためで、火薬がシケってきたためなわけでわ
ない。
ないったら。しかし爆発はナムいとき (なにこれ、打ちまちがい、ネムいとき) には
威力が弱まる。でもこの 2-3日やけにネムいのよ意味もなく意味もなく意
味。
だからさ。
もしかするとこれは寝すぎ病 (そんなものがあれば) じゃないのか?? ああ、秋ですわねえ。
そういう意味でいえば「Prolog 使え」としつこく言っていたタナカ先生は 圧倒的に正しかったのかもしれない? しかしいくら GC があってもさすがにあんな言語は使う気になんないな。 てくるで (ところで)、Lisp 信者はいまだに現存するし密教的儀式をやっているのも目撃したが、 Prolog 信者ってのは (タナカ先生を除いて) ほとんどお目にかかったためしがないな。
まえに heow が言っていたが「(何年か前までは) オレたち Lisp ファンは ほとんど 70年代のゲイと同じような虐げられた者としての感覚があった」という。 わさこんわさこん
2つのプログラムを交互に作る。 一方が飽きてくるたびにもう一方にスイッチし、両方飽きた場合は暇つぶしに翻訳をやる (はて、なにを訳しているんでしょう?)。 来週の heuristics algorithm は新山が「戦場係」だが、1週間前 (つまり今週中) には準備して アーキテクチャを発表せねばならない。しかし今回のゲームは動的な対戦モノではなくて、 静的なパラメータを与えられて解くパズルであるため、リアルタイム性はない。 つまんないの。ところがそう簡単でもない。 今回のお題は「盗聴されないような通信プロトコルを設計せよ」というもので、 じつは評価するほうが大変なのである。まずフレームワークをきめて、 与えられたプロトコルを破るための分析を自動的におこなうコードを書かねばならない。 しかしあんまり手のこんだ枠組みにするとそもそも分析できないため、ある程度単純なものに、 それでもパズルはそれなりにむずかしく、という注文。 なんだかかくれんぼのオニになったような気分だ。
ホイマシペーター!!
てくるで (ところで)、「ホイマシ」ってかなり謎なネーミングセンスだと思うんだけど (マイワシに似ている)、「ペーター (Peter)」ってドイツ語っぽいから やっぱ「ホイマシ」もドイツ語圏の名前なぬかな? しかし欧米でおもしろいのは、 言語はちがってもみんな同じキリスト教圏の名前を使っていることである。 英語の Peter が、ロシア語で「ピョーーーーーーーーーーートル!!」だと知ったときはショックだった。 John がヨハンだとか、Elizabeth がイザベルになるのはまだいいのである。 ピョーーとるですよ、ピョーーーーーーーーーーートル!!! (この語感が好きらしい) キリル文字でかくとПоторになるぬだろうか? まあそれにしてもオレのセンスもそうとうヘンだがな。まあいい。もうねるころだ。 教は駿きしたので明日は速くねよう、世の中もうだいたいそうなっている。決まってら
なぐっても なぐっても 悪くなる アタマ
こんなのにインフラを任せている国はいつか滅びる。 べつに滅びなくてもどのみちオレが嫌いだからそれでいい。Microsoft VBScript compilation error '800a0411' Name redefined /ForYourHome/includes/footer/eDeskLogAppender.asp, line 4 dim guid ----^
From: Anina We're scheduling this semester's meeting for Monday, November 1, in room 1302, Warren Weaver Hall. Lunch will be provided at 12:15, and we'll begin the meeting at 12:30.
新しい部屋はこぢんまりしていて好きなのだが、こまったことは日当たりが激悪いということだ。 おまけに風通しも激悪い。まあ、日当たりがよくて風通しもいい一人部屋なんてそうは ないだろうけど。f
まあそんなことはどうでもよいんだけれどもさ (すっかりまたもとの口調に戻ってしまった)。
ベジタリアンの店では玄米を出すところも多い。日本と同じように、 ここでも玄米はなんか「健康にいいもの」と考えられているようだ (脚気、脚気!)。 しかし、その食い方が…。新山はこっちへ来てスゲーひさしう゛りに玄米などというものを 食したのだが、炊いたゲンマイがドレッシングと一緒に出てくるのである。 ようするに、これで食えと、いうことらしい。連中にとっては玄米は野菜みたいなものなんだろうが、 米国で菜食主義が拷問のごときモノだと考えられている理由はよくわかるよね。 新山はベジタリアンではないが、アメリカニから見ればほとんどそう見えるだろう。
ドッペルときたらたいしたもんだ。のんのんのんのんのんのんのんのんAJAX BLEACH
(bleach と breach は違うよ)
で、こういうときにブログロは既存メディアよりも役に立つとかいってる人が 本当に役に立つ情報をさがせるのか、興味あるところではある。 けっきょくのところ、web で面白いのは「超ローカルな情報をグローバルに発信できる」という ところだと思うしそれには同意するのだけど、そういうものは普段からやっていないと 面白くないわけで、今回のよーな災害時はべつとして、平常時は ネット上の情報をおっかけることにしか興味ない人々にそんな真似ができるんかいな。
おそらくこれからも何度もやるハメになるのだと思う。 ケッキョキ、新山はぶつぶつ言いながらも最終的にはコレに適応するんだろうな、と思っている。 なぜならこの人生のテェーマは「アウトローに育てられた新山が紆余曲折を経ながら 社会システムに組み込まれていくところ」だからです。 どうせ現代人はみんな地獄行きだ!
ヒッコシ的作業、ほとんど終了。全部で 5時間もかかっていない。 なぜなら引っ越し先はフロアがちがうだけだからである。 いいかげんルームメイト探しに疲れたし、そろそろ一人でもやっていけるかな、 と思ったんで、このさい一人部屋に動いてしまうことにした。 ちょうど近くに部屋が空いてたという理由もある。家賃はちょっと高くなるが、 もうこれでルームメイト候補との接触とか、騒音対策とかインド人対応などをしなくていいのかと思うと、 まあ、嬉しいことはうれしいのだけれども、チョっと楽すぎるかなという気もする。 人間、ある程度は居心地の悪いところにいないと緊張感がなくなって 堕落するんじゃないだろうか。新山がいままでルームシェアしてきたのには、 こういう理由もわずかながらあったことは否定できない。ある人からも 「新山さん、わざと自分を追いつめてるんでしょう」と言われたので、他人から見ても そう見えるのかな…。ワガママをすこしは矯正しないとダメだと自分では 思っているわけですよ。とは言ってもこの日記を見るとほとんどの人には新山は とてつもなくワガママに見えるらしいが、実際そうでもある。… つうかねー、きのうセキネさんからやたらと「お前はワガママだ」と言われたんですけどね、 アンタに言われたかないんですよ、本当。ワガママ℃でいえば あの人も新山に負けず劣らずである。だってさーだってさ−以下りゃく
まあ、とにかくほとんどの移動は終わったわけで、まだ新しい部屋での こまかいレイアウトを考えてないのだが、もとの部屋のほうにはもうほとんど何もない。 いや、実際にはあって、それは PC と、お茶を飲むための道具一式 (ポットなど) である。 なぜならケーブル接続が移動するのは火曜日になるからで、それまでは 新しい部屋ではネットが使えないからだ…。つうことでここは火曜日まで「PC兼茶のみ部屋」として使うことにする。 ゼイタク。しかし実際には、階下でもじつは無線 LAN が入ってしまうということを発見したので、 PowerBook を使えばべつにここの部屋でなくてもいいのだった。それでもやっぱデスクトップのほうが キーボードがいいからなあ。けっきょく、PB はいまだにあまり有効活用されていない。
どーでもいいけど、この部屋にはほとんど感情移入しなかったなあ
(何かが起こったらしい)
いやそれにしても、公衆の面前でコケただけで大ニュースにされてしまうカストロってナンだ? おまけに「2001年にも公衆の面前で転んだ」とか書かれるあたり。
今日のトークのお題は「Monte Carlo Model Checking」とゆーもので、 一見するとつまらなそーな感じだったが、やはり題名で内容を判断してはいけないのだった。 トークはわかりやすくて非常に勉強になった。 自動モデル検証というのは、ソフトウェア検証の世界では一般的に行われているらしいが、 この研究は時相論理 (厳密には Linear Temporal Logic) の命題をモンテカルロ法をつかって チェックすることにより、従来の方法よりチェック時間を短縮できた、というものらしい。
時相論理 (temporal logic) というのは様相論理 (modal logic) の一種で、 時間によって真理値が変わるような世界をモデル化するのに適している。 で、これはソフトウェアの「正しさ」を命題として記述するのによく使われているわけだ。 たとえば、あるミッションクリティカルなソフトウェアを書いたが、そのロジックでは デッドロックが絶対に起こらないという確信が欲しいとする (飛行機の管制システムや原子炉がそうなったら困るでしょ)。その場合は、 まずロジックをぜんぶ時相論理の形式に変換してから、 G ¬(pc1 ∈ cs ∧ pc2 ∈ cs) という定理を証明する。 ここで G は「世界のいかなる時点においても (globally)」を示す限量子で (これはふつうの述語論理にはない)、 pc1, pc2 はそれぞれプロセス1 と プロセス2 の実行番地、cs はクリティカル・セクションを表す。 これが証明できれば、「世界のいかなる時点においても、プロセス1 と プロセス2 は決して両方が 同時にクリティカル・セクションに入ることはない」⇒ 従ってデッドロックは起こらない、と断言できる。 似たようなのに G (req ⇒ F service) みたいなのもある。これは F は 「いつかは必ず起こる (finally)」を表す限量子で、これは全体として「リクエストが来たら、 いつか必ずサービスが実行される (= ユーザが永久に待たされることはない)」という命題になる。 ま、ここまでは基本ね (新山は大学院の 1年次でやりました)。 ただし自動モデル検証というのはふつう莫大な時間がかかる。 これは「反例が見つからない」ということを示すことによって証明するので (与えられた命題を公理から導出することはすでに複雑すぎて不可能)、そのために あらゆる入力の組み合わせをシステムに与えてみるのである。まあ、予想はつくけど、ふつうは モデルの大きさに対して指数オーダーの時間がかかるわけだよね。だから現在の研究の多くはいかにこの底を 減らすかということにとりくんでいる。で、今日のおじさんの研究 (毎度毎度、発表者の名前なんか覚えてないので、 新山からみるとみんな「おじさん」としか呼びようがない) はモンテカルロ的に これをやることにより、速度を劇的に上げることができた、というもの。 ただし、その結果は確率的にしか正しくなく、その確率の下限もパラメータとして 与えてやらねばならないので、一長一短だが。
で、具体的にどうやるかというと、このへんは詳しく説明されなかったのだが、 まず線型時相論理の命題集合 S をすべて B なんとかオートマトンというものに変換するらしい。 このオートマトンはつねに S に対して valid な言語 (language、ここでは「文字列」ぐらいの意味) を生成する。 ここで証明したい命題の反例 Φ が与えられたとすると、このオートマトン B が Φ を生成しないということを示せばよい。ここでモンテカルロがどう生きてくるかというと、 このオートマトンをかたっぱしからたどってみるのではなくて、「random walk する」んだと。 ここにはとうぜん分岐が入っているわけだが、その分岐はつねに 2 らしく (つねに? これは謎)、おのおのの分岐は確率 Pz のベルヌーイ試行とみなせるという (Pz は不明)。 で、なんとかいうアルゴリズム (これまた忘れた) を 使うとオートマトン中のループを効率的に発見することができて、最終的に「Φ を生成しない確率」の 下限を保証できる、というのだ。へえ〜? って思ったけど、まあそういうもんかな。 ただしここには自由度が 2 あって、実際には「Φ を生成しない確率」ではなく 「ある確率で Φ を生成しないという予言が否定される確率」しか保証されないという。 もう何がなんだかわかんねええ。しかし、そんな細かいこたぁー専門外の人間には どうでもいいのだ…。ただし実験につかった問題はセコく、これはこの分野の シキタリなのかもしれないが、「dining philosopher がデッドロックしないことの証明」だった。 あれ dining philosopher ってデッドロック「する」んじゃなかったっけ? ふん、まあいい。それでも線型時相論理というのは時相論理の中でもまだ単純なほうで、 物事はつねに一定の方向にしか進まない。これが時間によって世界が複数に分岐するようになると (Branch Temporal Logic 、日本語訳がわからない、分岐時相論理??) になるが、これについては まだ難しすぎて何もわかってないらしい。
…と、いうことが、とりあえず今日のころきあではわかったワケです。 でもさ、ソフトウエア検証論って、けっきょく複雑なシステムのごく一部しかチェックできないわけよね。 とくにセキュリティに関する話なんかは、あまりにも関連する要素が多すぎて とてもチェックできないと思う (CSS (スタイルシートじゃないほう) なんかまさにそうだ)。 述語論理を用いて暗号プロトコルの安全性を証明しようって研究はあるけど…。 結局のところ、ソフトウェアを書く人間と使うユーザにある程度のつつましさがなければ、 何をやってもムダなこと。
このような意味不明な会話はもう 3℃とできないだろう。まさか、隠しているのじゃないだらうな!?
「いすどん」とpか「あどする」は常識だが、「みかか」という単語を使ってはいけない。 おじさんくさいから。
あれは「んんt」と呼ぶ。ことになっている。順序が多数おかしくても新山気にしないことは気にしない。
こういうのがいつもいちばん疲れる。 楽しくないのに楽しいようなフリをしなければならないし、憂鬱ー。 しかし、まあこれも仕事なのだ…と思うことにしている。 とにかく愛想ふりまいておけばいいのだ。
おおっと、けふは 13:00 からミーティングがあるんだった。忘るなよ odrkmmnk
まあそんなことよりオレは長野の台風のほうが気になるわけですが。 だってもう 10月末じゃない? ヘンな時期にくるよね? それにしても上今井のあたりって、前にも鉄砲水 (←変換できない!) でなかったっけ?
ぬぜなら (なぜなら)、うっかり論文とかプリントアウト置くとヌレちゃうから。
こんな新山でも気がつくとすでに一ヶ月以上の間 30歳でした。ホントに? てゆうか、思うんだけど、こんなヤツはダメだね! (断定)
今週から来週にかけて引っ越しのため回線が切れることがあります。
SHARP が米国向けの Linuxザウルスをやめるのだと。新山は PDA には全然興味ないが (PDFにはある、ちょっと)、きょうの nylug-talk では「悲しい!」メールが飛び交っていた。 てゆうかあれって日本でも売れてんのかなあ? わからんが。
どうでもいいけど今日発見したおもしろそうなページ:
こんなこといつもはやらないのに、なぜ今日はやるのか? というと、それは、なんかお腹が下痢気味だから。