ブロックチェインはなにかすごいのか

この記事のタイトルをよく見ると、「なにが」ではなく「なにか」と書いてある。ブロックチェインがすごいのかすごくないのかよくわからないからだ。君はEthereum Foundationで働いているのではないかと聞かれると、はいそのとおりですと答えるのだが、ブロックチェインはなにがすごいのかと聞かれると、なにかすごいのかしらんと考え込んでしまう。

こっそり思うブロックチェインの一番の功績は公開鍵暗号の利用者を増やしたことである。電子メールにせよwebページにせよ、つけようとおもえば公開鍵暗号をつかえるのだが、つかおうと思わなければつかわないで済む。いっぽうブロックチェインにはアカウントの秘密を保持する機能がないので、自分の秘密鍵は自分で管理するのが当然の開拓時代である。これは、ブロックチェインがすごくないから起こることで、秘密を管理する機能がないところで価値を扱おうとするから利用者にしわ寄せが行っているだけで、まあ怪我の功名と言えるだろう。

そういえば、ブロックチェインで合意が取れるという話について、昔からある研究に照らして何か言えるか考えてみた。

分散アルゴリズムの研究では、ビザンチン故障(すぐせつめいします)するノードがいくつまでなら、まだ動きますよ、というような定理を証明していくことが多い。ビザンチン故障したノードは何をするか何をしないかわからないノードで、意味不明なデータを送りつけるかもしれないし、黙り込むかもしれないし、意味ありげだけなデータを送ってきてだましてくるかもしれないし、ふつうにしばらく動いているかもしれないし、とにかくなにをするかわからない。よいアルゴリズムを使うと、このような胡乱な参加者がたくさんいても、そうでない参加者同士でアルゴリズムを動かし続けられる。たとえばビットコインとかEthereumとかでビザンチン故障の参加者がいると何が起きるかというと、よい性質がすべて失われる。ビットコインでもEthereumでも、超絶的に運のいいビザンチン故障ノードが人のアドレスから秘密鍵をずばずば当てたり、proof of workの課題を他人の億兆倍のスピードで解いたりしはじめると、全体的に崩壊して素のインターネットよりよいところがなにかあったのか、わからなくなってしまう。これは極端な議論なのだが、ビザンチン故障に耐えるというのは、そういう超絶幸運参加者がいても壊れないということなので、しかたがない。

それではといって、これらのビザンチン故障のノードは実は確率多項式チューリングマシンで、これこれの計算は安くなくて、うんぬん、と、暗号の議論をするときに使うような仮定を置いていけば、暗号の議論でよくある結論の、セキュリティパラメータの増加につれてそのどんな多項式よりも早く攻撃が難しくなっていくので、これはいい方式なんですという議論ができるだろうか。できないとおもう。ビットコインにしてもEthereumにしても、たくさんお金を出してproof of workの課題を人より速く解けば、昔の支払いをなかったことにさせたりとか、いやな攻撃ができる。この「たくさんお金を出して」という障壁を、秘密鍵の長さにつれてどんな多項式よりも素早く引き上げていくというのは、できない話である。世界の富の半分以上がそのブロックチェインを支えているというふうになれば安全かもしれないが、それはディストピアだと思われる。

それから分散データベースとしてどうなんですかというと全然だめである。なにしろすべての参加者がすべての歴史を持つので、一台の計算機より速くなるということがない。そもそもすべての歴史に全順序をつけて一列に並べようというのがなんだか無駄な感じがして、個々のアカウントのすることについて全順序がつけばそれで十分なのではないの、と思ってしまう。全順序をつけるつけかたにしても、原子時計でタイムスタンプをつけたほうが、性能はでそう。このへんをもうちょっとましにする計画はあるが、分散データベースとして開発された分散データベースに性能が及ぶことはあるまい。

ブロックチェインはなにかすごいのか。たぶん、おたがい信用しないノードがたくさん集まって、ちゃんとprice of anarchyを払って一つの歴史を編んでいくのが、これまでになかったことで、おもしろい眺めなのだろう。そしてそのうち、ブロックチェインの側が地球を眺めていることになるんじゃないかしら、と思わせるようなところがある。既の僕のまわりでは変わったブロックが現れるたびに人が働いているので、ブロックチェインの側の都合で人間が動いている。

ともかく、人が使い始めていて、Ethereumのスマートコントラクトが走る仮想マシンはごく単純なもので、形式手法のよいターゲットとなっている。自分にとってはそれで十分である。

ETHDEV Berlinに遊びに行った

ふとETHDEV Berlinに遊びに行ってみた。

  • 上階の空手道場の振動で、部屋の照明が揺れていた。
  • 突然の来客、Ethereumってどうすれば買えるんですか、と切り出して、質問重々、お茶を飲んで帰って行った。
  • みんな黙々コードを書いていた。
  • Why3+Z3を試している人がいて、なんでこんな簡単な事後条件を判ってくれないんだと嘆いていた。
  • git fix-upという技を教えてもらった。git blameしてからgit rebase -i、というgit史改変を簡便にできるらしい。
  • Berlinにはemacs meetupがあるらしい。よいなあ。

目標を決めてそれに向かって進むのが嫌いだ。たぶん目標を言葉にしてその題目に自己投企するのが嫌なのだろう。巨視的な道筋を決めてそれに沿って進むより、微視的に意義ありげなことをずっとしているほうが好きである。それでは大事は成し遂げられないというかもしれないが、大事には興味がない。

ただ、微視的に目先をほじくり返していては、ひとつも形が現れないおそれがある。そこで枠を切る。切った枠の中を散漫にでもずっと掘り返していれば、枠の中のどこかは深く掘り返されて、暖かみさえ帯びるだろう。

この枠の形が人にとってわかりやすいとそれは専門と呼ばれるが、世界には地脈が巡っているので、人には関連がわからない飛び地をいくつも持つこともできる。枠の切り方は人にはわからないほうがたのしいかもしれない。

このごろのよみもの(2015年5月)

このまえ日本で買った本を読み終えたわけでもないのに、別のものばかり読んでいる。

  • 中野幸一編「変体仮名の手引」。「つ、つ、つ、つ、つ」とか言いながら、たくさんの「つ」の書き方をみている。頭を冷やすのによい。あと良寛の字がかっこいい。
  • Andrew Kennedyら “Coq: The world’s best macro assembler?”のCoqのソース これは読み始めたばかり。おもしろい。
  • bitcoindのソース ちょっと気になったので、ぼんやり眺めている。わりと荒っぽい感じがする。
  • Marco Poloの、ドイツ語で書いてあるアムステルダムの案内書 辞書を引き引き読んでいる。やっと分離動詞を見切れるようになってきた。住んだことがある場所なので、辞書を引いたらだいたい現実と対照がつくのが楽。

他に7冊か8冊、休眠状態のがあるけれども、あまり気にしない。

ところで、読んでいて頭を使うものがあまりないので、なにか仕入れようということで、刹那的瞬発力のために確率論パズルみたいのを、もうちょっと息の長い演繹を追うためにGeneral Topologyの教科書を、それぞれ買った。

311

2011年3月11日

北海道の定山渓というところでPPLという学会が終わって、新千歳空港でそろそろ手荷物検査を受けようかというところで揺れを感じ、なにか落ちてこないかと天井を見上げていた。新千歳空港のテレビで、津波の映像を見た。羽田行きの飛行機は遅れたが飛んだ。

羽田空港、出られなくなった人々で混雑。コンビニの前に警官がいて入店制限をしていた。自分は歩いて外に出ることにした。天空橋を渡って鎌田に向かう途中のコンビニで、おにぎりやパンや弁当など食事になりそうなもの一切が売り切れていたが、アイスクリームはたくさん残っていたので、それを二つ買って、食べながら鎌田のほうへ歩きつづけた。居酒屋やラーメン屋が営業していて、そこで夜を過ごそうかとも思ったが、鎌田駅まであるいてみた。途中、都心から来て多摩川を渡ろうとする行進に出会った。東急鎌田から列車が動くというので、乗ってみたら、乗り継いで実家の近くまで行けたので、歩いて帰った。

2011年3月

プラハで食べたもの

