PC 用メガネ

例の青色を抑えるとか言う奴なんですが、コーティングに関しては、

＊　後悔している

感じです。今まで、まったく困っていなかったんだから、余計なことをすれば変なのは当然なんだけど。でも、それは違和感があるぐらい。

問題は、

＊　そもそも、Retina dot by dot で k14

14 dot font なんか使ってて良いのかってことね。nn と rn とかの区別が微妙。コーティングの問題か、メガネをかけると focus が落ちる感じ。視力的にも落ちているんだろうな。拡大モードだと、ちょっと狭くて。

いや、まぁ、離れれば小さく見えるのは当然なので、そのせいもあるんだけどね。もう少し大きいフォントを使えばいい説もあるが、16 dot なX11用の Unicode font ってのがなかなか。 昔、少し探したんだけど、やっぱり k14 が良くて。まぁ、困ったものだ。

それでも、15cm で MBP 使うより、PC用メガネ使った方が姿勢的には楽。というわけで、dot by dot k14 で、しばらくはいるつもりです。

久しぶりに泳ぎに

先週は風邪がぶり返して死んでたので泳ぎに行けませんでしたが、今日は、調子が良かったので行ってきました。

天気が良かったし暑いぐらいだったので、外でも泳いで見ました。水は全然冷たくない。去年は5月でも寒かったのだが。でも、もう梅雨明けた? いや、まだまだらしいなぁ。

外で泳ぐなら日焼け止め使わないとだめだな。なので、外ではあまり泳がず。1時間ぐらいにしました。

泳ぐのよりも、バスが中部商業までなので、そこから大学までの山登りの方が辛いかも。汗かくからなぁ〜　

このまま、痰と鼻水が収まってくれれば良いのですけど。咳は収まったので。

Agda

Haskell で書いた証明支援系ですね。院生時代は HOL だった。去年は Coq を使ったんですが、

＊　Haskell やるなら、近い構文の方が良い

というので、Agda をやろうと。「どうせ、おんなじようなものだろ?」とも思ったので。

なんだけど、

cabal install agda

で簡単に install が終わる割には、起動方法がまったくわからない。全然わからない。コマンド名がない。なんなの? いや、Coq でも、Application の中にある裸の coqtop を使っていたりするので、かなり怪しいことしていたわけですが。

で、しばらくしてわかったのだけど、

＊　Emacs の中から使うしかない

らしい。なんだよそれ。いまさら Emacs か? Emacs から脚を洗って vim 使いになった僕に Emacs を、また使えと。

それで、やる気が一気にくじけて、しばらく放置して圏論やりまくっていたんですが、ソフトウェア工学の授業は証明やるつもりなので、やるしかない。

で、Emacs 上げるんだけど、全然動かない。agda-mode が見つからない。locate agda してみたら

＊　~/.cabal/bin/agda-mode

そこか! なんで、そういう隠すようなことするかなぁ。~/.cabal/config をいじると、もっと、まともな path に置いてくれるみたいです。そういうわけで、~/.zshenv の path に ~/.cabal/bin を追加。それで、動きました。

で、Tutorial を見ていくのだけど、

Dependently Typed Programming in Agda
http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

なんだけど、延々、構文の話ばかり。Agda って、どうやって使うの?

Interactive Theorem Proving for Agda Users
http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html

こっちの方の Section 2 の方に、使い方が書いてありました。Refine とか、で Emacs の中で .agda なファイルを直接書き換えていくという方式。

Coq の方は、変数を宣言して、証明すべき式を Theorem や Lemma で書いて、そこに intro とかで、Natural Deduction の推論を直接当てはめていく方式。こっちは、auto とかもあるし、証明支援系らしい。

Agda は、Emacs の中で、式を書いて、これから書くところを ? と書くと、そこに入れる式の型とかを支援してくれる方式のようです。なのだが、いかんせん Haskell なので、

＊　構文がくせありすぎ

もちろん、Indent が構文の一部なんだけど、

＊ : とか -> あるいは任意のUnicode な記号

とかを自由に使える。なので、: と -> には両側に空白を付ける必要がある。しかし、その二つは、最もよく使われる記号だ。あだだだだ。慣れるだろうとは思うけど、どうしても、そこで構文エラーを食らってしまう。実際、 Interactive Theorem Proving for Agda Users でも、スライドの多くを費やして、そこを指摘している。いや、その判断はどうだったのかなぁ。

S:p

と書けないってのは厳しいよ。そんなこんなで、Coq と Agda は全然違うってのがわかりました。

まぁ、もう少し agda 見てみるつもりなんですが、Coq の方が良いという結論になりつつあります。Natural Deduction から、直接、繋がっているのは良いね。

