Yoneda Functor

型Bから型Cへの関数全体を考えると、型Aから型Bへの関数fを使って、型Cから型Bへの関数全体を得ることができるってな話です。型Bから型Cへの関数全体ってのは集合だから、いろんな型と関数からなる圏から、型Bから型Cへの関数全体の集合を返すのは Functor と考えることができて、関数 f は、その Functor 間の自然変換を提供するというわけ。

grep と nkf で、nkf を Functor、grep を自然変換と考えて、grep してから nkf しても、nkf してから grep しても結果は同じってのが、grep の自然変換の可換性ってな例を考えました。

この辺りはわりとわかりやすくて、最初に読んだ時にもちゃんと理解していたはずです。役には立たなかったけどな。その後、勉強して理解したつもりになっていた頃は、明らかにずれていた。そういう時もあるよ。

今回、Agda で証明して得るものは、苦労した割には、それほどなかった気もする。Sets と圏が入り交じるのが難しい。あと、Full Embedding ( 二つの型から型への関数全体が等しければ、それぞれの型は等しい )ってのは、どうも証明できないみたい。

＊ Hom A a b = Hom A a a → a = b

背理法を使えば自明なんだけど、Agda は背理法は使えないからなぁ。本の方でも must be とか、歯切れの悪いことが書いてあるので、きっと背理法抜きではできないのだと思います。いや、できるのかも知れないけど。

refl で受けると、a と b が違うと言ってくる。なんていうか「前もって同じだとわかっているものしか同じだと証明できない」みたいな感じ。 A [ f g ] → Category.dom A f ≡ Category.dom A g とかはできるんだけど。

これから、卒業生たちと飲みに行くみたいです。

宇宙戦艦ヤマト 2199 第七章

テレビに先行して最終回までということらしいです。ちょうど残りが見れる感じか。いろいろ考えるね。映画版は一部短いので、後の放送もちゃんと楽しめると。よくできてるな〜

別に地上波放送をゆっくり待っても良かったのですけど。いや東京にいないと、こういうものは見れないからな。結局、映画で見たのは七章だけ。

羽生さんも言ってましたが、予告編がよくできてます。ほぼ原作通りですが、いろんな工夫があるね。お約束もちゃんとありました。

今、1974年の原作を見るのは、HDリマスターでも辛いので、リメイクはうれしいです。当時、急降下爆撃機とかを馬鹿にしたものだけど、今あえて、同じことをちゃんと描くのが良いです。某巨大ロボットアニメと違って安心して見れるのが良い。

一万円のヤマトのプラモデル? ふーん。いや、別に欲しくないし〜

IMAX

IMAX は映画館の規格の一種らしいです。3Dにしては明るいです。

＊ http://en.wikipedia.org/wiki/IMAX

AVATARの時に「IMAXとそれ以外」みたいに言われましたが、正直に言えば、

＊　　3D 以外は IMAX である必要はない

気がする。スクリーンにシミのある桜坂劇場でも良いよ。

僕は立体視はあまり良くない。他の映画よりも疲れるだけな気もする。それでも3Dなら IMAX を選ぶかな。無理に手元まで持ってくるようなのはちょっと。

なんと、特別料金、つまり、余計にお金を取る。としまえんは、さらに

＊ ウィンブルシート

なるシートが振動するオプションがあり、さらに200円取ります。ふーん。手続きが面倒なのでパスしましたが...

割と前の方でも大丈夫なみたい。今回は真ん中辺りだったのですが、もう少し後ろが良かったかなと思いました。川崎の方が大きいのかな? でも見てる分には、差は感じなかった。

ネットで予約できる。でも＊払い戻し不可＊、この辺り納得できないね。IMAX と IMAX でないのが混在してたりするし。一回ハマったことがある。

うっかりメンバーズカードとか入っちゃたけど、
http://www.unitedcinemas.jp/toshimaen/club-spice.html

年間500円は元を取るのは無理。それに IMAX は割引してくれないらしい。それを見落としただけです。

豊島園の駅のそばだけど、練馬から歩いて20分ぐらい。大江戸線は使うとちょっと高く付く感じだしな。