プラハで食べたもの

  • Wine sausageという、柔弱なソーセージを食べた。ぐるぐる渦を巻いて楊枝で止められていた。ふにゃふにゃしていて、おいしかった。

  • トマトスープを食べた。クリームたっぷりで、おいしかった。

  • ニョッキを食べた。ニンニクが効いて、おいしかった。

  • 豚スネ肉の煮込みを食べた。学校給食みたいな器で出てきた。脂身が健康に悪そうだった(私は脂肪が余っている)が、おいしかった。

  • 鴨のconfitを食べた。一緒に出てきた、じゃが芋の餅みたいなものが、おいしかった。

  • 麻婆豆腐を食べた。山椒が効いて、おいしかった。

  • Tom’s burgerというのを食べた。たれの味と卵と肉が調和して、おいしかった。

ドイツで働く話

海外で働くエンジニア(or Webの人) Advent Calendar 2014の12月11日分の記事です。半年ほど前から、ドイツのドレスデンという街で、アメリカに本社がある会社に勤めています。

数日前の東京とボストン(シアトル含む)の比較をみて、アメリカとヨーロッパはだいぶ違うのだなあ、とおもったので、そのあたりのことを書いてみましょう。

医療費

このまえ、歯のつめものがとれたので歯医者に行ったら、詰め物をしてくれました。健康保険証を見せただけで、支払いをしないですみました(ただし、詰め物の色を白にしたい場合は、追加の支払いが必要だったようです)。大学の学費も無料だそうです。

ビザ

EU Blue Cardという制度があって、IT-skilled workerで年収がいくらか以上の雇用契約がある人には、ビザがおりるようです。ビザの抽選はきいたことがありません。

チップ

チップは払ってもよいが、べつに特別なことをしてもらったわけではない場合にチップを払わないのは普通のことのようです。

公共交通機関

ドレスデン限定のことですが、路面電車が充実しています。自分は家から職場まで歩いています。

職場の構造

自分のところはオープンオフィスですが、ふつうは三人一部屋くらいの小さい部屋らしいです。

時間の使い方

みんな、ちゃんと帰ります。同じ会社に、自宅で働いている人もけっこういます。インターネットごしに会議できてしまいます。ときどき顔は合わせます。

喫煙者

喫煙者はたいへん多いです。タバコの吸殻が大量にちらばっているところがあります。

労働市場

労働市場の需給がどうなっているのか、いまいちよくわかっていません。自分は、特殊技能をもって入りこんだので、あまり参考にならないでしょう。ベルリンには起業している人がたくさんいるようですが、まだ、その界隈に出掛けていません。

ドイツ語

仕事は英語でも、ドイツ語が話せないと困る場面がいろいろあります。勉強しながら、ややこしいことが起きないように慎重に暮らしています。

このごろのよみもの(2014年11月)

このまえ日本に帰って本屋をうろついた。いくつか読み始めた。

  • 飯倉照平『中国民話集』登場人物がすぐ死ぬ(日本の民話もそうかもしれない)。
  • 神取道宏『ミクロ経済学の力』。著者をいちどだけ見たことがあって、どういう人だったのだろうと思って、読んでみた。たいへん親切な本。この本の補論Dというところをみて、おもいだしたのは、一度、休みを取って東大の図書館に行ってKoopmans, “Three Essays on the State of Economic Science”のはじめのほうを読んだ。そこで、価格は情報の節約だというせりふをみたのだった。
  • 竹内啓『賭けの数理と金融工学』もとになったShaferとVovkの本は長くて大変だなあとおもっていたので、助かった。5章の有利な賭けのところをみて、そりゃそうだなとおもって、なにがしかの具体例を計算してみたけれども、ちょっとした確率分布の変化にだいぶ敏感に戦略が変わってしまうので(というか手持ちの情報がどういう確率分布をもたらすのかあまりよくわかっていないので)あった。このへんの話の登場人物を多くしていくと何が起きるかは、ちょっと気になる。
  • 宇治拾遺。最初の話をよみおえて、翁は誰だったのだろうとか言っていて、題を見ると誰だったのかわかるなどする。

Slaughterhouse-Five

Kurt VonnegutのSlaughterhouse-Fiveを読んだ。ドレスデンの小説だと教えてもらったのがきっかけだ。読んでみたら、文脈がころころ行ったり来たりして、CPUになったような気持ちがする小説だった。第二次大戦末期のドイツと、ベトナム戦争の頃のアメリカと、UFOで連れ去られた他の惑星と、記述が行ったり来たりする。主人公は時間を行ったり来たりするので、ときどき映画を逆回しに見てしまって、燃えさかる市街から炎を飛行機が回収して、飛行機は後ろ向きにアメリカまで飛んでいき、危険物は工場で分解されて、石油は地面に戻される、というようなことになる。しかし、UFOや時間跳躍は日常めいて、第二次大戦末期のほうが、よほど現実離れしている。貨車に捕虜を積んで何日も運んでいると、貨車全体が生き物のようになって、食べ物が入って排泄物とうめき声が出てくる。爆撃の跡は月面で、鳥の声がプーチーイー、である。

ドレスデンの地理的描写はあまり出てこないのだが、そろそろドレスデンに半年も住んでいるので、ちょっとしたことで、どのへんの話だか見当がついてしまう。かぱこぽと馬車が進んでいたのは、我が家の前の道ではなかろうか。

Ukraine Diaries

Andrey Kurkov “Ukraine Diaries”
を読んだ。切羽詰まったときに何が起きるのか読みためておくと、自分が切羽詰まったときに、すこしはましな動きを取れるであろう。

  • デモの勢いを抑えるために、地下鉄が市内の駅をすべて通過するようになる。
  • デモのあったときその広場に近寄った携帯電話すべてに、同じSMSが届く。
  • Vodkaの値段が、ウクライナとロシアで違うので、クリミア半島には、Vodkaをウクライナの値段で買っておいてロシアの値段で売ろうとしたひとがたくさんいる。

というような、さかしい行動ががたくさんでてきた。こういうことは、言われてみれば納得がいって、かしこいなあ、というくらいの話である。こういう、かしこいなあ、というくらいの話のよこに、少し間違えただけで、あるいは何も間違えていないのに、命を落とす人もたくさん出てくる。

ところで、著者はヨーロッパべったりで、ヨーロッパに啓蒙してもらいたい、というようなことを書いている。ロシアには批判的だ。強国に挟まれて、どちらにつくかで国が二分されると、個々人も自分がどちら派か決めると楽なのだろうか。

十全外人大庭亀夫

大庭亀夫は英国の人なり。号して十全外人といふ。幼時よりキュウリのサンドイッチを餐する身なれど、自力にて発明や投資やを以て億万の財を成す。料理、乗馬、格闘など多才尽し難し。

日本語練習帳といふ文、率直自然に綴れば即ち中る。百千を知り一のみを書くやうなり。数多の人の苦楽を、直に聴き知れる人なるべし。富貴の極みを草頭の露と飲み下して浮遊する人なるべし。

日本の記事多し。暗然たる未来を見通す。
http://gamayauber1001.wordpress.com/2014/09/13/nomad17/

ときに生活の一端を覗かしむ。
http://gamayauber1001.wordpress.com/2014/04/30/living-in-obscurity/

これらの文は日本語界の風穴なれば、驚き疑ひ誹る者あり。嘘と決むる者あり、偽外人と呼ぶ者あり。日本への警鐘を賢しらに聴く者あれど、日本人の為す所変はらず、解釈改憲は成り韓国人への罵倒は続く。遂に呆れ果て「日本語人なんて心から嫌いになった」と述ぶるに至れり。宜なり。

8さいのじぶんへ

きみは、わからないのがきらいだ。ひとにわかるのに、じぶんにわからないわけがない、そうおもって、しばらくがんばるといい。わからないときに、わかったふりをしては、いけない。わからないまま、うんうんいうとよい。しつもんできるとよい。そうしてくらすと、ものすごくかしこいひとに、あえる。すると、がんばらないとわからないことが、たくさんでてくる。たのしい。わからないことがたくさんでてくる。たのしい。

きみは、れんしゅうがきらいだ。れんしゅうしないとうまくならないことが、きらいだ。どうしてうまくいかないのか、わからないのが、きにいらない。どうしてうまくいかないのかわからないのに、なんどもためすだけで、うまくいくのが、きにいらない。にんげんは、じぶんがどうしてなにができるか、あまりよくわからないようにできている。たくさんしっぱいするだけで、せつめいできなくても、しっぱいしなくなることがある。どうしてうまくいくのかわからなくて、ほんとうにうまくなんてしんじられなくても、やればすこしはうまくなる。

あとは、たのしくしているのが、だいじだ。たのしいふりは、しなくていい。

18才の自分へ