Time Capsule 換装

500GB を4TB に換装ってのを去年の6月ぐらいにやったのですが、

＊　また Time Machine Volume が Full

もはや、毎年の行事だな。

で、PS3 のbakup とかを、ごそそご調整して捻出した2.5inch 750GB に入るかと思ったら入らない。全部、archive する option しかなくて一部だけ書きだすとかできないらしいです。ネットワーク経由ならできるのだろうけど。

しょうがないので、4TB の3.5inch HDD x 2 を持ってきて、

＊ 2TB TM を archive (*)
＊ TM を 4TB に換装
＊ 中身を戻す

という方法で。今回は割と簡単に Time Capsule を分解出来ました。しかし、組み立てた後には「HDDの脚4つ」が余る。うう、そんなものがあったのか。まぁ、いいか。いや、大した手間じゃないから、そのうちに、もう一回分解するか。

取り出した 2TB は、問題なく Mac OS X から見れる。spasebundle も開けられました。ということは、まる二日かかった(*) の手順は不要だったようです。

でも、TC のUSBから元に戻す方法がないのね。そうか。でネットワーク経由でしこしこと。これも一日では終わりそうにない。

iMac → Time Capsule → Bitcasa
→ 外付けHDD

という感じの流れですね。HDD も Bitcasa も信用してない。そこまでやって残す価値あるのか? いや、残るとまずいんじゃないの?

TM を Bitcasa に上げている人もいるようですが、あまり勧めないな。読み出せることを確認した方が良いです。Bitcasa は基本的には「ゴミを置くところ」だと思ってます。

Bitcasa は 5TB ぐらい。PDFとか音楽あたりは取り出すのは簡単なのだが動画はなぁ。でも、この辺り、どんどんネットワークが速くなるだろうからなぁ。 Bitcasa は、いろいろ癖はあるが、Mirroring 捨てて、upload script 書いてからは順調です。

ソースコード読み会二日目

結局、ずーっと mysql を読んでました。PyPy も読みたかったが。

SQL の parse から、INNODB の page access までで時間切れか。I/O に辿りつけなかった。

もう少し絞らないとだめですね。ちょっと手を広げすぎ。

iPhone 5 と、ソースコード読み会

昨日の夜中に 4S を落としてしまって。落としたことは何回かあるが、画面を割ったのは初めてだ。なので、いつもの大平で 5 に換えてきました。5s/6 を待つ気も特になく。4s の時には発売初日に行ったのにね。

読み会の方は、

＊　Linux Open Flow の kernel 内 trace

＊　mysql

を読んでました。kernel 内部を gdb で trace するわけだけど、そこまでで、準備不足が。

mysql も test db がないとか、postgresql は動作しないとかいろいろ。

明日は、もっとなんとかなってるかな。それでも去年よりはスムース。

Java Kuche Agile Satellite とメガネ

がんばらない方針で、メガネ二つ取って、午後3時から参加です。

PC用のメガネはばっちり。Retina MBP でもぜんぜん平気。すばらしい。15cm に寄らなくても良いし。Retina dot by dot の広さを使いこなせる感じ。可変度数メガネ欲しい。

一日数本の28番のバスに丁度当たったので、コンベンションから北谷まで直通〜　便利。

なんだが、ついたら「参加しますか?」(え? 何に?)「あ、やります」「人数足りないとkろがあったので、そちらに」ブレストからプレゼン。15分で。なかなか面白いです。

二日休んだので、だいぶ回復したけど...

＊　5/25,5/26 は、朝から恒例のソースコード読み会

ええええ。この体調で大丈夫かぁ? あまり話さなければ喉は大丈夫なんだけど、例年話しているのは僕だけみたいな感じだからなぁ。

なので、ぜんぜん、乗りきれる感じがしないです。学生たち、自分たちの勉強なんだから、学生たちに頑張ってもらうか。

可換図

コピーした本の余白に書きまくっていたんですが、

＊　やっぱり、なんかツール使う?

ということで、最初にみたのが、

Math ML http://www.w3.org/Math/Documents/Notes/graphics.xml

一見できそうなんだけどな。でも現状では　Math ML では可換図は書けないみたい。

SVG で書くぐらいなら OmniGraffle で書きます。

やっぱり TeX か? と思って探してみると、

tikz package http://www.jmilne.org/not/Mtikz.pdf

あぁ、そうそう、こういうのが欲しかった。

\begin{tikzcd}
A \arrow{r}{a} \arrow{d}{b}
&B \arrow{d}{c}\\
C \arrow{r}{d} &D
\end{tikzcd}