途中に大きな木があった。この大きさは珍しい。

Pacific Rim

怪獣映画、見てきました。

豊島園に United Cinemas ができていて、そこが IMAX なのね。3年前のAVATARの時には「日本では、しばらくIMAXはできない」みたいに言われていたけど、既に、その「しばらく」は過ぎてしまったわけね。時間が経つのは早い。

ちょっとスクリーンが近い気もしましたが、没頭できるかも。ただ、この映画は…

＊　疲れる

そういう映画だからなぁ。怪獣を自分で殴りつける(とロボットが同じ動作で殴りつける)というものなので。IMAX は 8/29までとか。そうなの?

ロボットの形状は、鉄人28号的なずんぐりむっくり。二人で同期して操縦ってのは、そういう設定のロボットもあったなぐらい。音楽とか極めて日本の怪獣映画を意識したものですが、映画自体はアメリカ的です。アメリカ的なノリで観に行くものだとも思うな。

このモビルトレースシステムは、Gガンダムなので「師匠〜！＊☆(TOT)」なノリが欲しかった気がします。が、日本のアニメや怪獣映画のオマージュは、いろいろありました。

この手の映画だと3Dは大きさを感じられるように使うべきだと思いますが、あまり成功してない感じ。やはり AVATAR は別格ということね。

移動日

というわけで、東京です。 忘れ物しないようにと思ったけど、

＊ やっぱり、圏論のやつ持ってくか
＊ MBP の電源が大学

なので大学へ。でも、そこで気がついたのだが、

＊　診察券とPASMO を家に忘れた

なので、いつもの往復ビンタでした。あららら。

PASMO を西日暮里で使おうとしたら通らない。券売機で見ると残高はある。駅員に見てもらったら、

＊　長く使ってないと、こうなる

まあ、確かに長く(1年ぐらい?)使ってないけど。そういうアルゴリズムが入っているのか。更新して終わりのようです。なんか意味あるのかな?

那覇空港は激込みでしたが、飛行機自体は空いてました。

明日から東京

でも、やってることは、こっちと差はないはずです。しばらく東京です。

カメラ用には16GBなSDカードを使っています。HD動画を撮りたかったらね。でも、

＊　撮りたいのと、撮るのとは別

で、思ったほど使わず。動画を撮るには「ここから、こう動いているシーンを何秒撮る」ってのを考えないといけない。後ろ姿を撮っても意味ないので、
山で走って、前に出て撮る。まぁ、ご苦労様なことです。沖縄に来てしばらくはムービーを持ち歩いていたのだが。

グリーンフラッシュの瞬間を撮りたいと思って、昨日も撮ってはみましたが、残念ながらダメでした。でも、なんだかかんだで、いくつかカードに
溜まっている。と言っても、100MBから500MBで、1GBとかはいかないですね。10秒は撮らないとだめだけど、1分のシーンとか撮れないもの。
会議撮っているわけではないからね。

でも、それをノートPCに保存するのは、ちょっと大きすぎる。NASとBitcasaに上げると言うのが最近の手順です。ここ数日、Bitcasa 結構、調子良い
感じ。しばらく激遅だったのに。

一人が使うディスク容量とか、しょせん限られているような気がする。Edge User は、そろそろ飽和しているんじゃなかろうか。もっとも、仮想マシン
イメージをぶち込んでいる人とかもいるらしいけど… 僕は Bitcasa は 6.8TB ぐらいです。既に Bitcasa に払ったお金で買える容量ではないな。
これが、そのペースで来年も増えるとはちょっと思えない。でも、10TBぐらいはいくのではないだろうか。そういうユーザがどれくらいいるのかは
良くわからない。Bitcasa は、その辺りの予測に命を賭けているのだろうけど、どんな感じなのかな。

ハッカーズチャンプルー

行ってきました。今回は、スポンサーちゃんといるので、なんと、

＊　ビーチパーティがただ

ぱちぱちぱちぱち。

長丁場でしたが、僕は、ゆっくり行ったので問題なしです。気持ちの良いビーチパーティでした。

　＊　＊　＊