明日なにをしようか、考えていると思う。実をいうと、君が明日なにをするのかで、君が十年後になにをしているのか、だいぶ決まってしまう。こんなことを知ると、深刻になってかえって愚かな判断をすることもあるので、気にしないでもいいけれども。雲先生に楽しいことをすればいいと言われた通りだ。

君は、わかってしまえば単純なような話が好きなので、米谷先生の量子論の講義を眺めてよくわからないと思い、アイシャムの本を見てよくわからないと思い、そのままにしてしまったけれども、真面目な物性物理の人になる気はないのか、一度よく考えてみるといい。真面目と言ったのは、計算機と比べての話で、だいたい、電気を食べて熱を出している箱の中にいると、何かが保存するという気もしないし、どこに原則を求めるのかで意見が一致することもない。

君は、あるとき、立花隆事務所の本を運ぶ手伝いをして、書棚の夥しい昭和史の本を見て、北一輝とはどういう人であったのかなあと思ったが、そうしたら、その場でしゃがみこんででも、読んでみるとよかったと思う。

ところで君は、あるとき高校の数学の教師に何をするのか聞かれて、「研究者になるのかなああ」とか言って窓の外を見て、「いや、研究者じゃなくてもいいんだけれども」なんて言われていた。君の「なるのかなああ」は長く尾を引くのだけれども、君はうすうす気付いていて、君は北の窓から小金井の方を見ていたつもりだったが、つくばに行くことになった。そのあと外国に行くことになるのは、知らなかったであろう。

さて君は、USの大学には行かずに日本の大学に通っている。それで良かったのか悪かったのか、よくわからない。流行が激しい分野では、田舎で学問をやるのにも、思うままにじっくりやれるという長所がある。君はその後、ちょっとだけUSに行くけれど、極めて短期のお客さんだったので、どういうところなのか、あまり洞察が無い。もっと言うと、君は日本がどういうところであるのかについても、あまり洞察がなくて、おかげで土地をうつっても、どうにか暮らしてしまう。もちろん、初めて一人で出掛けた外国の、ダカールの空港を出て、炎天の下で途方に暮れることはあったが。

ドイツ入国してから働き始めるまで

5月19日にドイツに入った。入国にあたって日本のパスポートを見せた。働くためにドイツに来たと伝えると、外人局に行かなくてはならないことを知っているか聞かれ、知っていると言ったら通してもらえた。税関で、赤の門に行って、持っている高い品の品名、買った場所、値段の一覧を見せたら、申告するのは正しいけれども、今回はドイツに引越しするということで、これらのものは自分で使うためのものであるから、まったく問題ないと言ってもらって通してもらった。

泊まった宿は、現地のrelocation agentが教えてくれたところで、そこに泊まっていれば住民登録できるという。宿に着いたのは20時ごろ。

5月20日の8時半にrelocation agentと宿のロビーで待ち合わせて、そのままWelcome Center Dresdenという場所で、住民登録等の面談。この面談は、relocation agentのひとが、ぎりぎりに空き枠を見つけて予約してくれたもの。いろいろと日本で準備してきた書類を見せたら、住民登録してもらえて、仮の就労許可証も出してもらえた。翌日から働けるとのこと。ただし、学位の証明書をドイツ語に訳して持っていくという条件と、健康保険の加入証明を持っていくという条件をつけられた。

宿に戻って、健康保険の人と面談(これもrelocation agentの人に予約してもらった)し、加入する旨の書類にサインした。

5月21日の午前に、銀行まで行って銀行の人と面談(これもrelocation agentの人に予約してもらった)して口座を開いた。のちに、いろいろな番号やカードが郵便で届いた。その足で携帯を買おうとしたら、月賦払いの承認が下りないとかで、面倒なことを言われたのでprepaidの携帯を買った。仮の就労許可はあったので、そのまま仕事に行った。

ドレスデン行きの理由

なんでドレスデンに行くのか、よく聞かれる。

まず、証明士という職業を作りたいとか言っていたら、既にformal method engineerという職名で募集をかけられて、どうもやることがまともそうなので、負けを認めて軍門に下る。

地理

ドレスデンには路面電車がある。ドレスデンの路面電車は編成も長くて、路線もたくさんある。人口50万人程度の都市なのに、総延長130kmもの路線があるのだ。路面電車で暮らせてしまう。階段を上り下りしなくていいぶん、大都市の鉄道よりも楽かも知れない。ちなみに運転免許は取ったけれども、間違いが多めの人間なので、できる限り自動車の運転は避けたい。

文化

ドイツで暮らした日本人の本をみると、わりと自分には暮らしやすそうな気がする。理屈っぽい、たいへんよろしい。個人をやらないといけないのは、まあ練習だと思おう。

2012年頃

自分が書いたものをみていると、どうも、2012年の春ごろに、将来のことをながなが考えていたようすがある。たとえば、立花隆がどこかの本で、ジャーナリストとしての活動方法として、みはらしがいいところに立っておもしろそうなところを見つけたら寄っていって掘るということを繰り返すのだという趣旨のことを書いていたのを思いだしていた。みはらしのいいところに行ったら今度は面白そうなところに飛びつくぞと思っていた節がある。

それから、2012年5月1日に、このように書いている。「日本のふつうの人が海外にほいほい出かけられる時代というのは、あと何年もつかわからんが、案外すぐに終わってしまうものであろうという気がしておるので、どっか外に根を下ろすのもよかろう」。当時の気持ちを思いだすとだいぶ真面目に書いたようだが、今となっては、いるべきところの決め方がこう大雑把ではいけなくて、もっと局所的にどういう人となにをするのか見ないといけないと思う。ただし、日本がどうのとかいう話を気にするときに、動きまわれるようにしておくのは一つの作戦だ。

やはり同じような時期に、「人生から情報量をたくさん取り出すには先が見えないことをするといい」と書いた。これに従うのは、いまでは、どうかと思う。つまり、いろとりどりの不幸につっこんでいくよりも、単調な幸福のほうがよい。ホワイトノイズに浸るのが一番いいかというと、それも違う(ホワイトノイズの各試行の違いが分かって感興を覚える人なら、いいのかもしれないけど)。毎日びっくりするのが望みかというと、それは違う気がする。このへんは、もっと考えてから、また別に書こう。

結局のところ

Ellery Queenの推理小説を一階述語論理式に書き起こそうとして時間をつぶしていた変な小学生が長じて、演繹して暮らしたい、記号列が動くなんて楽しい時代だ、ソフトウェアについて演繹して暮らすのだ、と、わがままを言い出し、このわがままが叶う世の中になるとするとどんな具合に進むのかなあと考えて、それに沿って進んでみている。

よみもの

accelerando

Accelerandoという、singularityを描いたSFを読んだ。猫型ロボットの物語だが、ちゃんと猫らしく勝手な振る舞いをする。

話の筋はともかく、出てくる技術がときどき面白い。訴訟を自動化してDOS攻撃するとか。

物語の後半になると、だいたい仮想空間上の話になってしまって楽しくないのだが、登場人物が日常的にfork(2)するのはうらやましい。

遅れた政府の描写:

convinced that, if you have to pay for software, it must be worth something

また、遅れた人々の描写:

They’re like medieval peasants looking in puzzlement at the troubadour

戸田山和久『哲学入門』について:もっと大胆にやれないか

戸田山和久『哲学入門』について。

この本は「ありそでなさそでやっぱりあるもの」を扱う。あるとかないとかの話をするなら、あるというのがどういうことか決めないと、話をすすめづらい。この本で、せっかく情報量の話を書くなら、どうしてこう言わなかったのだろう:情報量が大きいことが起きたらなにかあったということで、たとえば静寂に小さな音がするだけでなにかある感じがするのはそのためである。

戸田山氏は「私は唯物論者である」と言ってから、意味とか機能とか「人生にとって大切な『存在もどき』」を物理的ものだらけの世界に煎じ詰めようとする。まず問題がわからない。意味とか機能とかを「存在もどき」と「もどき」をつけて呼びたくなる気分がわからない。機能というのがうまくいきそうもないことがうまくいくことなら、もともとうまくいきそうもなかったほどに情報量が大きくて、なにかあるということになる。また方法が気に入らない。起源を論じて煎じ詰める方法は姑息であると思う。昔の世界がいまより簡単だったらたまたま使える論法で、筋がわるい。