みたいに書くらしいです。

で、tikz ってのは、

http://sourceforge.net/projects/pgf/

あぁ、SourceForge ね。しかし、これが、

＊　手動でコピーする install

えぇ〜。これさ、いろいろやって、そのままインストールすると、他の人や、後日の自分がはまる。なので、久しぶりに EasyPackage を作りました。こうすれば、同じ作業を繰り返さないですむ。

で、動かしてみると、tikz-cd.sty がない。それは別物か。

CTAN http://www.ctan.org/tex-archive/graphics/pgf/contrib/tikz-cd

なるほどね。で、いそいそと、最初の例題を動かしてみるのだが、

matrix でエラーが出まくり。

エラーメッセージでググると TeX の拡張がなんとかとか。EasyPackage の PLaTex は、ちょっと古いんだよね。でも、tikz-cd の方は動いているらしい。それなりに、それっぽいものが表示出来ました。

でも、なんかエラーはたくさんあるらしい。すべての機能を使うわけにはいかないみたい。

ルンバの乱

風邪がぶりかえしたので、結局、一日家で、圏論やってました。

ルンバがタイマーが入っているらしく、動き出す。なんだが、いろんな破壊音が…

寝室からキッチンに出てきてしまったらしい。コードとか猫の餌場とかあるので、いろいろ危ない。がちゃん、がたん、ぐぐぐぐ。

でも、面倒だったので放っておいたら、

「ちゃらららん」

お、えらい。ちゃんと家に戻れた。特に被害もなかったです。お腹を見ると、

＊　猫の毛が一杯

そういう季節だからな〜

Bitcasa の upload の自動調整

while [ 0 != `du -s ~/Library/Caches/com.bitcasa.Bitcasa/Data/bks/outgoing|awk '{print $1}'` ]; do
sleep 1800
done

とすれば、Bitcasa の output buffer が空になるまで待てるのがわかりました。

1時間 rsync して、それを全部送るまで 3時間から6時間。週末は遅くなるというパターン。なので手動調整してたので、自動になるのはうれしいです。

output queue の size が見れないと思い込んだのだが、割と簡単にわかるのだった。

buffer を空にしないと、iApp/Web 側に upload が反映されないというのがあるみたい。どうも最新のものを優先に upload するからかな。ずーっと、
upload していると、送られないものが溜まったり。

4.8TB ぐらい上げたので、5月中には一段落かな〜

全体のスクリプトはこんな感じ。

src=hoge
log=/tmp/rsync.log
while ((1)); do
(echo -n "awake " ; date ) >>& $log
(sleep 3600; (echo >>& $log) ; killall rsync ) &
rsync -avP $src /Volumes/Bitcasa\ Infinite\ Drive/My\ Infinite/>>& $log
(echo -n "sleep " ; date ) >>& $log;
sleep 7200
while [ 0 != `du -s ~/Library/Caches/com.bitcasa.Bitcasa/Data/bks/outgoing|awk '{print $1}'` ]; do
sleep 1800
done
done

ちょっと、風邪がぶり返してるな。痰がちょっと。よわよわだ。

圏論の続き

手元にあるのは、Category Theory for working mathematician と、Introduction Hihger order categorical logic と、Category Theory for Computer Science で、どれも書いてあることはほとんど同じ。いや、後ろの方はいろいろ違うんだけど intro は同じ。そりゃそうだ。どれも古いです。

層圏トポスもあるはずなんだが、見当たらんな。

買った時にちゃんと読めよとは思うんだけど、まさか、今更、Monad とかの用語を見るとは思わず。いや、Edingbrugh とかでは結構見たんですけどね。Monad は、Triple とか standard construction とかの別名だったのか。

Universal mapping problem と Adjuction の対応の 3行の証明の確認が午前中で終わらないってのは、どういうことなんだよ。ま、stack overflow って感じもあるかな。

もう少し、直観が欲しいところなんだけど、いろいろ限界あるね。

はがない

「僕は友達が少ない」というアニメです。これは、胸が大きいだけのハーレム深夜アニメの典型みたいなものだな。前の中二病とか電波女に似ている「変な女性」ものでもあるね。こういうバカっぽいアニメも良いよね。

僕もどちらかというと一人遊びが好きな子供だった。今でも一人でいるのが好きかも。人がたくさんいると、それだけでうんざりです。というわけなので、ほっぽっておいてくれるとうれしいです。

というわけなので、一人の時間を探すのは得意な方かも。プールに人がいない時間とか、人の歩いてない道とか、空いているお店とか、誰もいない教室とか。いや、もっとはっきり「団体行動ができない」と言ったほうが正確かも。