Agdaでは、Hom(F(-),-)=Hom(-,U(-)) から随伴関手を導くってのに行き詰っていたんですが(逆はすぐにできた)…

あまりにわからないので、
<a href="http://en.wikipedia.org/wiki/Adjoint_functors">英語のWikipedia</a> を見たんですが

＊ Naaturality of Φ imply that

はぁ? そんなの聞いてませんが。で、ハッカーズチャンプルーを抜けだして、The Book (黄色のMacLaneのやつ)を
取ってきてみると、ご丁寧に可換図まで書いてある。つまり、この二日悩んでいた証明は…

＊　問題の仮定だった

らしいです(笑)。確かに、射の対応だけで、あんな複雑な式が出るわけない。その naturality は f = U(f*)○η で、 普遍問題の解そのものだったりするので、ちょっとあきれ気味です。随伴関手ってのは実は自然変換そのものだったのか。

ハッカーズチャンプル〜

前夜祭です。北谷なんだよな。バスのやりくりが難しい。

Agdaと圏論のまとめ

ここ数カ月(といってもAgda は7月かららしい)はまっていた、Agda と圏論の話をまとめて見ました。

<a href="http://ie.u-ryukyu.ac.jp/~kono/lecture/software/Agda/index.html"> Agda による圏論入門 </a>

入門と書いてあるけど、全然入門ではないといういつものパターンだな。自分のための覚書みたいな感じ。
もう少し可換図とか入れたい(Ascii art でない...)

Agda だと、github に証明載せて終わりというが多いみたい。本文中にコメント書くので十分か。

o2html に前のページ、次のページを付ける option とか、link の check とか入れないとだめだな。というか、
Wiki / WordPress にしろよっていう説もあるんだけどね。それも難しくはないんですが。

朝まで飲む

いや、だから、もう若くないんだからさぁ。いつものお店に呼び出されたら、そこにいうつもの呑み友達が待ち構えていて... 結局、朝5時まで。
まぁ、やっぱり泡盛は楽だよね。でも、最後は残波だったので、ちょっと二日酔いが残っている感じ。菊之露が良いんだが。
ナカヌヒだったのですが、親戚づきあいが終わってくる人たちで屋富祖は遅くから賑わってました。

まぁでも、4-6月の体調の悪さを考えると、元気になったということかな。

8月誕生の男性は多いみたいな説があるらしいんですが、子供の頃は学校休みだし、お盆に近いので、だいたい忘れ去れれていたはずです。
女性と違って、男性は誕生日にはあんまり思い入れないし。

TNG で、Mr. ウォーフが平行世界でトロイと結婚しているとかいう話があって、そこで、ライカー副長が誕生日のびっくりパーティを
企画したのをトロイが止めるって話があった。あれは良い話だったな〜 そう言えば、TNG のHDリマスターは、日本のNTSCレベルですが、
今までのぼけぼけのものよりははるかに良いです。この話がHDで見れるのは何年か先? まぁ、Blu-ray 買っても良いんだけど。

別に普通な日です

いろいろありがとうございます。

(と、あっさり片付ける) 世間では、ウークイ、ナカヌヒと来たおかげで、お店が全滅。街はがらがら。 大学は「一斉休暇」だったらしいです。

でも、何故か普通にゼミやってました。世間のペースと、まったく関係ない感じなのが、むしろ、それっぽいか。

証明とは非常に個人的なもの

もちろん、今までにない証明なら話は別ですが。

今朝もうっかりAgdaで Free Monoid の普遍問題と朝5時まで。そういうのやる年じゃないんだけどな。中毒性あるって
話だったけど、確かにそのとおりです。

わからない時はググって見るわけですが、ばっちり同じ問題をやっていても、かなり違う。Agda は式の変形が付いているだけ
かなりましで、Coq の証明は読むための証明じゃないからなぁ。Agda でも、

<pre>
unique : (xs : List A) → γ ′ xs φ xs
unique [] = ε-homo
unique (x xs) = M-trans (-homo [ x ] xs)
(M-trans (-cong (eq x) (unique xs))
(-cong (proj identity (f x)) (M-refl {φ xs})))
</pre>

とか書いてあってもわからないよ。