この本は、最終的には自由や道徳の話をする。道徳の話は集団維持の話だから、進化で説明するのもいい。しかし自由については、せっかく情報量の話を書くなら、どうしてこう言わなかったのだろう:自由とは、自分がなにをしそうか、周囲の予想よりずっとよくわかっていることだと。ついでに、自分というのは世界の中でどうなるのかの予想がつきやすい一角だと。

あとがきに「哲学はすべてを一枚の絵に描き込むことを目的とする営み」とある。これはやったほうがいい。でも話は簡単なほうがいい。シャノンの情報理論に目をつけたなら、もっと大胆に使ったほうが話が簡単になったのではないか。

Moving to Dresden to be a formal method engineer

This spring, I am moving to Dresden, Germany. In Dresden, I will work as a formal method engineer.

This decision incurred some costs. I had to give up a tenure-track position at a public research institute. My family and many of my friends get physically remote. However, the project in Dresden seems like what I wanted to do for a long time.

産総研を退職してドレスデンでFormal Method Engineerになる

産総研の博士型任期付研究員の職を昨日付で退職し、これから、ある会社でformal method engineerという職につくこととなった。ドイツのドレスデンに住むことになる。

昨日まで、産総研の人だということで、いろいろな人に呼んでいただいたり来ていただいたり面白かった。不満がないのに辞める人は初めてだ、と呆れられてもいる。しかし、ドレスデンでの仕事がたいへん気になったので行ってしまう。

ビットコインのしくみ

ビットコインに似ているのは、古代メソポタミアの神殿が人々の財産の記録を管理していた話である。いまどき神殿の代わりはインターネットで、インターネット中のたくさんの計算機に、誰がいくら持っているかの記録がコピーしてある。

AさんがBさんにビットコインを渡すには、「AからBにいくら渡す」みたいな文言に電子署名してインターネット中のたくさんの計算機に流す。というか実は、「誰がいくら持っている」という記録は無くて、「どういう電子署名をすればいくら使える」と書いてあるだけなので、気をつけないと盗まれる。

さて、インターネットのあちこちにたくさん記録があると、消えにくくてよいのだが、情報が地球一周するのに数分の一秒は遅れてしまうので、あちこちの記録は、どうしてもずれてしまう。あちこちで記録がずれると、会計的につじつまが合わないことができる。たとえば、もともと残高が100しかなかったAさんが、Bさんに100あげましたとか、Cさんに100あげましたとか、いろいろな相手にいろいろ言って、ある計算機の記録ではBさんに渡ったことになり、別の計算機の記録ではCさんに渡ったことになったら、白黒つけてどちらかの記録が間違っていることにしないと、つじつまが合わない。

白黒つけるには、神殿を一つ決めて正史の編集をまかせればよいのだが、その神殿を潰されると仕組みがもたなくなる。そこで、あらかじめ正史の編集者を決めておく代わりに、くじびき大会をして当たりを引いたら正史の編集をするというふうになっている。あとは、正史の編集者にごほうびが出たり、いろいろある。

人間の分類、自分はどれかな。

中学生のころ読んだのはじめのほうに、三つのフェーズということが書いてあった。

  1. 実行する
  2. 世界を観察する
  3. 自己を観察する

自分にどのフェーズが大事なのか間違えると大変であるということが書いてある。Yvonne通りを歩いているときに思いだして、さて自分はどれなのかなと思ってみたら、いまは世界を観察する人らしい。

まず実行したくはない。何かしたいという人の気がしれない。何がしたいかと聞かれると困る。気になることはあるけれども、したいことはない。これは、ほとんど生まれ付きのものだとおもう。小さいころもあまり喋らなかったらしい。

世界の観察は、したい。気になるのは、だいたい、あのへんにおもしろいものがありそうだというようなことで、「あのへん」というのは地理的な場所だったり、理論っぽい概念だったりする。その、おもしろそうなことをどうするかというと、行ってみて眺めて、それで満足である。論文を書くのだとか言われると書くこともあるけれども、だいたい景色が見えてからは労働としか思っていない。書いてみると景色が見えてくるということはある。

自己には、あまり興味がない。幼稚園児のころから根本的な思考回路は変わっていなくて、多少ひとあたりが良くなったり、待っていても損なときは動くこともできるようになったりするだけである。我ながらすごく単純なやつだという自覚はあるので、いまさらじっくり自己観察してなにがでてくるともおもわない。夢は、ときどき見るのだけれど、起きて数分で忘れてしまう。

A History of the Future in 100 Objectsを読んだ

このほん。書いた人はあたまがいいのうと思う。しかし、後半になるとネタ切れしている感もある。前半の章はだいぶ無料で読めるので、読んでみてもいいのではとおもう。

  • コミュニケーションの進歩は、遅くみつもられている感じがした
  • 計算速度の進歩は、速くみつもられている感じがした
  • “Japan walked farther down its path to becoming a[n] empty, haunted fortress”
  • Braidという互助集団。
  • 自動運転で荷物だけ運ぶdeliverbot
  • “Why should we continue to work so hard, Bertrand Russell asked, with such productivity?”
  • “weak epistemic closure” という、似たideaだけが行ったり来たりする塊。これはもうありそう。
  • 半分くらい失業。なんで昔の人はあんなに時間を縛られる契約をしたんだろう、と。

知らなかった言葉

  • ruse
  • slurry

Oberwolfachの数学研究所

Oberwalfachの数学研究所というところに来ている。近くの駅から15分ほど車で山に入ったところである。狭い道を飛ばすので怖かった。研究所から谷底をみると家がいくつか見えるけれども、だいたい木が生えた山がみえる。ここにたくさんの数学の本があって、スタインウェイのピアノもあって、ピアノがある部屋の温度と湿度は常に調整されている。部屋の鍵はどこも開いている。あまりに山奥だからだろう。料理がおいしい。水曜の午後はハイキングと決まっている。食事の席は、名前が入ったナプキン袋でもって指定されていて、毎食違う人と話をするようになっている。あらゆるものが最適化されている。だらだらと講義が続かないように、食事に出る時刻は厳密に決まっている。各自の寝室では無線LANがつかえなくなっていて、インターネットを使うためにホールに出ると、人と話をするようにできている。部屋には広い机があって、数学できるようになっている。暖房が暑すぎないのでぼおっとしない。電灯は、位置の調整が極めて容易にできている。ベッドの枕元は、壁が凹んでいて、そこにノートをおいていろいろできるようになっている。

しばらくいると、だんだん体調がよくなってきて、いろいろなことを思いつくようになってきた。図書館をふらふらと歩きまわって、いろいろな本を眺めて、おもしろそうだなあとかこういうのもいいのだなあとか、他の分野の人どうしが話しているときに、こういうことを気にするのだなあと思って、口をはさんだりとか、囲碁を打ったりとか、あほなはなしをしたりとか、ログファイルをtail -fしながらああだこうだ話しているところに割って入ってみたりとか、そういうことをしながら、もちろん本来の目的も果たしているのである。

rust has buffer overflow checking

I was not sure what happens when I try to make an out-of-bounds access on an array in rust. So I tried.

fn main () {
  let k = [1, 2, 3];
  k[4];
}

When I compiled the code, it did not complain. However, when I executed the result, I saw

task '<unnamed>' failed at 'index out of bounds: the len is 3 but the index is 4', overflow.rs:3

Not only the runtime refused to run the out-of-bound access, it produced a readable and informative message. I decided to investigate this language further.

Haskell Financial Data Modeling and Predictive Analytics

Haskell Financial Data Modeling and Predictive Analyticsという本を読んだ。著者のブログがけっこうおもしろそう。板の温度とか。板って、売り注文と買い注文が並んでいる板ね。

この本は、Haskellにも数式にも抵抗が無ければ(新しいプログラミング言語を半日でだいたい使えるという人は問題ない)眺めることはできて、どうせ詳細はコードを見たり他の文献をあたったりしなくてはならないような本であるが、入口としてはやくにたつ。この入口が、この世界の一番いい景色をみせてくれるのかは、私にはわからない。話が飛びすぎだろうという感じもする。しかし、この本に登場するいろいろなモデルやHaskellのテクニックを漁っていくと面白いことがたくさん出てくるのは確かである。著者はQuantlibというものをHaskellに移植している人で、いろいろと書きたくなったようだ。

扱われているquants的話題の一部。これらについては無知なので、扱っている話題がいい具合なのかは論評しがたい。

  • Grubb’s outlier detection
  • tick intervalのモデル
  • secantを使った零点探索をつかって、最尤推定
  • ARMA
  • Kalman filter
  • いろいろなvolatility estimator
  • trading dayが252日あるので、252の平方根が出てくる