本読んだり、ネットやったり、Twitter 書いたり、泳いだり、歩いたり。プログラム書いたり、プラモ作ったり、ゲームしたり、アニメ見たり、一人でできることは多い。バス停で歌の練習してたり。

スナックとかバーで飲んでいる時も iPhone ずーっといじってて怒られたりしてます。いや、だから放っておいてくれ。

てだこウォークの時にも、なんとなく集団から離れて一人で歩くみたいな感じに。たぶん、わざとだな。自然にそういう方に行動が向いているのだと思う。

でも最近は、一人で海岸に行って夕日が沈むのを見るみたいなのはやってないです。沖縄に来た頃はたまにやってた。一人の面白さ、あるいは、一人を楽しめるとも言えるね。

人と一緒にいるのが好きな人もいるよね。その方が、この過密な時代には幸せかも。

最近は木曜日に泳いでます

この風邪っ引きで、だいぶ休みましたが、先週から復帰。でも、1時間半は無理なので、1時間弱ぐらいから。今朝は筋肉痛くらいました。

なんとなくリズムがわかったような気がする。クロールは六拍子なので、どうも、うまくできなったのだが。

クイックターンは封印してます。一応、できるようになった気がするのでよしとする。

あとは、スピード上げていくぐらいしかやることないかな。でも、

＊　頑張らない

方針です。毎週泳いでいるというと「らしくない」と言われます。まぁ、そうだろう。

鞄どうしよう

今の Aletti は割と気に入っているのだが、奥様の評判がよくないらしい。

2004 年に17inch PowerBook を使い始めた時に、鞄にぎりぎりだったので、Aletti のを買ったはずです。結構高かった。

なのだが、奥様に非常に評判が悪く「猫がすりすりする」。別に良いじゃん。で、マンダリーナダックのキャンバス地のを買ったのだが、2008年に

http://seeker-s-eye.blogspot.jp/2008/10/blog-post_20.html 金具真っ二つ

を食らったらしい。チャックの鞄はチャックが壊れちゃうんだよね。2-3年だね。前のも一回交換したけど「もう交換できません」とか言われちゃって。

その後は、ずっーっと、Aletti です。いやいろいろあったんだけど。やっぱり、割と気に入っているかも。

つうことは、この鞄は10年物なのか。いや、ぼろぼろなんだけど。いや、ぼろぼろなのが良いんだよ。新しいの嫌い。ってことは、前のが完全にダメになるか、その新しいのが嫌いってのを乗り越えられるだけの良いものであるか、どっちかでないと買い換えないってことだな。あらら。　

この鞄、いろいろ問題があって、

＊　皮が臭い (今は、昔ほどでは)
＊　枠がないのでインナーが必須
＊　裏地が絶望的に弱くて、金具の裏が剥き出し
＊　皮の裏が、粉々になる
＊　ベルトの真鍮の金具が弱くて、壊れやすい

結構だめなんだけど。でも皮の感じが良いのと大きさと無骨な感じな割にシンプルなのが良いです。なぜか、

＊　留め金だけは丈夫

ここが壊れたら終わりだろうな。

なんか、奥様が Tumi のを買ってくれたんですが、どうにもこうにも気に入らず。黒のビジネスバックでポケットがたくさんってのは、どうもね〜 大きさが無用にでかくて。いや、いまの Aletti もかなりでかいんだが。チャックだしなぁ。

でも、そろそろ、やばい。この手の物は出会いだからな。気長に探します。

梅雨

え、梅雨入り? OS 研究会の時に「もう梅雨入りしてます」って言いまくってましたよ。

今年は結構寒くて、雨も多いなぁ。

困るのが、バスを降りる時に土砂降りってやつ。どうしようもない。別に良いんだけど。張り子の虎ではありませんので。

今日も、降っているが、しばらくすると止むみたい。止んでから帰るか。

Haskell

授業で使っているんだけど、この手のマイナーな言語、特に、理論よりのは嫌いじゃないんですけどね。

最初に触ったのは Prolog でかなりはまって理論も勉強しました。

次に見たのは ML 、SML だったはず。型推論は面白いと思ったけど、

＊　普通じゃん

みたいな感じでつまらなかった。HOL (定理証明支援系) の実装言語だった。あまりはまらなかったな。

その頃の Pure Functional な言語というと、Hope というのがあった。一応、動かしたはずだけど、あまり惹かれはしかなった。その関係で、SKIM とか λ計算とかπ計算とかいろいろやりましたよ。

Prolog はいろいろ問題があったが、琉大で学生に使わせたこともあります。最近でもたまに教えてる。面白ので。まぁ、でも死んでる言語だよな。