でも、

Kleene Closure is Free Monoid
http://www.proofwiki.org/wiki/Kleene_Closure_is_Free_Monoid

こちらはわかりやすい。

日本語Wikipeida の Monoid / 普遍問題を書いたのは誰なんだろう? 昔は、もっとまともだったと思うのだが、
可換図さえないって、どういうことなのかと小一時間問い詰めたい感じです。

でも、証明って全部書いてあるわけじゃないんだよね。自分で証明を追うとの読むのとではかなり違う。それと同じくらい
Agda で書くのは違う感じ。

また、人のAgdaの証明があっても、かなり違っていることが多い。Agda は特にトンデモ記号を使う人が多い。おかげで
7x14 なフォントをだいぶ作った。

Reasoning という式変形の部分に手を入れたりすると、Emacs よりも Customize されてしまう感じ。Agda は、あくまでも
自分のためのものなのかも。

もちろん、library はちゃんとしているんだけどね。

300行ぐらいの証明が多いので、行き詰っても「あらゆる組み合わせを試している」うちに、なんとかなってしまうことが
多いようです。新しい関数を作るとかは難易度高い。

JICA

最初に来た頃、一回だけ講演したことがあるくらい。あんまり縁は無いです。前の教授の喜屋武先生が、ケニアと良く行ってました。学生を沖縄に連れてくるとか、ちょっとブラックな感じもするが... たまに優秀な学生が。一度、トンガに送り込まれそうになったが、他に希望者がいたようです。

いろんな人がいるのは面白い。食堂もハラルとか置いてある。もっとベジタリアンメニューがあっても良い気もするんだけど。ちょっとだけ寄ってカレーを食べてみましたが普通でした。ちょっとがっかり。

一回休み

どう考えても飲み過ぎだろという一週間だったので、今日はお休みです。

昨日はアウグス ビア ダイニング オキナワで、ビール何杯飲んだかは良く覚えてないんですが、途中でめんどくさくなって、同じ銘柄ばかり頼んでいた。一つだけ超苦いのがあったな。

http://tabelog.com/okinawa/A4701/A470103/47009532/

ビールの方が、翌日少しきつい。Mou のせいで最近はビールが多いかな。

鍵

琉大OBとごきげんで飲んでいたら、なんか「イベント発生です」とかいう電話が。「鍵を前のお店に忘れた」と。

で、タクシーでお店に行って鍵は確保したんですが、落とした本人に連絡が取れず。いると言った場所では「10分前に出ました」あらららら。

Facebook にメッセージがあって、無くした人が僕の考えていた人とは別なことであることが今朝になって判明。沖国大近いので、お昼に寄ったら「不在です」あだだだだ。

結局、琉大に取りに来てくれて渡すことができました。めでたしめでたし。

外延性

昨日も(っていうか今朝まで) Agda いじてっていて、なんか珍しく口内炎くらいました。

Monad のいつもの例題をいじっているだけ。しかも、

＊ T : A -> M x A ( A は集合、Mは Monoid 、x は直積)

という極めて簡単なものなんだけど、ある意味で簡単なものほど難しいものだよね。こいつは Haskell では簡単に書けたのに、
Agda では、まったく歯が立たず。 http://seeker-s-eye.blogspot.jp/2013/08/monad.html

Haskell にそって data とかを定義して、それを圏にしてとかいうのは、途中まで頑張ったのですが、どんどん違う方向に
いってしまう。でも、そこで Monoid の要素が Carrier という名前の Set だというのがわかりました。

そこで、最初の頃に作った、Sets (既に定義されている圏で、射が Agda の関数 ) と直積を組み合わせる方向に戻って、
みたら、あっさり、T と ηとμが定義できた。しかも、

＊　　結局、教科書に書いてあるとおりの定義

いや、もちろん、そうでなければならないんだけどさ。