それから、扱われているHaskell的話題はこのようなもの。まあ知っておいて、こんど使えるときにつかってみればいいのでは。

  • attoparsec
  • quasiquote
  • quickCheck
  • HMatrix経由でLAPACKとかを叩く
  • criterionでのベンチマーク
  • parallelなHaskell
  • cabalのsandbox機能

別にどちらの人にどちらを説明するというわけでもなく、こういうことがしたくてこういう道具を使うとなんかできますということが本には書いてあって、あとはおまけのコードをみればよいという仕掛けのようだ。

さて、この本のアプローチのよいところはなにかというと、数式とコードが近いところかもしれない。

2050年の世界『エコノミスト』誌は予測する

まあいつもの調子でばっさりばっさり書いてある。2050年のことはたいしてわからないが、ところどころへえっと思うところはあった。わざわざ買うべきだったかは微妙。

「デジタル画像は撮影直後に見られるので、写真の技巧を習得するのに必要な時間が減少した。」というところは、へえっと思った。たしかにこういうところはある。技術的なことって、結局のところ、何回やってみたかでもって指数関数的に欠陥が減っていくという印象がある。おそらくソフトウェアでもそうで、失敗を許して何度も試すほうが、早く完成度が上がっていくはず。このへんが、形式検証の使いにくいところ。

それから、「世界を変える新機軸の大半が、理知的な構想や計画ではなく、やみくもな試行錯誤の賜物」ということだから、元気にしていればいいのではないかと思った。

Dodenherdenking

アムステルダム大学の新しい建物の横にポルダーという飲み屋があって、ちょっとしたお祝いのときなどに行ったものであるが、あるとき、ふつうに食事していると、誰がアナウンスするでもなく、突然ひとびとがナイフやフォークを机に置いて沈黙し、給仕は給仕をやめその場に立ち止まり、沈黙となっていた。戦没者に祈る日であるという。国中がこの調子で、路面電車も止まるし、自動車も停まるという。街の中心のダム広場では、横の百貨店屋上の旗がはためく音だけが聞こえるという。

Next to the new building of the University of Amsterdam, there is a cafe called Polder. I used to go there for a small celebration and the like. One evening, I was dining when people put their knives and forks on the table and stopped talking, waiters stopped serving and stood still, and there was silence. That lasted for two minutes to remember the war deads. The whole country is like that, I hear, and in the Dam square, you would only hear the flags on the department store.

reading libstd::trie of rust

After reading libstd::bool I chose libstd::trie because the special thing about rust is pointer management. The code is at least readable although I had to go back to the language manual to see the meaning of ~.

The ~ shows an owned box. An owned box is a chunk of memory which is freed whenever the owner is out of scope.

enum Child<T> {
   Internal(~TrieNode<T>),  // what is this ~ ?  OK.  It's an owned box.
   External(uint, T),
   Nothing
}

For me, it was a bit strange to see that Mutable trait requires clear method. Intuitively, a mutable thing should have a method called update or something.

impl<T> Mutable for TrieMap<T> {
    /// Clear the map, removing all values.
    #[inline]
    fn clear(&mut self) {
        self.root = TrieNode::new();
        self.length = 0;
    }
}

I am in the midst of reading insert operation. I like the match expression on the right hand side of =. I do not understand why swap appears here. Also, the chunk function is still a mystery for me.

fn insert<T>(count: &mut uint, child: &mut Child<T>, key: uint, value: T,
             idx: uint) -> Option<T> {
    let mut tmp = Nothing;
    let ret;
    swap(&mut tmp, child); // why not just tmp = child ?

    *child = match tmp {
      External(stored_key, stored_value) => {
          if stored_key == key {
              ret = Some(stored_value);
              External(stored_key, value) //value changed
          } else {
              // conflict - split the node
              let mut new = ~TrieNode::new();
              insert(&mut new.count,
                     &mut new.children[chunk(stored_key, idx)],
                     stored_key, stored_value, idx + 1);
              ret = insert(&mut new.count, &mut new.children[chunk(key, idx)],
                           key, value, idx + 1); // recursion here.
              Internal(new)
          }
      }
      Internal(x) => { // well, OK, internals are internal nodes.
        let mut x = x;
        ret = insert(&mut x.count, &mut x.children[chunk(key, idx)], key,
                     value, idx + 1);
        Internal(x)
      }
      Nothing => {
        *count += 1;
        ret = None;
        External(key, value)
      }
    };
    return ret;
}

reading libstd::bool of rust

I am getting more and more curious about the language rust and today I read bool.rs

OK, this is how to import some of the names in a library.

use option::{None, Option, Some};

What is this cfg(not(test))? Looks like some pragmas for not testing something.

#[cfg(not(test))] use cmp::{Eq, Ord, TotalOrd, Ordering};

Now I find that these are called attributes. Maybe better than preprocessor magics. I also see #[test] and #[cfg(test)]. #[test] marks unit tests and #[cfg(…)] specifies when to build. (https://github.com/mozilla/rust/wiki/Doc-attributes) (https://github.com/mozilla/rust/wiki/Doc-unit-testing)

This one also.

impl ToStr for bool {
    #[inline]    // what is this inline symbol?  primitive?
    fn to_str(&self) -> ~str {
        if *self { ~"true" } else { ~"false" }
    }
}

What is this keyword “mod”? Wow, this is a module.

mod tests {

    use super::*;
    use prelude::*;

    #[test]
    fn test_bool_from_str() {
        do all_values |v| {
            assert!(Some(v) == FromStr::from_str(v.to_str()))
        }
    }

『リーン開発の現場』

スウェーデンの警察で使う捜査情報管理システムを、60人くらいで開発した記録がこの本である。前から自分はやりかけのことがたくさんあって困ったものだくらいに思っていたが、この本を読んで、新しいことに着手するのは当分あきらめようと決めた。「何かを始めるよりも先に、今の作業に集中して終わらせること」と書いてある。

この本の途中に、別の言い方で、「あらゆるキューを制限することだ!」と書いてあって、仕掛かりの作業の数を減らすという作戦が行き渡っていた。なんとバグは重要なものから30個しか管理しないという。結局のところ、仕掛かりの作業の数が減ると、やりはじめてから成果になるまでの時間が短いというよいところがあって、顧客からのフィードバックを得るまでの時間も短くなる。というか、やりかけのことがたくさん溜まっていても、外からみて嬉しいことがなくて、その無駄を省ける。

もうひとつの大切な点は、ホワイトボード上を進行していく付箋の群れの前でミーティングして、状況把握を共有するということである。面とむかって情報共有したほうが早いときはそうするという作戦なので、バグを見つけたときにシステムに登録しないでもそこのコードを書いた人に直接話して直してもらったほうがいいということになる。

現在の状況を把握するだけではなくて、付箋が動いていくのを観察していると、開発をはじめてからできあがるまでの時間は作業日数の5倍から10倍ほどで、作業していない間は待ち時間だということがわかったりもする。つまり、開発中のことは5〜10個くらいにしておけばいいだろうということになるのだろう。自分の状況を考えると、たいして人を待っている時間はないので、実は、やりかけのことはひとつかふたつというふうになっていいはずなのである。まあ、作業の種類が少ないと飽きるので、ちょっと多めにしてもいいような気がするが。

仕掛かりの作業の数を減らすとなると、次になにに手をつけるのか選択するのが大事なのである。そこで、大事なことからやるのは当然として、この本には「どの機能[の開発]が知識を生み出し、その知識によってリスクを減らせるか」とも書いてある。勝手に言いかえると、まだ扱ったことのない技術であるとか、顧客がどういう反応をするかわからないような技術、リスクがある開発を優先して行うということである。はっきり言うと研究所の仕事はこういうことであるはずなので、あまり結果がわかるようなつまらないことをしていてはいけないと思った。同じようなことはほかにも書いてあって、決定をできるだけ遅らせるということも書いてあった。

リーン開発って知らなかったのだが、実例に徹して見せてもらえて、わかりやすかった。

TOEIC 985

このまえ職場でお金を出してくれるというから、TOEICを久しぶりに受けてみた。前回受けたのは大学受験の直後で、925点だった。それから10年ちょっと経って、今回は985点だった。あと一問で満点というところであるが、わからなかったのが二問あったので、毎回受けて毎回満点というところには、まだちょっと距離がある。リスニングの試験で脈絡のないことをいろいろ言われていると、とりとめのないことを考えはじめてしまって、気付くと取り返しがつかなくなっている。

英語はそんなに使えない。

英語にも、日本語でいう「未だ謦咳に接していない」のようなまわりくどい言い回しがあって、そういうのを英語で聞いたことはあるのだが、自分で言えとなると、さっぱりできる気がしない。あと、やはり文化的背景が離れているので、雑談に参加できる率はそんなに高くない。浮世ばなれした話題ほど簡単で、「どうして国境が必要か」という話になったときには、「銃を持ち歩ける国があるから、その人たちがここにくると嫌だなあ」と言ったり、「インターネットの美術館と本物の美術館の違いはなにか」という話では「本物の美術館では絵を破壊できる」と言ったりするけれども、テレビ番組の話とかはわからない。あとあれ、米国の大学受験のときに使うらしい、ラテン語ギリシャ語起源の単語ども、あれをあまり知らない。Wordpower made easyとかを眺めて面倒になってしまった。それから、アメリカ合州国東海岸の早口青年の言うことは、まったくわからない。逆に言いたいことはだいたい言える。

言いたいことがいろいろとあって、整頓しがたい。