なので、最近の Lisp とか Haskell の流行はちょっと意外かも。でも、どの言語もそれなりに実用的。

特に Haskell は Pure Functional だから面白い。MLや Ocaml みたいな「普通の言語に型推論」とは違う。Monad も Haskell だから意味があるように感じる。学生が面白がって、Java で Monad っぽくみたいなことをやっているが、あまりうれしいようには見えないね。でも、Haskell だと必須なので。

なんだけど、いろいろ神経さかなでする言語なんだよな。

＊　インデント構文

いや、単純に嫌いなんだけど。でも、vim を expand tab にしたので、トラブルはなくなった。

＊　Monad が使いまくり

ううう、それでは、なんか C で書いているのとあまり変わりない気がする。まぁ、でもだから実用になったんだろうけど。

let はともかく where がちょっと違和感ある。これは慣れの問題だろうけど。

プログラム書く時の発想が Prolog 寄りになってしまうのが欠点かな。つい、引数一つ増やしてとか考えちゃう。まぁ、しばらくすれば慣れるのか?

宇宙戦艦ヤマト

何回も書いてますが、あまり思い入れはないです。スペオペよりはハードSFでとかいう時期に出てきた、どちらかといえばレガシーなスペオペだから。といいつつ、リアルタイムで見ていたはずです。

で、HDリマスターですか。いや、セルの傷が見えるな。重ねて動かしている部分の傷は取れないのね。最近のHDリマスターは妙に綺麗なのが多い。サンダーバードとか。でも別に話が変わるわけでもないし。気合いいれて見ようという気にはならないが、

＊　持っていよう

という気にはなるので、録画はします。

そして、リメイクの2199。きれいです。少し登場人物が増えてるね。女性のコスモファイター乗りは映画の踏襲か。映画では話はかなり変わっていましたが、こちらは、ほぼ原作通り。木星の浮遊大陸、反射衛星砲。いや、良いんじゃないかな〜　もともとレガシーなスペオペなんだから、なんでもいいんだよ。それっぽければ。

船体逆さまにして、あの第三艦橋が潜水艦の艦橋になる。いや、子供の遊びってそういうものでしょ? 理屈じゃないです。潜水艦に見えれば潜水艦なんだよ。いや、もちろん多少苦笑いはしますよ。でも、SF って多かれ少なかれ、そういう要素はあるわけでさ。「けれんみ」といえばそうだし。

先行き不安なところもあるけど、基本、元の話をなぞっていくだろという安心感も良いね。ガンダムUCも、そういうところがある。

＊　おっさん向けの拡大再生産

需要があるから良いじゃん。良くできていると思います。

Bar

風邪もだいぶ抜けたので(いや、まだ少し残っているが)、割とお酒を飲んでました。

最近、良くいく(沖縄の) Bar は、

＊　Bar Balic 大謝名交差点

そんな怪しいところに奥まってだいじょぶですかという感じですが、普通の Bar です。Bar は、まぁ、どの店も普通ですか。

＊　E-en 宇地泊、GEOの向かい 2F

広い。トロピカルビーチのビーチパーティの帰りとかに便利。下がラーメン屋さん。

＊ Gold Dust 一銀通り久茂地小学校向い

上の二つは、新しいのですが、ここは、結構老舗らしいです。全然気が付きませんでした。Jal City Hotel の裏からだと近い。

大平のVintage とか、長田のCross over 、若狭のBar Suzuki とかいろいろあるが、このところはご無沙汰です。そういえば、若狭の Bar Teada もあったな。なかなかいけません。久茂地の Babary Coast も最後に行ったのはいつだろう?

Bar はお酒を勉強するところだとも思うけど、最近は新しいのを試すこともあまりなく。近所で飲んでいることが多いです。

メガネ

なんかJINSがコンベンションの方にできたとか言うので、メガネを作って来ました。ちゃんとした度のメガネは片方の脚が取れてしまって、今は、PC用に中途半端に度を弱めたものを使っているんだけど、これが不便で。

しかも、Retina 用に使うには度の弱め方が足りないという「ぜんぜん役に立たない」メガネに。まぁ、僕は車運転しないので、あんまり困らないんだけど。で、

＊　4段度を弱めた Retina 専用
＊　遠くを見る用

の二つを頼んできました。

毎回言われるんだが「プリズム? 入ってませんよ」。いや、だから良いから入れて作ってくれよ。ただ、プリズムの存在意義は、もはや良くわからず。おそらくは、

＊　斜視の修正用