＊ FObj = λ a → (Carrier Monoid) × a
＊ TMap = λ a → λ(x : a) → ( ε , x ) ;
＊ muMap a ( m , ( m' , x ) ) = ( m m' , x )

なんとなく、信用してなかったようです。で、そこから楽勝。だと思ったのだが、Monad の性質を満たすことの証明が、まったくできない。全然できない。

＊ ( λ x → (( ε (proj x)) , proj x )) = ( λ x → x )

を示せば良いだけで、εが Monoid の単位元で、( ε (proj x)) が (proj x) を返すとわかれば、

＊ ((proj x) , proj x ) = x

つまり、直積はその成分の直積だってことで、これ自体は簡単。なんだけど、どうしても証明できない。λ x -> x のλ x を
cong で構成するとかやってたのに歯が立たず。で、証明できない式自身、

＊ (f x ≡ g x) -> (( λ x -> f x) ≡ (λ x -> g x)

でググってみたら、

＊ http://math.stackexchange.com/questions/154704/if-fx-gx-for-all-xa-why-is-it-not-true-that-lambda-x-fx-lambda
＊ If f(x)=g(x) for all x:A, why is it not true that λx.f(x)=λx.g(x)?

え? 証明できないの? はぁ?

＊ http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/
＊ function extensionality

というものらしい。

＊ ∀x -> (f x ≡ g x) -> f ≡ g

ってのを公理して仮定しろと。確かに、Agda の library にも仮定(postulate)するように式が書いてある。超良くある質問らしいです。

そう言われて見ると、ZFの 外延性の公理 (extensional principle )

＊ ∀ {x} x∈ f ⇔ x ∈ g → f ≡ g

と(要素がすべて同じなら同じ集合)にクリソツ。これを仮定したら、ちゃんと証明出来ました。朝の5時に。あだだだ。 これも元の本では三行なんだよな。

ラーメンフェスタ2陣

あんまり頑張ってません。虎威原と鍵です。

ですが、既にカード無くしたみたい。そういえば胸ポケットに入れて、しばらくそのままだったような。この前、胸ポケット掃除したような。がーん。

ま、いいか。

学生も「卒業したら東京だから Topping pass も時間的にあまり使えない」とかでエンジンがかかってない様子。

とか言いながら、ちょっと脂っこすぎて帰ってきてからダウン。最近、そういうのたまにある。いや昼間泳いだからか。今日は、それほど混んでませんでした。

海抜131m

琉大は海抜131m。沖縄の＊山＊の上ですので。311 以来、そんな表示をするようになったらしい。

中部商業辺りから、がんがん登るので、歩くととっても疲れます。汗かきます。歩くの嫌いじゃないけどね。

古波蔵あたりは低いので危ないのですが、東シナ海側なのが救いかも。もっとも太平洋側だけ心配すればよいかというとそうでもないんだけどね。

Monad の例

最近、はまってた Agda の例をまとめているんですが、(何回目の清書だよ) そういえば、Monad の例がない。例がなくても証明がどんどん進むところが圏論っぽいところなんだけど。

Higher order categorical logic に載っている例が、

T : A -> M x A ( M は monoid )
η : a -> (1,a)
μ : (m, (m', a ) -> (m*m', a)

っていう例でなかなか良くできてます。これを Haskell で、そのまま Monad として動かすのもできた。

なんだが、Agda で全然書けない。Agda こういうの多いんだよな。どう書けば良いのかさっぱり。本来、T ってのは、圏A に対して、

T : A -> A

だったよね? T : A -> M x A を Sets -> Sets と考えると本には書いてある。それって、Agda では、どうするんですか?

(1) Sets と直積を使って T という Functor を作る
(2) M x ( M x ... A )) っていう圏を作って、その上にTを定義する

の二種類の方法を考えて、どっちも、そなりに途中まで書けたんですが、なんかだめ。だめだ。これじゃない感です。なにか思い違いしているんだろうな〜

例がないってのもあんまりだし、実際の Monad と結びつかないってのもまずいからなぁ。

土曜日は xhago に顔出して懇親会にも寄って来ました。アプリ作りましたみたいなのが多い。良いね。次はハッカーズチャンプルーが8/24。その後から東京かな。ソフトウェア科学会まで、しばらく東京の予定です。

XHago4

やってるみたいです。

http://hago.doorkeeper.jp/events/4396

夏休みに入っちゃうと学生が大学に来ないので、その前の方が良かったかもね。いや試験期間に当たると、それもだめか。

　　＊　＊　＊

使っている blog ( http://seeker-s-eye.blogspot.jp ) の検索がうまくいかないのはちょっと気になっていて、少し調べてみると、

＊ bloggerの検索ガジェットでうまく検索できない

で検索すると良いらしい。

ところが全然動かない。そこで、

＊ Google Custom Search https://www.google.co.jp/cse/all

ってのを使ってみます。URL を指定するだけね。簡単。生成された URL を HTML/JavaScript Gadget として貼れば良い。 ところが

＊　　全然動かない

もしかして、blog の設定の問題か? と思って設定を見てると、serach は全部許可してる。なんだが...

Blog Address
Warning: You are using Google+ Comments. Changing the blog URL will negatively impact existing comments. Learn more
seeker-s-eye.blogspot.com

と書いてある。jp じゃなくて com? そう言われて見ると、

＊　いったい、いつ jp になった?

そこで、URL を com にしてみると、ばっちり動きました。なんなんだ。

なんだけど、テストしているうちに、左上に Search とか出てるのに気がつく。navbar というらしい。そこで探してみると、

＊　　問題なく動く

ななななななんだよ。

いや、確か、昔、そこはちゃんと動かなかったんだよ。ような気がする。ということにしておこう。ということで、せっか付くけ加えた Search は外しました。ま、良くあること。

障害物競争

さすがにシーズンなので、プールが混んでます。がきんちょ避けながらなんだけど、横から飛び込むのはやめて欲しい。

都内のプール並みに混むのはお盆の周辺だけなみたい。午後2時ぐらいが「子供のお昼寝タイム」なので空くみたいです。

むかーし、豊島園のプールとか後楽園のプールとか行ったような気がする。とっても混んでいた気がする。お正月の東京のスポーツクラブも混んでいた。それに比べればどおってことありません。

問題は来週/再来週だな。混むだろうな〜 8月の間はプールお休みしても良いんだけどね。(軟弱)

LLVM をいじる

なんか、ぜんぜん gdb の break point がかからなくて。-v 付けてみたら、なんか長いオプションが。その長い option で fork exec しているわけね。それでは、break point に引っかからない。なので、その長い option で起動してやると良いようです。どれくらい長いかというと、

"/usr/bin/clang" -cc1 -triple x86_64-apple-macosx10.8.0 -emit-obj -mrelax-all -disable-free -disable-llvm-verifier -main-file-name test1.c -pic-level 1 -mdisable-fp-elim -relaxed-aliasing -masm-verbose -munwind-tables -target-cpu core2 -target-linker-version 134.9 -v -coverage-file test1.o -resource-dir /usr/bin/../lib/clang/4.1 -fmodule-cache-path /var/tmp/clang-module-cache -fdebug-compilation-dir /Users/kono/src/device -ferror-limit 19 -fmessage-length 153 -stack-protector 1 -mstackrealign -fblocks -fobjc-runtime-has-arc -fobjc-runtime-has-weak -fobjc-dispatch-method=mixed -fobjc-default-synthesize-properties -fdiagnostics-show-option -fcolor-diagnostics -o test1.o -x c test/test1.c

これぐらい。

なんだけど、gdb で break point 掛けるたびに沈黙。

「ねぇ、そのノートPC、メモリどれくらい?」
「4GBです。」

あぁ、無理無理、全然無理だよ。4GB のメモリで LLVM を追いかけるとか無理無理です。だからといって、16GB なら楽勝ってわけでもないんだろうけど。もちろん、debug しなければ、そんなには食わないんですが。

それようの強力なマシンがあるんだから、そっちでやれば? ノートPCでやりたいのはわかるけど。

カップ麺リフィル

いや、それカップ麺じゃないだろと思うんだけど。朝カップ麺最近多いかも。なので、奥様が箱買いするのだが、リフィルを使うと、ゴミが少し減ります。いや、僕は「コーンとんこつ」が好きなんですが。

なんだけど、この間、パイレックスのカップを一つ割ってしまいました。やかんを移動する時にぶつけて割れちゃった。残念。で、安いという理由でプラスチックなカップに。

まぁ、それは良いんだが「使い終わったら洗剤に漬けといて」とか言われる。まぁ、プラスチックなので色が付くのが嫌なのわかるけど。

わかるが、納得はできないな。パイレックスのでいイイじゃんみたいな。

駐車場

新しいビルが出きる関係とかで、大学の駐車場を拡大しているみたいです。琉大は山のてっぺんなので、放っておくとジャングル。草刈りしても、しばらくすると背の高さの草が生えるみたいな、そんな感じでした。

工事中は、結構遠回りさせられる。と言っても、その道は、

＊　大学の正規の地図には載っていない裏道

だったらしいです。環境建設とかが、勝手に道を作ってしまうらしい。いや、一応、街頭とかも後では整備されていたんだけど。

何故かあった「暴露試験場」も、なくすのかと思いきや復活するらしい。台風でひどいことになっていたのに。

駐車場ができると、駐車場を通って歩くみたいになるのか。まぁ、仕方ないかな。

バグの入れ方

学生と一緒にペアプログラミング、というよりは、学生に gdb や Editor を操作させてデバッグやプログラミングってのをたまにやります。それなりに面白い。

なんだけど「動きません〜」って声が。いや、だから直してよ。と言っても進むわけではないので土曜日にちょっと見てました。酒のんで帰って、すぐに直せたんですが...
(最近の、その酒飲んで帰ってから、またプログラミングするのって、良くないんだよな...)

「え〜、こんなの書くはずないんだけどな」ってのがいっぱい。まぁ、学生も変更しているので当然なんだけど。で、Mercurial で「ここを書いたの誰?」ってのをやってみたんですが。

あぁ、あの時かぁ。3/29 みたい。確かに、Editor の操作をさせてて「あれ?」と思ったんだよな。そこで、 2行コードを関数間で移動した時に、

＊　　2行の順番が狂った

そういうバグでした。あれっと思ったんだが「学生に取ってもらう」と思ったような記憶がある。

http://seeker-s-eye.blogspot.jp/2013/03/blog-post_29.html

これだな。この時のはバグが多くて、結構、後までたたってた。やっぱり、その場で動くまで持ってかないとだめか。テストが少ないからそうなるとも言えるし。

風立ちぬ

観てきました。昼間は混んでいたみたいだけど、18時の回はがらがら。

割と何も起きない話。帝大から三菱、外遊から抜擢というエリートコースな人の話なので、まぁ、そんなものだとも思う。そんな時代もあったな〜という感じで観てました。書いてないところを観る映画でもあると思う。

計算尺が良く出てくるけど、特に話しとして使われているわけでもなく。家具職人だった父が大きなのを愛用していた覚えはあります。

＊　カーソルを使った繰り返し計算
＊　逆数を使った割り算
＊　尺を固定して定数計算
＊　副尺を使って一桁精度を上げる

辺りを入れて欲しかった気もする。でも、自分で思い入れがあるわけでもなく。実家にはあるけど手元には、もうないな。

つけとどけ

なんか研究室OBが、研究室につけとどけするのが流行ってるみたい。昔から、たまにあった。

＊　カップ麺
＊　野菜ジュース
＊　Red Bull New!

Amazon から直送だと、誰から来たかわからんぞ。

Red Bull? 決して、うちの研究室はブラックではないんだけど。ただ、

＊　夜行性

なだけでさ。11時に来たら、誰もいないというパターンです。

今週末は、福島 Game Jam をやってるみたいです。一応、沖縄も同期してるのかな? やってる?

Mac 率高いな。

https://twitter.com/SquashSesame/status/363537498841939970/photo/1

Meeting の合間に Agda

Agda の合間に Meeting かどうかは知りませんが、そんな感じでした。10分あると、一つ証明できるか。

証明時は難しくないことが多いけど、データ構造を決めるのが難しい感じ。あとで再利用する時に祟るし。

プログラミングと証明とは同じということだね。難しい気もするけど、基本はそれほどでもない。アセンブラに相当するのが、項書換だというだけですね。

それにしては、はまりまくることが多いけど。