  • TOEICの点を目標にしたってどうってことにはならないから、使い道が先にあったほうがいいのでないかと思う。
  • 日本語でわかることは、わりとちょっとであるが、わりとおいしい。英語でわかることは、それなりに多い。中国語やアラブ語がわかると、また変わるであろう。
  • 日本語だけで暮らしているとわからないことが多い
  • duolingo.comは便利で、いま日本語版もつくろうとしているらしい
  • 何十万人の翻訳部隊をつくればスループットは上がるが、レイテンシはあまり減らないので、金融とか生物学とか旬が早い分野ではあまりやくにたたないかもしれない。一方で、数学とか物理とかは、頑張ってよいものだけ選んで日本語にしておけば、けっこうやくにたつのではないか。
  • 日本語だと、どんな連用修飾をどの動詞にかけられるかっていうのが、わりあい簡単なのだが、英語だと動詞ごとにどんな前置詞が続くのかが決まっていたりして、もう動詞ごとに決まり文句を覚えていくしかないのだということを早めに悟ってわりとよかったということ。
  • 紙の辞書をいちいち引くと、辞書を引くめんどくささが記憶するめんどくささに打ち勝って、脳味噌が仕方なく記憶しはじめること
  • Longmanの英英辞典を引いていたら、語義の説明に使われている3000語だかの使い方がわかってきてよかったこと
  • 日本の企業でも若いものは世界中をまわっている人がおおぜいいるのに、どこにいても通用する学問を修めたくせに外国に行くのは学会くらいというのんびりモードでいているのはどうも怠慢で、もっとうごきまわったほうがいいのではないかということ

それはともかく、Journées Francophones desなんとかかんとかという恐しい名前のところに論文を投稿してしまったので、通ったときに備えてフランス語やらないといかんという焦っており、こういう必要に迫られた学習がもっともいいのではないかとおもわれる。

いろいろな国の起業の例の本

Sarah Lacy: Brilliant, Crazy, Cockey: How the Top 1% of Enterpreneurs Profit from Global Chaosという本を読み終えた。いろんな国を旅していろいろな起業家と話をしたようだ。著者なりの理屈はあるけれど、具体例がおもしろい。地球表面の人間のことをわかりたかったら、やっぱり旅して人と話すのが一番いいのだろうなあ。自分でやらないのでこういう本を読む。

読みながら気になったこと:

  • アフリカ中央部の掘っ立て小屋では携帯の電波が入るのに、サンフランシスコでは入らない
  • 2000年から2010年にかけて、アメリカ(合州国)の民間の雇用は減った
  • スタートアップで働くほうが、かつて安定していることになっていた企業で働くよりもリスクが少ないということになって、つまらない人がスタートアップに集まりはじめた
  • インドの裁判が遅れを取り戻すには300年以上かかるという
  • イスラエルの人が明日がないように働いているという話をインドの人にしたら、われわれは無限の人生があるように過ごしていると言われた。
  • インドはSMS経由の商売が増えている
  • ベルギーがルワンダを30年支配しただけで、のちのちの民族紛争が生じた。

Rustをいじってみる

前に、C言語に代数的データ構造がつけば、だいたい満足であるということを書いた。
しばらくして、まさにそういうプログラミング言語があることに気付いたので、
さわってみることにした。

とりあえず、コードを拾ってくる

% git clone https://github.com/mozilla/rust.git

ビルドの仕方はここに書いてある。
https://github.com/mozilla/rust/wiki/Note-getting-started-developing-Rust

なんとなくpandocを入れてみた。

% cabal update
% cabal install cabal-install
% cabal install cab
% cab install pandoc

% brew install valgrind ccache

% ./configure
とちゅうでいきなりgit repositoryをcloneしはじめてびっくり

なんかこれに時間がかかったので、その間いろいろ読んでいた。
% make

そしてチュートリアルをたどってみる。

http://static.rust-lang.org/doc/master/tutorial.html

Emacs 24なので、packages-list-packagesからrust-modeを選ぶ。

メモをとって忘れる

大事なことばかり考えている人になりたくないものである。とりもなおさず、暇でいたいということである。「暇ある身になりて世の事を心にかけぬを第一の道とす」と徒然草にもある。

しかしながら四方八方からいろいろなものが飛んでくる。果ては、四方八方からたくさん受け止めたくさん投げ返すのを価値として、「一人でゲームをしない」を仕事の心得として掲げる人もいる。何も作戦なく巻き込まれてしまうと、四方八方から飛んできたがまだ投げ返していないものが、もやもやと心を占めて、気が塞がってしまう。

そんなわけで、いつのころからか、気にしなくてはならないと気付いたことは全て書いてあって、書いたものは然るべきときに目に入るはずであるという状況を目指すことにした。気になることはメモして忘れる。ただし、メモは見るはずのところに置いておく。すると、オリーブ油が流れるように滑らかに学習と探求をすすめていくというテアイテトスに、ちょっと近づける。

このごろは、Emacsのhowmで暮らしている。

IRCつかってみよう

このまえ従兄弟と久しぶりに会ったらLINEつかえと言われて、電車で向きあってちょっと使ってみたら、なるほど0.2秒もかからずにこっちからあっちにメッセージが飛ぶので、使いたくなるわけである。よくよく考えるとこれはたぶんIRCの感覚に近いのだろう。

知識論理など学んでしまって、わりとすぐに気がつくのは、通信の遅延があると共有知識をつくれないということで、特に、いくらでも遅れる可能性があるような通信では全然むりである。遅延がないと錯覚できる程度に早く届くなら、共有知識ができたような気分になったりするので、対面でのやりとりは重宝される。対面でのやりとりで大事なもう一つのことは、手を出せば届くという点にあるが、IRCにはkickというコマンドもある。

で、freenodeに#jcoqというチャネルができて、日本語Coqづかいが溜まっているようになってきたので、気になる方はwebインタフェースからのぞいてみるといいように思う。

8月の読書

8月に読んだ本を挙げていく。

プルタルコス 英雄伝 3

戦いとか占いとか政略とかの細かい逸話が延々と続くので、だいたいの内容は忘れてしまった。ただ、象を伴って街に攻め入って大混乱に陥った描写がおもしろかった。「こうして互いに押し合いへし合いして、誰ひとり、誰に対しても自分の力を奮うことができず、さながら釘づけにされて一体となってしまったように、あっちへ揺れたりこっちへ揺り戻したりした」(ピュロス33, 7)

月を見つけたチャウラ

ピランデッロの短編集。

くだらない話が多いが、なぜか読み進めてしまい、全部読んでしまった。風邪を引いていたからだろうか。自分に似た犬が出てきたからだろうか。くだらない話と書いたのは、今でもありふれた話ばかりということで、もしかすると今の自分はこの人が軽々描写できる範囲で暮らしていて、この人は実はすごいのかもしれない。

Henry Kissinger: On China

毛沢東、周恩来、鄧小平らと会ってきたHenry Kissingerが、中国の判断基準を解読した本。孫子の兵法や囲碁の考え方を持ち出して、アメリカ人にはわかりにくかった中国の指導者の判断を説明している。特に毛沢東と周恩来に対して敬意が伺える。合理的でないように見える不思議な判断を、相手の国の特殊な歴史や文化に帰するという論法がちらほら見えるものの、中国の固有の歴史や文化を学びに学んで中国の判断を理解しようと数十年にわたって努力してきたからこそ書けた本だ。

ソ連とベトナムが中国を囲んでいた状況から、アメリカと中国が協力してソ連を取り囲み孤立させる状況に移っていった様子は、本当に囲碁のようであった。

中国からするとアメリカの政治家が国内世論を気にしなければならないこととか、大統領が交代すると外交方針が変わってしまったりするところが、変に見える、特に中国での人権や民主主義という話題についてアメリカ人が意見を述べるのが内政干渉に見えるということも書いてある。

riak(005) reading Rpc.mli

I was reading epmd’s protocol description when I realized that the protocol involves keeping connections after an ALIVE2_REQ message. In order to implement this on top of an RPC framework, I have to specify whether to cut off the connection after each response. I was willing to tweak Async’s Rpc module if necessary, but fortunately, I found an interface called Pipe_rpc, which is capable of keeping connctions.

Next, I will be happily using this library.

(Comment: since I am working towards a Mandarin exam, the developments will be very slow during July.)

Riak(004) discovery of epmd

After peeking riak_core codes, I noticed some occurrences of net_adm:ping/1 calls. The net_adm:ping/1 takes one argument called Node and it sends a ping request. When the peer specified by Node answers back, ping returns pong. In any case, some mechanism must resolve the node names like ‘node1@machine.example.com’. The name resolver turns out to be epmd. So, I am trying to port it into OCaml.

Since the epmd-equivalent daemon has to communicate with local and remote nodes,
there must be some data serialization mechanisms. The bin_prot should be suitable.

github repo

Date Plan
7/7 nothing (traveling)
7/8 start editting Rpc code to support connection keeping
7/9 Rpc with connection keeping
7/10 Rpc with connection keeping
7/11 parse some of epmd options

証明士について:三宅秀道『新しい市場のつくりかた』

このごろ証明士という言葉をつくって、ことあるたびに書くようにしてみたら、あるとき電話がかかってきて電話の先の人が証明士という単語を発音してくれたので、すこしずつ証明士という言葉が広がっているようである。三宅秀道『新しい市場のつくりかた』の最初のあたりに、製品開発ではなく文化開発でウォシュレットは売れるようになったのだという話がある。確固たる作戦無しに証明士という言葉だけ作っていたのだが、どうやらこれは文化開発ということになるらしい。

昔から証明を書くのは数学者だったが、数学者は知らなかったことを知るために証明を書いたり例をつくったりしてきた。証明士は当たり前そうなことを確かめるために証明を書く。ソフトウェアが思ったとおりに動くことを確かめるために証明を書くと、形式検証していることになる。入力が一億通りくらいなら全部テストできるけど、10バイトくらいになったら全通りテストしていると地球が無くなってしまうので、代わりに証明を書いて済ませるのである。

いまの形の形式検証が流行るかどうかは知らない。一部、形式検証を使わないと認証が取れない規格も登場してきているらしいが、規格ごと素通りされるようになる可能性はある。ユークリッドをみればわかるように、形式化オタク的傾向をもった人というのは世の中にいる(本当の形式化オタクは、ユークリッドの原論をみて、正三角形を作図するところで、つまずくはずである)のだが、形式化オタクだけからなる市場では、形式化したくて勝手に形式化する人ばかりいて、その人たちを必要とする存在が感じられない。一つの可能性は、必要はなくても芸事として進んでいくという方法で、ものすごく上手でそれに人生埋める覚悟の人がプロになって、そこまででない人が習い事として証明を書くというものである。そんなに流行るであろうか。

もう一つの可能性は、ソフトウェアを書いたのに証明が書いてないのはなんだか気持ちが悪いとか、数学っぽいことを書いたのに形式化されていないのは、なんだか落ち着かないというように、形式化されていることが当たり前になっている領域をつくることである。そういう領域はちょっとずつ増えている。項書換え系の停止性の議論は、だいぶ形式化されているらしい。目標として数学者というのは、どうもよくない気がする。というのは、ある数学者が若かったころに話をしたら「一度証明できちゃったら他の証明とかぜんぜん興味ないんだよね」とか言っていたので、自分が(ひとつの証明を)わかってしまえばどうでもいいのが数学者だからである。というわけでソフトウェア屋さんを相手にしたい。検証したい問題を解ってもらうだけで手間がかかるのが最大の問題であるから、まあ、かっこいいことを証明したいとかいう欲はしばらく捨てて、それなりに高速なsortとかuniqとか、ごくごく身近な小さなものを検証していって、くだらないことから手当たり次第にやっつけていけばいいのではないか。

新しい市場といえば、ヨーロッパにいくつかNew Marketとかそれに類する地名があった。アムステルダムの南記という中国料理店があったのはNieuwmarktと呼ばれる広場で、蒸し牡蠣のたれがおいしかった。Henry Cecilという人が薔薇を育てさせたり馬と話したりしていたところもNew Marketという名前であったように思う。

Riak(002) Going through dependencies.

After I tar xf’ed the Riak source, I found deps directory containing many packages. This night I go through these.