なんだろうけど、3度ぐらいだとなんだか良くわからん。プリズムが入っている方が、むしろ眼が疲れるわけで、最初の頃はメガネが変わるだけで結構慣れるのに苦労したものだけど。でも、今は、あんまり感じない。

大人になって、というか年食って、いろいろなことに鈍感になるのも悪くはないよね。

ハリーズ

行きつけのカレー屋さん。前田、幸地入口のバス停付近です。ここの定番メニューは「野菜チキン激辛」

http://tabelog.com/okinawa/A4703/A470404/47001941/

なんですが、久しぶり。三ヶ月ぶりか。おばさんが乳がんで治療中。抗癌剤が結構きついらしくて心配です。ですが、お医者さんを信頼して、そういう方針で耐えるしかないな。癌になること、お医者さんの方針、治るかどうかも、運次第。誰が悪いわけでもないのですが。なので今は昼の営業だけらしい。

今はインターネットでいろいろ調べられるので、どうしてもあれもこれもと考えてしまうもの。でも、結局は専門家の判断が一番良いはず。そう思うしかないですね。

ここのカレーは、いわゆるスープカレーなんですが、野菜の処理がばっちり。野菜単体で美味しい。カレーもスムースな玉ねぎとスパイスがばっちり。インド風かな。札幌の木多郎にも似てるかも。

東京で、ここに匹敵するカレーは存在しない、少なくとも僕は見つけてないです。学生が東京にいるOBに持って行って喜ばれたりしているようです。

元は崇元寺のお店らしい。まだある説もあるけど見つけられてません。大山のハリーズはハバナカレーになっちゃったしなぁ。

英語の文法は重要か?

最初に英語を習った時には文法は全然やらなかったです。

でも、中高では文法を「極めてゆっくり」勉強する。退屈だったなぁ。で大学受験で勉強しなおした時には、一応、文法書は勉強しました。二冊ぐらいは片付けたはず。なんだけど、文法を勉強している時には、あまり試験の点は向上せず。

なので、文法が重要かと言われるとどうかなぁ〜 もちろん人に寄るのだろうと思う。英作文する時は文法から入る方が良いし、Dectation する時も文法は手がかりになるから知っている方が良いといえば良いんですが...

英語は語順にはうるさい言語だと思うけど、結構、倒置とかあって自由な感じもある。スペイン語とかは語順は割とどうでも良い。というかどうでも良い方が普通なんじゃないかな? とはいえ、

* a few kinds of data

とかを、

* data kinds of a few

とかは言わない。いや、data kinds, a few ぐらいは言うかも。会話では、何も言わないよりはましだし。

いくつかの言葉の集まりがあって、それが少し弱くつながって文になるみたいな印象があるな。小さい集まりの方が大域的な文法よりも役に立つ度合いは高い。

* the real world
* take a look at

とか。たくさんあるけど、単語の量よりは少ない。

つまり、文法よりは、

* 単語、熟語

の方が優先なんじゃないかな。その正しい組合せが文法なのは理解してますが、

*　　文法ってのは例外のかたまり

だからな。英文法の本って結構分厚いわけだし。しかも、

*　　英語で書いてある英文法の本

とかないし。英文法を勉強している間は英語に集中できない感じがある。

と言っても僕も英文法復習してからなんとかなった気もするので、英文法抜きでできるのかどうかはわからないです。

語彙を調べると、どんな文章でも、まぁ、なんとなく意味はわかる。でも、文法だけわかっても語彙がわからなければ、全然ダメだよね。もちろん、わからない単語がなくなるまでにはかなりかかるので、いくつかの単語は推測したりする段階が多い。

すべての単語を調べないと文法解析できないような状況だと英語の勉強ってあまり楽しくない。なので語彙優先かな〜

もっとも、TOEIC 300ぐらいだと、文法も語彙も足りない状況だし、語彙だけ覚えるのも苦痛なものだからな。文法か語彙かどっちかっていう単純な問題ではないのかも。

やっぱり、What's what かな?

Display Off

VNC で画面をいじると結構明るく点いてしまうので、remote から消す方法がないかなと思って「そうだ、AppleScript だ」と思ってぐぐって出てきたのが、

activate application "ScreenSaverEngine"

ふーん。簡単じゃん。Command line からだとこんな感じ。

osascript -e 'activate application "ScreenSaverEngine"'

で、MBP では動くんですが、iMac/MacMini だと、

0:40: execution error: File ScreenSaverEngine wasn't found. (-43)

えぇ、なんで? 確かに ScreenSaverEngine というアプリケーションはなくて、Framework があるだけなんだけど。わからん。どれも Mountain Lion で同じはずなんだが。

その場にいれば、ホットキーですむんですけどね。

絶園のテンペスト

