Priority argumentというのがあって、あやしい集合の存在を証明するために、あやしいチューリングマシンを作る、たのしい証明技法である。あまりに楽しいのであそびはじめるとやみつきになると言われている。で、これを形式化したらおもしろいかもしれない、とこのまえ口走ってしまった。探してみたところ、既に誰かがIsabelleという定理証明系で扱ってみている様子(12/27追記: うそでした、なのでなおさら)なので、こんど適当にあそんでみようと思う。いつかそのうち。
どうせだから、次はpriority argumentの証明を出力するチューリングマシンを考えてみたらどうか。
しびれを切らして一般化してみた。風景が変わってよい感じ。適用できそうな既存手法の名前が浮かんできたのが、うれしいかも。とりあえずそっちに慣れよう。
午前中は本郷にて、なぞのミーティング。学部1・2年生たちの様子を観察すると、原稿にいい影響があるはずなので、めでたい。
夕方から横浜で、ISSスクエアのソフトウェア分科会。XSSとかSQLインジェクションとかって、データ構造が文字列だからいかんのではないかと思ってしまうのは、たぶんプログラム代数とかHaskellとかの見すぎだろう。もちろん、TCPのdumpを取ってそのまま読めるのは、それなりに大事なことだと思う。まーしかし文字列であっても、束縛構文でなんとかするというのをみると、こんなところできちんと束縛、λ計算偉いなり。
なぜかザーサイを買って帰宅。
あしたは、ちょっと試したいことがある。書き物も、あいかわらずある。
読みたい本を宣言できるところ。仲間がいたら輪読してみたい、けど、自分で旗立てして仲間を集めるほど熱心に輪読してみたいわけではない、そーゆーことを宣言できる場所を準備しておくといいのかな、と思ったりする。んで、自分が輪読したいと宣言した本を他の人も読みたい宣言したら、メールが飛んでくるようにも。十分な数読みたい人が集まったら、適当に相談するかもしれないし相談しないかもしれない、というような。
一年中同じところに座って、同じ窓から枝ぶりの、季節に従って葉の数が変わったり色が変わったりするのを眺め暮らしていると、葉を落としたり落とさなかったりするのは投資行動であろうと思い至った。多少寒くなったからといって葉を落としてしまうと、しばらくしてうららかな光合成日和を迎えたときに損したと嘆くことになろうし、かといって後生大事に葉をたくさんつけたまま冬を迎えると、損ばかりする羽目に陥るのではないか。つまり株価が下がっている時にどのへんで損切りするかという問題と同じなのである。
従って、世の中の株価の動きに従って気温を変化させる実験室で植物を栽培して、その成長度合いに応じて株を売ったり買ったりすれば、なかなかよい戦略になっているかもしれない。つまり生き物に戦略を計算させるのである。しかし植物を使うのは計算測度に難があるので、もうちょっと小さめの生き物がいいかもしれない。
某苦手の会で読んだ平均値の定理の証明で、1/k とかいうのが登場する理由を、わかっていなかったけれども、わかった気がする。単に0だと、頂上が平らのとき困りそう。ついでに、負の傾きを避けて、0と1/kの間にしておくことによって、いつでも左のほうに寄っていくことができる。ちがうかなー。
とりあえず、簡単な問題ふたつに帰着させた。両方解ければ、解けたことになる。
どっちか解けなかった場合には、ふたつに分けた分け方が悪いせいかもしれないし、反対を証明しようとしたほうがいいのかもしれない。とにかく解けなかった問題の反例が、何か教えてくれるはずだ。
MetaMLの論文を読んでいたら、ふつうにμとηをunitとbindと名づけて定義するんじゃなくて、射をKleisli圏の射にうつすものを、bindと名づけていたせいで、少しだけ戸惑った。なんで引数がふたつあるんだろー、という。
とりあえず、今日の発表を終えたので、抱えている書き物は、
ということになった。
しかしながら、考えかけているもののほうが優先順位は高く、
である。両方とも方針が見えてしまったので、IO負荷が高い。
方針が見えたのは、書き物が発生した後のようだ。方針が立たずに悩んでいてCPU負荷が高く、疲れてしまうときに、上記のような書き物によってIO負荷がかかるとコンテクストスイッチを動かす必要に迫られて、悩んでいた原因のひっかかりを通り抜けることができるらしい。
岡潔は、早寝早起き時期と、宵っ張り朝寝坊時期があって、たくさん書けるのは早寝早起き時期で、たくさん考えるのは宵っ張り朝寝坊時期であったようだ。そういえば、昨夜7時半ごろに寝たら、今朝6時半ごろに目が覚めた。
FriendFeed