  • basho_stats is apparently a statistics library: variance, min, max and histogram.
  • bear also a statistics library.
  • bitcask serves as a backend. Other alternatives include LevelDB. This one looks like an interesting porting origin.
  • cluster_info dumps status of Erlang clusters.
  • ebloom says, it is a NIF wrapper around a basic bloom filter. NIF stands for Native Implemented Function, probably something similar to FFI in Haskell and so on. I didn’t know bloom filter either, but took a glance on the picture in the Wikipedia article.
  • edown says Markdown generated from Edoc. Well, yeah, there can be n(n-1) translators.
  • eleveldb: Erlang binding to LevelDB.
  • eper: Erlang performance related tools.
  • erlang_js sounds like a javascript library.
  • erlydtl compiles Django Template Language to Erlang bytecode.
  • folsom capturing metrics. Probably the previous stat libraries are used by this.
  • getopt seems like getting options.
  • lager logs in the traditional UNIX way. You can do error, warning and so on.
  • lager_syslog sounds like its interface to syslog.
  • meck mocking library for Erlang. I like the name.
  • merge_index stores ordered sets on disk. OK, this one uses the bloom filter on the memory to find locations on disk.
  • mochiweb is a web framework.
  • poolboy is a pooling library, like connection pooling. I love the name.
  • protobuffs for Protocol Buffers.
  • riak_api Riak API on protocol buffers.
  • riak_control lets you control your cluster on a web browser.
  • riak_core has its own blog post. TODO To be explored.
  • riak_kv is a key/value data store on top of riak_core.
  • riak_pb contains Protocol Buffers message definitions.
  • riak_pipe says it’s “UNIX pipes for Riak”.
  • riak_search is a full-text search engine.
  • riak_sysmon. System monitoring. Memory usage, ports usage, a slow peer node, and so on.
  • riaknostic an interface for sys admins.
  • sext is a term_to_binary() library.
  • sidejob. Oh what is this? README.md is empty. It involves workers and supervisors, but no clearer idea.
  • syslog is an Erlang driver for syslog.
  • webmachine is an HTTP framework built around REST principle.

It is a bit surprising to see these proliferating libraries. It seems that Prolog found its way out.

Riak(001)

I decided to read the Riak source code. My day job involves lots of Coq scripting, paper reading and PowerPoint drawing, but I rarely read codes. So I have to hack at home to keep my programming skills. Another thing is, since my employer does not want me to leak information, my public exposure is somewhat diminished.

I set a goal: porting Riak to OCaml. Well, Riak is written in Erlang but OCaml runs presumably faster. The Erlang code contains lots of pattern matching, but OCaml has some pattern matching. The concurrency should be dealt with OCaml light weight thread techniques.

My available resource on this project is limited. I’ll be slow. Maybe somebody else finishes this sooner, but in that case, I will be able to understand their code better if I work on this now.

Date Plan
June 26 Planning.
June 27 nothing (partying).
June 28 grasp what deps/* do
June 29 read Real World OCaml appendix A and build an OCaml environment.
June 30 try using Riak
July 1 choose one of deps/* to port first

The Big Short

The Big Shortという本を読んだ。Subprimeローンの返済が滞る方に賭けた人たちが出ている。

変人ばかりである。やはり変人でないと、世間の人がみんな信用しているものごとの誤りを確信できないようだ。

私も変人の役割をきちんと果していきたい。

この変人たちから見たときの世間の人には、考えていないという特徴があるようだ。誰も何とも格闘していない、という描写がある。変人たちは、謎の証券の中身がそのうち返済が滞るsubprimeローンであることを見抜くために、長いものを読んだり住宅地に赴いたり、努力している。格付け機関が、なにかしているつもりで、なにもしていなくて、なんか銀行の人が適当に統計で理屈をつけてきたのを信じてAAAの格付けを出していて、そのAAAを見て、中身を調べずに証券を買って大丈夫だと思い込んでいた人たちも、会議やイベントに出て講演を聞いたり情報交換したりして、なにかしているつもりで、なにもしていなかった。

言われてみると、なにかしているつもりで、なにもしていないという罠はある。私の近くでもそういうことはありそうである。なにかしているつもりで、なにもしないなら、遊んでいる方がはるかによい。なにかしているつもりで、なにもしていない人が安定して給料を得つづけるような組織は淘汰されていく、それが努力している人たちに対する公平というものであろう。

学生時代に働いたこと

学生時代にいろいろなところで働いた。当時は給料のことを気にしていたが、今から思うと、堂々といろいろな会社の中をうろちょろできたのが、大変おもしろい。家庭教師や個人指導や塾の講師のようなこともしたが、高校生のとき座っていた席から黒板を背にして一回転したようなことであるから、大しておもしろくはない。新しいところで見聞を広げることが、おもしろかった。

ある会社の研修で講師役として、自分と同じくらいの歳のひとたちの相手をしたことがある。最初は新人として入りたての四月のひとたちに、それから一年くらいして二年目のひとたちに。一年目の新人たちは就職活動の続きでしゃきしゃきしていて、直前にマナー研修があったとかで僕が話を始める前には、起立・礼なんてしていた。二年目の人たちは、もうへとへとになっていて、座っていて話を聞いているうちに眠りこんでしまう人もいた。会社で働くという二十世紀の現象が、自らやってみないうちに、よく理解できた。私はいまは、一年目には余りしゃきしゃきしないように、あまり疲れないように、かえって二年目以降になったら礼を重んじてしゃきしゃきするように心掛けている。いまでは職場の大先輩に、職場べったりでも職場きらいでもない、新人類だと言われることもあるが、世代の問題ではなくて、新人と旧人を見比べてとくと考えたことがあるというだけである。

情報系の学生であるから、プログラミングのアルバイトもした。有り難いのは、ただただオープンソースの大きな、割と綺麗なコードを半年も一年もかけて読んでいたら給料をくださったことで、まだ直接研究で使ったことはないけれども、研究の出口を考えるときには今でもそのコードを思いだすし、いまでも技術的なことを考えるときの拠り所になっている。たいしたことのない、刹那的なwebサイトとかiPhoneアプリケーションづくりは、自力でできたので、細かい小品をいくつか世の中に出したものである。しかし、すっかり足を洗ってしまった。

IIJの研究所でCoqを書いたのは、Coqを書いてお金をもらった最初であるから、わりと、その後につながったように思う。もっとずっと昔のこと、特定非営利活動法人数理の翼で、主に高校生が参加する合宿をやる手伝いをしたことがあった。会場を確保したり講師を呼んだり広報したり移動のコースを考えたり物を運んだりといったことである。当時の働きぶりは自分では落第を出したいのだが、得意苦手がよくわかって、そのご注意してくらしている。

なんでもできるように思って、なんでも手を出していたものであるが、いつまでもそうしているわけにもいかず、そのうち自分はこれをやる人ですと言ってお金をもらわなくてはいけない時期がやってきて、それでも相手のことを解らないと話が通じない。節操なくいろいろなことに手を出して、いろんな人と話せるようになったので、たいへんよかったと思う。二十世紀的な会社の働き方をすると、それでもって世界の見えかたが決まってしまうのだから、当時おもっていたよりもおおごとであった。

働きはじめた感想

アムステルダム大学にいたとき、Life after ILLCという、卒業生を招いた講演会があった。ILLCは、論理学者がたくさんいるところで、修士や博士をとろうとしている学生たちが、根を詰めて論理のことをやっているのであった。講演会の意図は、そういう学生たちに、世の中には論理学以外のこともあるのだぞと見せることのように思われた。卒業生たちは、コンサルティング会社で病院の仕事をしていてその病院にうつって管理のようなことをしている人とか、つまと一緒に住めるポスドクの口を探して街から街へうつっている人とか、起業したひととか、いろいろであった。

最も印象に残っているのは、Philipsの研究所に就職した人の話だった。他の人の話は具体的で、どんな仕事をしたとか論理学を学んでいたときと何が違ったとかロジックをやったから大丈夫ですと言ったら面接を通ったとか、そういう話であった。しかしこのPhilipsの人の話は、スライドに字が無くて、抽象画がぽんと貼ってあって、一枚すすむたびに十秒ほど沈黙して、気分を語るのだった。新しい環境に向かう不安であるとか、飛び込んでみると案外あっけなくて、あれこれでいいのかなと思ったりとか。少しは具体的なことも話してくれて、Philipsに就職したのは、学生時代にたまたまdescription logicをやっていて、当時Philipsがそれを使ったデータベースかなにか作ろうとしていたらしいからだけど、入ってからは全然その手の仕事はしなかったとか、仕事の目標の選択肢はあまり無くてそれを嫌がっている人もいるとか。

研究職ではあるが大学ではないところに飛び込んでみて、最初のごたごたが落ち着いてきて、新しい日常が回りはじめたときに、あれこれでいいのかなという感じは、なるほどわかる。それで寝床から抜けだしてこんな文章を書きはじめてしまった。この研究者の名前はもう思い出せないが(記録をひっくりかえしたり、知り合いに聞いてみればわかるが)、あの落ち着いて話している姿はありありと覚えている。これは、ここだけのことではないのだ。

中国語入門I

このごろ放送大学の中国語入門Iという講義を受講している。きちんとお金を払っている。先週、放送大学で打合せに出たときにその話をしたら、お金を払ってくださっているのですかと驚かれた。たしかに、放送内容はインターネットでも公開されている。

中国語の文法がだんだん判ってきて、まるでLISPのように洗練されている言語という印象ができてきた。もしも日本が無くなって日本の詩歌をよめる人がいなくなってしまうと悲しいことであるが、別に全世界の人が中国語を使うようになっても構わないのではないかと思う。いまからでも遅くはないから、中国語に英単語でルビを振って、漢字で英語を表記できるようにしたらいいと思う。

ある程度すすんだら辞書を買おう。それから英語で中国語の勉強をしよう。それから、オランダにいた中国人青年に中国語で近況を書こう。そういったことを目標にしてみることにする。

「現代暗号の基礎数理」1

以前ひとに勧められた黒澤馨・尾形わかは『現代暗号の基礎数理』(コロナ社)を読みはじめた。ごろごろ寝転がりながら読んでいたら、4.1まで読み終えた。演習問題は解いていない。なんだか随分と字が大きくて小学校の教科書みたいな体裁の本なのだが、簡潔でいい。証明は省いてあったり書いてあったりする。ぜんぶの証明を見るより技法が端的にわかるところを選んでもらったほうが、私のようないいかげんな者には、ありがたい。

証明が省かれているところは「○○となることが知られている」と書いてある。たとえば、p.13に「[長さnのランダム置換族]P_nは、長さnの疑似ランダム関数族となることが知られている」とか書いてある。ここに、自分のメモが書いてあって、R_nには単射でないものが属していて、P_nには単射しかないのに、どうしてP_nでR_nの真似ができるのかとある。さらに返事が続いていて、elementwiseにしか観察できないからか、と書いてある。選択平文攻撃の定義を読みとばしたようだ。

書いていて、数式をTeXで処理してもらいたくなったので、さっそくブログの仕組み自体をいじる口実ができたのである。

hexo

このブログはhexoを使っている。きのう見つけて、すこし使いたくなった。静的ファイルを置いておくだけというのが、すばらしい。hexo自体はそんなに複雑ではないから、こんど練習にHaskellに移植してみようかな、などと言っている。ただ、やればできる気がするので、あまり優先度は高くない。優先度が高いのは、次に書く、暗号の勉強やなにやである。

つくば

つくばに暮らし、はや二ヶ月となった。萩谷先生の随筆にあるとおり、優雅に暮らしている。きちんと車をもち、巨大な駐車場が完備しているレストラン、本屋、風呂屋がある街で、オフィースから、歩いて5分くらいのところに住んでいるのである。ただし、まだ家を買っていない。