最初の頃に「これはいいや」で落としちゃったのですが、あとで時間物だってことが判明。絶海の孤島のお姫様の話だったのに何故見逃したのか良くわからないです。自分に見る目がないことはわかった。なので、1-5話を録りそこねました。テンペストなので劇を意識しているので、演出がくさいのがな〜 と、ここまでは前に書いた。

そのまま放置していたんですが、なんとか最後まで見ました。やっぱり、そういう落ちかと思う、ということは丁寧に伏線が貼られていたということかなぁ。ちゃんと終わっていたのは良かったです。

時間物にしては破綻は少なかったかな? 葉風(はかせ)が未来にわざわざ出向いた意味はどこにあるのかは少し疑問だったけど。でも、そうしないと時間物にならないからなぁ。

始まりの木と絶園の木の解釈が「宇宙人による文明封鎖」なら、これから宇宙人がやってくる展開になるわけですけど、そっちの方はやるとしても炸裂しそう。この手の文明による文明封鎖ものとしては、

時間封鎖
http://seeker-s-eye.blogspot.jp/2009/01/spin-rcwilson.html

があった。木が、そのまま宇宙エレベータになるという展開だったら、似ていたかも。

人類の文明が行き詰まっているからと言って宇宙人頼みはいけないなとは思います。まだ、結構時間はあるので、何か残してほしいものだ。

愛花は性格が悪いという設定でしたけど、ちょっと皮肉っぽい言動だというぐらいで、それほど悪いとは思いませんでした。性格が悪い女性は割と好きです。どちらかといえば葉風の方が性格悪いよね。すぐ命令するし。

こういう魔法があることがわかれば、科学者はなんだかんだで解明しちゃうだろうな。「ぼくらの」では、歯が立ちませんで片付けられていたけど。

ラーメンフェスタ

我流とんこつ、桃原、遇、もとなり、たつぞうと、5件廻って、スパイスもらいました。

学生は一週間ぐらいで全部廻って二週目とかやっているらしい。そんな風に楽しむものではないと思うんだけどね。人の勝手ではあるけど。6月いっぱいだから、まだ、時間はあるね。

ちょっと、とんこつに偏ってるかな? それもあって、急いで廻ろうという気にはなれず。

4月後半からGWは結局、ほとんど寝ていたので、あまりお金を使わなくて良かったかも。うっとうしくてすみません。まだ、ちょっと鼻水が残っているが、これは長引くんだよね。

圏論

学部時代に「層圏トポス」で勉強したはずです。特に深い意味はなかったが、数学の勉強の延長線上。直観主義論理と関係があるぐらい。米田レンマぐらいは追ったはず。この時は「選択公理なんて認めん」みたいな人だったので、locally Small とは「はぁ?」だったはず。随伴関手とか双対とか面白いんだけど、面白いなぁぐらい。Category thoery for working matehmatician も、一応は読んだはずなんだけど。圏は対象(集合)と矢印(写像)で作るんだけど「なんで集合なの?」って辺りが嫌だったかも。(今は選択公理勉強したから、それほど抵抗はない)

なので、論理型プログラミング勉強した後、計算理論の方でカテゴリーが出てきたは意外な感じ。関係ないと思っていたのに、やっぱり、そこいくの? みたいな。まぁ、直観主義論理なんだから当然と言えば当然なんだけど。

とは言えば、いまだにピンとは来てない。使いこなせてもいないです。単一化の双対に minimun confilt set があるとかは面白かったが。萩野さんのカテゴリカルプログラミング言語 CPL も、ちょっとだけ見たはず。大学院とかでも何回か復習はしてるけど。

で、灘高の文化祭で

圏論によるプログラミングと論理
http://www.npca.jp/2013/

ってのが。おお、300ページ超かぁ。力作ですね。CPL とかに費やしているのは関係した人の趣味かな。λ計算、型理論、圏論、モナド、論理、カーリーハワード対応、CPL と一通り入ってます。

この手の物は自分で勉強した時の目録みたいなもの。これを作るのは良い勉強になる。僕も物理と化学では作った。数学は作りませんでした。

でも、間違ってもこういうもので学んじゃだめなんだよね。例の岩波の基礎数学と同じで、

＊　わかっている人はふんふんですむが、最初に読んでもチンプンカンプン

いろいろ理由はあるのだけど、

＊　詰め込みすぎ

＊　確認のための問題がない

そして、

＊　記法の説明が完全でない

わざとやっているわけでもないんだろうけど、そうなっちゃうものなんだよ。当たり前のところを省いちゃうわけね。でも初学者は、そこでつまづく。なので、結局は演習を地道にやるしかないです。というわけなので問題と解法がたくさん載っているものが望ましいね。

a → b → c は a → (b → c) のことなんだけど、そして、そう読まないとつじつまは合わないわけだが、そんなことを書いてくれる人はいないんだよね。

でも復習には良いんだよな。一方で、やっぱり今の段階で役に立つかというと微妙だなとも思う。その割にモナドとか証明支援系とか流行っているので、逃げるわけにもいかんし。困ったものだ。必要なところだけ近い道したいところ。学問に王道なしだけど、300ページは寄り道多すぎる。

Linux と DAM

ふる〜いDAMのリモコンは、Linux 。たまに、freeze するので、横にあるリセットボタンを押すと、Boot message が見れます。

この白黒チェックの模様は、確かに懐かしのX11 。いや、今でも xterm 使っているんですけど。

TOEFL

大学入試に使うで若干話題になっているようですが。2016年目標? さぁどうだかね。

うちの学科では大学院入試には TOEFL を使ってます。高いという人もいますが、ITP っていう安上がりのやつがあります。なので高いという批判は、ちょっと外れだね。

難しすぎるので差が出ないとかいう人もいますが、ちゃんと英語の成績に沿って差が出ます。問題ありません。どういう重みで判定するかは各大学の勝手だな。

で、そう決めた時に一回学生と一緒に受けに行ったのですが、あんまり良くはなかった。515点は低い。iBT65相当なので大きな声で言える点数と言い難い。でも、今受けて、それを越えるかどうかは自信がないな。強力に集中力を要求する試験なので。とは言いながら、大半の学生よりは上の点数です。

つまり、今の学生の英語の出来なさ加減は半端じゃないってことね。

受験勉強始めたら模試の英語に歯が立たなかったので、自分で勉強したんですが、文法書一冊と試験に出る英単語ぐらいで3ヶ月で偏差値60ぐらいに。その後は、短いエッセイとかSFのペーパーバックとか読んでました。で、理系の入試だとそれで十分。80点ぐらいは取れるようになっちゃう。なので、そこで英語の勉強をやめちゃうんだよね。ってことは、高校までは全然英語勉強しなくても英語の授業を乗り切っていたってこと。

言っちゃぁなんだが優秀な学生だったと思うので、要求される英語のレベルが低いのはもったいなかったと思う。実際、

＊　大学に入って、英語の本を読むようになったら、まったく役に立たなかった

で、そこで勉強しなおしなわけ。と言っても問題集とかはもう解かなくて、ひたすら本読むような感じだったけど。それが良いかどかは別なんだけど。Dictation とか Shadowing とか、もっとやれば良かったかも。でも、大学で英語の勉強ってのはもったいないです。他にやるべきことたくさんあるから。

大学入試でも80点から90点に上げるのは結構大変。TOEFLだと iBT60からiBT80に上げる感じかな。その段階を大学でやるなら、ありかな。いや、文系の人には笑われるでしょうけど。

＊　今は、80点から90点に上げるメリットはない

わけだけど、TOEFL baseになると iBT120まであるので英語を勉強するメリットが上がる。それは大きいと思う。それに、

＊　十分だと思う程度に勉強したが、まったく役に立たない

ってのは避けられると思うんだよね。

もちろん、それに対応した英語教育をできる教師がいるのかとか教授法を変えないとだめだとかあるが、

＊　てめーら大学生なら、英語ぐらい使えるようになれ

ってことね。優秀な学生は必ずクリアできます。でも iBT 45 は目標として低すぎると言っておこう。

ビーチパーティ

火曜日は前回に引き続いてビーチパーティでした。基本的に奥様の趣味なので、僕はほとんど手を出さず。だいたい座ってました。

＊　鉄板にアルミホイルを敷いて焼く

ってのは、前回のBBQで学習した成果らしいです。その方が美味しいかな。

会費3,000円はちょっと高かったかな。会費なしでカンパぐらいで良かったような気もします。入れ替わりとか、ちょっとのぞきに来た人とかで面白かった。普段会えない人も会えたし。

天気には恵まれて、晴れたり曇ったりで雨は降らず。水曜日だったら寒すぎただろうな。

僕は体調は良くなったのですが、まだ、痰が抜けなくて。とはいいつつビールは良く飲んだ。10リットルは、なくなったみたいです。さすがです。

12時から19時だと、ちょっと長過ぎる。15時ぐらいからの方が良いんじゃないかな。体力的にきつかった。

＊　ビーパーは、バスで行くもの

ではないんですか? トロピカルビーチは、最近、バスちょっと増えた。コンベンションセンタ前から歩けばすぐです。帰りのバスもあるし。