先生に似る

ふっと、本田耕平が Edingburgh から CSL に来て少し話を聞いた時に、

＊　話し方が Milner 先生にそっくり

になっていたのを思い出しました。あぁ、まぁ、そういうのあるかもな〜

自分が影響を受けた先生って誰だろう? 中学受験の時の先生とかか?

篠田陽一教授とか僕とかに話し方が似ると、それなりに不幸だとは思う... 気をつけてください。

viper-mode

Emacs の vi emulation です。vipper と書いて笑われた。むかーしの佐藤先生の vip-mode の拡張らしい。

Agda で、Emacs のキーにだいぶ苦しんだので入れて見ました。やっぱり快適だな。

＊ () の対応で % でそこに飛べる
＊ 行内サーチ f とか F とか
＊ cut&pasteの振る舞い。ddp とか

なんだけど、いつものことだが、少し違う。

＊　u が1つしか戻らない。

いや、vim が複数回戻れるだけなんだけど。viper は複数戻れると書いてあるので、なんかのバグかも。このせいで、"1p . が効かないのが痛い。痛いです。Emacs の undo が効くので、まぁなんとか。

w とか f とか / とかないので、Emacs だと、

＊　カーソル移動キーを押しっぱなしにする

という風になっちゃう。incremental search はキャンセルすると元の場所に戻ったりするし、ピーピーうるさい。

そういえば、viper も ESC を複数打つとピピとなるのでうっとうしいです。何故かデフォルトで、

＊　ESC の後、すぐにキーを入力すると Emacs の振る舞いをする

という風になっている。ESC で h とかやると、

＊ emacs の help mode に入り、h で世界の Hello を表示する

ということになるみたい。ふーん、便利だね〜　教えてもらってさっさと停めました。そうすると、

＊ ESC-X で Emacs の command に入れなかったのはなんで?

どうも、Emacs では「ESC-X のESCはゆっくり押す」という癖が付いていたみたいです。vip-mode のせいかなぁ。代わりに C-\ x で入るらしい。

ついでに、C-Z は viper が食ってしまうらしく、一度、C-\ x しないと suspend できないみたいです。

あんまりカスタマイズしてもしょうがないので、やらない方針だが、~/.viper にゴミを入れられて起動できなくなったとか、いろいろひどいです。

まぁ、でも、これで Agda を扱う苦痛が少し減った。

Toropical Game Jam 発表会

11時から発表なので、行ってきました。テーマは自然だそうです。

＊ 2D 音ゲーっぽい、神様が地球をはぐぐむ
＊ 2D バイクで夕日を背景に走る bike natural
＊ 3D 雨の街から脱出 rain town
＊ 3D 猿が木をひたすら登る
＊ 2Dな3D ドリルでひたすら掘る
＊ 花と虫のタワーディフェンスで地球のバランスを維持する
＊ 羊が、ステージの上で爆弾と戦う (Network 対戦!)

ってなのでした。

デザイナーさんが超優秀で、絵が可愛い、綺麗。特にバイクと Rain Town 。二日でここまでできる。技術的には、羊のが難しかったかも。でも、ゲームの面白さはプログラミングの難度とは関係しないからな〜

いや、ソースコード読みたいんですが。

今回は全部、Unity でした。まぁ、便利でいいんじゃない? ちょっと問題もあるけど。

まだ「あのゲームを作ろう」という段階で、全く新しいゲームを作るというところまではいかないみたい。そういうのは、ゲームを作り飽きてからできるものなのかも。

今回も自分で参加するのはパスでしたが、流大生が5人ぐらい参加してくれました。なんか来週もあるらしいが... そして、年末には Global Game Jam が...

Game Jam Okinawa

というわけで北谷に来てます。でも、様子を見に来ただけです。自分は Agda やってます。ちょっと行き詰まってるかも。いつものことか。

3回目なのでだいぶ慣れてきている感じ。いや、僕はやったことないんだけど。この手の物って、

＊　回数こなして、スピードあげる

ってのは重要だからな〜

僕もゲームは何回か作ったことはあるけど、こういうグループワークはやったことないな。今度は参加する方に廻ってみようかと思うけど「一晩」ってのがな〜

証明と詰将棋

大半は答えのわかっているものを再度証明するわけだから。

でも、自分で追ってみない限り、絶対に理解できない。

おんなじようなものだな〜

そういえば、大学時代に詰将棋にはまって「これはダメだ、やめよう」と思って詰将棋はやめたのだった。

TeXLive and EasyPackage

epkg の TeX の version が古いのはだいぶ気になっていて、今日は、gradle かなんかを EasyPackage で入れるのを M2 に教えた ( M2 で習っても手遅れだが ) ついでに、MacTex を EasyPackage 化するのをやってました。

でも、簡単には動かないだろうな〜

やり直すたびに、2-3GB のcopyが始まる感じ。

＊ (1) Download
＊ xar で mpkg を展開
＊ gunzip + cpio で pkg を展開
＊ それを一度 copy して、plist を作成
＊ さらに install で copy
＊ package を tgz で作成

ってことで、6倍ぐらいcopy するらしい。

で、なんか、動いたっぽいです。 (いや、まだ、いろいろ問題はあるだろう。man path 設定してないし )

まーみなーチャンプル

チャンプルーは、ルーが上がる感じなので、チャンプル〜みたいな表記の方がそれっぽい気もする。

コンベンションセンターの歓海門近くのうみちか食堂で

＊　マーミナーチャンプル、ご飯半分、ポーク抜き

と言ったら、もやしと豆腐以外なにも入ってませんでした。これはさびしい。しょうがでいいや。しょうがないし。みたいな?

また中部商業登ったので汗だく。でも、汗かくと血圧は下がるね。医者に行く時に血圧が低いのはそれか。

Universal mapping

なんか、意外に早く終わった。って、朝の四時までやってれば解けるさみたいな。380行ぐらいでした。

Universal mapping から Adjoint Functor って圏論の初期の壁だと思うんだけど、

＊　やさしい部分と難しい部分が混在している

感じ。と言っても、数学者に言わせれば、まだやさしい方なんだろう。

Agda の証明は紙で書いて、textで書いて TeX で書いての延長だけど、Adjoint Functor から Universal mapping を出す部分で、解の一意性を出すのを忘れたいたのを見つけました。

逆方向の証明をする時に解の一意性を使うわけだけど、その定義を Universal mapping を表す record に記述すると、Adjoint から導出する時に、その部分も証明しろと言ってくる。

で、すごすご証明し始めると、解の存在の方では Uε○ηU = 1 しか使わなかったのに、一意性で、Adjointのもう一つの条件 εF○Fη = 1 を使うことになって、なるほどそういう対応かと理解しました。確かに片方しか使わないのは変だと思っていたんだよな。

C-C C-A とすると、? を自動的に埋めてくれるらしいんですが、

＊　まったく役に立ちません

Agda 潔くて良いよ。まるで証明の手書きツールのようです。

＊　＊　＊

近所のライトビルのお店、待夢は、あのビルにしては長い営業だったのですが、今週で締めてしまうらしい。なので、今週は三千円飲放題だそうです。特に思い入れがあるわけではありませんが、たまに寄ってました。

Monad合成

Monad合成はできました。

http://www.ie.u-ryukyu.ac.jp/%7Ekono/lecture/software/s07/lecture.html

こんな感じでできるらしい。明日の授業のネタだけど。こんな自転車操業でいいのか? これにも一週間かかった。慣れもあると思うけど。自分で Monad を書く話は、あまりぐぐっても出てこない。あまり書かないものらしいです。

昨日はせっかく飲みに行ったのに、Monad 合成の話が抜けなくて、結局、途中で帰ってきてしまいました。酒よりも、面白いものはたくさんあるね。

論文の締め切りも過ぎたので一段落かも。なので、Adjoint と Universal mapping の証明の Agda 版にも手を付けて見ました。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/tip/universal-mapping.agda

これで半分行ってないかな。 これも楽しめるな〜

選挙

投票券が玄関にあったらしいのだが、すっかり忘れて。でも、なくても投票できるのは知っていたので、そのまま。「券は?」「もってません」「家には着きましたか?」「わかりません!」すると、その場で券を手書きで書くのね。ご苦労様です。免許証見せたけど、身分証明書も不要らしい。まぁ、住所書いてあるのであった方が便利。

免許証返上しても代わりの身分証明書を出してくれるそうだが、いつまで出してくれるかは謎。そもそも有効だと受け取ってくれるのかも怪しい。

実質的な選択肢があるわけではないんだけど、世代別の投票率は議員は見るはずなので、投票自体は重要だと思います。が、そこまで考えない人は多いだろう。投票したら税金キャッシュバックぐらいやっても良いと思うけどね。千円でも効果あるでしょう。

オープンキャンパスでした

出し物は、OSC とほとんど同じ。なんだけど、ちょっと足りないと判断して去年の Alice の水族館も出してもらいました。ちょっと手抜き感もあるが、こんなものだろうな。論文の締め切りと重なってたし。

プロ3の学生が、またしょうもないゲーム作って持ってきたので「え? スタンダアローン? 大学生でそれはないだろ? 」と突っ込んだら、当日にはネットワーク対応になっていました。やればできるじゃん。

今の学生に「琉大のオープンキャンパス来た?」と聞くと、

＊　山田先生のヒトデロボット

とかの他に「河野先生がいました」とか。確かに出し物自体よりも先生を見る方が面白いのかも。というわけなので効果があるかどうかは良くわからない。まぁ、こういうイベントは嫌いじゃないです。学祭とスケジュール合わせれば良いんじゃないかとも思う。

1時から4時半は、ちょっと疲れた。展示説明の学生も音をあげてたし。お疲れ様でした〜

そんな面白グラフがあるなら、ちゃんと論文に載せろよ

とかなんとか、学生の論文に突っ込んでいると、いろいろ出てくるので面白いです。血圧は上がるけどね。

いろんな主張の根拠に測定するわけだけど、出し惜しみってのは珍しい。

ソフトウェア科学会は今年は東京の年らしいので、9月あたりには東京にいるはずです。

少しずつ進む

昨日のわけわからんバグは、単にループで使う変数を Thread で共有された場所に置いておいたせいでした。だいたい、
バグなんてそんなもの。今まではそういう共有は起きなかったのだけど、自分で入れたのを忘れてた。gdb で目の前で
値が変わったのを見て、ようやっと理解しました。

Monad の合成の方は、一引数つまり余計なパラメータを持ってない Monad の例題は動いた。でも、自分で書いた T [m]
の例題は動かず。なんか間違ってるのか、はたまた、実はできないのか。できない可能性もあるな。

学生たちが論文書いているので今日は帰れないの? そうなの?

堅むすび

Lawson で見つけて、最近、気に入ってます。

＊　量が適当で

＊　甘くなくて

＊　割とまともなせんべい

今日は、最初のバグは簡単に取れたけど、最後のは絶対ありえないだろっていうバグで、ありえんで終わりました。マルチスレッド絡みであることは確かだが...

Monad の合成

学生の(いや、社会人でもそうかも知れないけど)デバッグを見てると、大半は、printf debug 。まぁ、一番お手軽。それに、source code debugger が使える状況は、かなりラッキーなわけだし。

なんですが、Haskell は PrtStrLn とかを任意のところに挟むわけにはいきません。こいつは IO Monad なので。 例えば

    fact1 0 = return 1

    fact1 n = do

        putStrLn (show n)

        c <- fact1 (n -1)

        return  ( n * c )

とかは、問題なく動くんだけど、自作の Monad をはさむと、

    fact4 0 = return 1

    fact4 n = do

        putStrLn (show n)

        c <- fact2 (n -1)

        Tn [c] ( n * c )

これは型エラー。これは Monad T1 を返す関数なんだけど、 putStrLn (show n) は IO を返すので、それが衝突してしまう。

    mylift  m  =

      Tn [] ( do

           c <- m

           putStrLn (show c)

           return c

      )



    fact2 0 = return 1

    fact2 n = do

        mylift $ putStrLn (show n)

        c <- fact2 (n -1)

        Tn [c] ( n * c )

とすると、mylift が IO a -> T1 なので、型は合います。合いますが、IO Monad を誰も触ってくれないので印字してくれません。これは誰も見ない printf だから消されてしまったみたいなものだな。

つまり、IO Monad と T1 Monad が合成できれば良いわけね。調べてみると、

http://www.slideshare.net/tanakh/monad-tutorial

http://d.hatena.ne.jp/m-hiyama/20070507/1178496486

全然自明ではないらしい。Haskell 内蔵の Error とか Maybe とかには、ErrorIO とか MaybeIO とかあるらしい。

自作 Monad 用には、MonadIO とか MonadTrans とかあるらしいのだけど、

＊　使い方がまったくわかりません

うううう。困ったものだ。Haskell library の source を見てみるのだが、どうにもこうにも。困ったものだ。まぁ、時間が解決するとは思いますが。

Outline mode

編集している text を段落毎に折りたんでくれるあれです。 最初に見たのは、

＊ MORE

ですね。Mac 上のソフトだったはずです。どうやって見つけたのかは覚えてない。たぶん、Net News でしょう。超感動したのを覚えている。これだ〜みたいな。

でも、Mac 上でしか使えないから僕に取ってはゴミだった。で、そこで見つけたのが、

＊ Emacs の outline mode

です。MORE と、ほぼ同じ機能を持っていて、

* ほげ
ほげほげ
** ふが
ふがふが
* ふが
ふがふが

とか書くと折りたたみしてくれる。

MS Word も Outline mode を持っていて、それがベースになっているので、極めて使いにくくなってます。MS Word のわけわからない振る舞いは隠された Outline mode のせい。tab で下げた部分が変なのは誰もが体験していると思う。なのだが、もはや MS Word 入れてないので、どうだったかは試せないです。あらら。

で、それを * がいやだったので、- に直したのを今でも使っているわけですが、vim に移っちゃったので、outline mode は使えず。

といいながら、vim にもなんかあるらしい。:set foldmode=indent とか。zc とか zo とかやるのか。でも、indent なの? なんか、いろいろ設定できるようだが、今までのものとは互換性はないみたいだなぁ。

This will make a fold out of paragraphs separated by blank lines: >
:set foldexpr=getline(v:lnum)=~'^\\s*$'&&getline(v:lnum+1)=~'\\S'?'<1':1

これって何だろう。Emacs の outline mode に近くすることもできそうだが...

https://github.com/vim-scripts/Emacs-outline-mode/blob/master/syntax/outline.vim

これか? 一応、動くみたいだ。なんか怖いよ。close body ってどうやるんだろう。

もっとも、一部消せることに何か意味があるかというと、

＊　あんまりない

感じ。それよりは、画面を大きくして全部見る方が良い気がする。閉じたり開けたりめんどくさいし。

Idea processor 的に、Outline を使いたい時には FreeMind 開けることが多いです。つまり、

＊　Outline mode と、論文や資料書きモードは異なる

ってこと。なので、普段の editor に outline mode は必要ないのかも。

git and mercurial

Agda の Category は github 上にあるので、せっかく、Reasoning 書いたので、pull-request してみました。

＊　github 上で fork

＊　fork したものを local に clone

＊　さらに branch

＊　そこで変更して commit

＊　github 上の fork へ push

＊　pull request を送信

長いんだよ。branch するのが礼儀らしいです。なんだが、ちょっと間違えた気もする。でも、そのまま入るわけもないだろう。

Git は、正直面倒。

　　　release 管理用の repository
　　　開発用の branch しまくり repository

で良いんじゃないかとも思うんだけど、一直線に管理したい人が多いのか。Patch 送りたいだけなのに git 経由ってのもなんだかね。

Mercurial は rebase もないので(最新のだと有ったりするのだが、disable されているらしい)、単純で学生向きだと思うんだけど。

だけど、ちまたでは Git Git と言っているのでミーハーな学生が僕の気持ちも理解せずに git を使ってしまうのは、まぁ、理解はできます。

でも、自分で git の変態コマンドと、妙な作法を教えると思うとなぁ。ちょっと苦痛。まぁ、やった方がミーハーには良いんだろうけど、その方が大変だと思うよ。

git の本は学性に自炊してもらったんだけど、雑なんだよな。中身的にもちょっと厳しかったし。今だと、おすすめの本はなんだろう。

マテ茶

地理の時にどっかの名産が「マテ茶」、どこかは忘れました。南米?

結婚した時に「お茶何にする?」と聞かれて「マテ茶」と応えていたら、どっかで売っていたらしく、出してくれました。これが、

＊　うまい

まったりした味で、ビタミンCが多いらしいです。葉っぱも食べる説があるらしいが、それはどうかなぁ。

この間、沖縄の自動販売機にもあった。なかなか、うれしい。

Agda 一段落

ここ数カ月はまっていた Agda と圏論ですが、目標のところまで到達しました。Kleisli 圏の射の結合法則が証明できてうれしい。手計算でも、かなりやっかいなものです。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/d9c2386a18a8/nat.agda

Agda には(Tutorialには載ってないが)、数式変形モード hoge-Reasoning というのがあって結構便利。で、これを Category https://github.com/konn/category-agda で使おうと思って、今週の 7/6 に「できた」とか言っているんですが、その全然動かず。

Agda の library にある ≡-Reasoning のソースコードを見ながら書くんだけど全然動かない。そいつは、≡という集合同士の等号なので、 という独自に定義した等号には無力。なので、

-to-≡ : {a b : Obj A } { x y : Hom A a b } -> A [ x ~ y ] -> x ≡ y

を証明しようとしたんけど、抽象的な圏には、　A [ x ~ y ] の定義がない。結合則とかの抽象的な定義しかないので、証明できないらいい。なので、

Category の性質として要求しちゃえ

ってことで書いてみたんですが、圏の圏 Cat で文句を言ってくる。一段、上の A [ x ~ y ] -> x ≡ y を一段下のものから作らないといけないらしい。圏の射は Functor だったりすので、二時間ぐらい Mou で頑張ったんですが諦めました。

で、もう一度、 -Reasoning を書き始めたんだけど、朝、動かしたら、なんか動く。え? 別に方針変えてないんだけど。どういうこと。どうも、7/6 に動いたのは、本当に動いたらしく、その時に、複数の Emacs を上げていたので、ダメなコードに置き換えられてしまったのではないかと。7/6 ぐらいのコードを見てみるんだけど、殆ど差がない。ええぇ。この一週間の試行錯誤はなんだったんだ。

でも、動いてめでたいです。

Agda は、だいたい 1行書くのに10分かかるらしい。作業は、

(1) recored IsHoge に公理を書いていく。
(2) recored Hoge に constructor を書く。
(3) recored Hoge に isHoge : IsHoge を書いて、公理を呼び出せるようにする

これが第一段階。

(4) 証明したい式を Lemma の型で書く
(5) 証明をλ式で Lemma = で書く

これが第二段階です。時間がかかるのは、(1)と (4) ね。(2),(3),(4) は自明なことが多い。いや、簡単なものならってことね。
い。いや、簡単なものならってことね。

    record IsNTrans {c c ℓ c′ c′ ℓ′ : Level} (D : Category c c ℓ) (C : Category c′ c′ ℓ′)
                     ( F G : Functor D C )
                     (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A))
                     : Set (suc (c  c  ℓ  c′  c′  ℓ′)) where
      field
        naturality : {a b : Obj D} {f : Hom D a b}
          → C [ C [ (  FMap G f ) o  ( Trans a ) ] ~  C [ (Trans b ) o  (FMap F f)  ] ]

    record NTrans {c c ℓ c′ c′ ℓ′ : Level} (domain : Category c c ℓ) (codomain : Category c′ c′ ℓ′) (F G : Functor domain codomain )
           : Set (suc (c  c  ℓ  c′  c′  ℓ′)) where
      field
        Trans :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
        isNTrans : IsNTrans domain codomain F G Trans

    open NTrans
    Lemma2 : {c c l : Level} {A : Category c c l} {F G : Functor A A}
          → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b }
          → A [ A [  FMap G f o Trans μ a ] ~  A [ Trans μ b o  FMap F f ] ]
    Lemma2 = \n → IsNTrans.naturality ( isNTrans  n  )

こんな感じ。変な記号が多いので読めるかどうか。\n は改行でありません。この例は公理を呼び出せるかどうかだけなので簡単。

複雑なものは、 Reasoning を使います。

 
      begin
         join k b (Trans η b) f
      refl-hom 
         c [ Trans μ b  o c [ FMap T ((Trans η b)) o f ] ]
      IsCategory.associative (Category.isCategory c) 
        c [ c [ Trans μ b  o  FMap T ((Trans η b)) ] o f ]
      car-eq f ( IsMonad.unity2 ( isMonad ( monad k )) )  
        c [  id (FObj T b)   o f ]
      IsCategory.identityL (Category.isCategory c) 
        f

こんな感じ。begin で初めて で終わる。目的の式に到達したら終わり。もちろん、証明したい式は型に書いてあって、この場合は、

-- η(b) ○ f = f
A [ join k b (Trans η b) f ~ f ]

こんな感じ。本当は、もっと長い。 x の x が式を変形するλ式ですね。実際には、

A [ (f o (g o h)) ~ ((f o g) o h) ]

とかを生成する関数です。refl-hom は、

A [ x ~ x ]

を生成してます。つまり、何もしてない。何もしてないが、join とかを展開することができます。

Agda はいろいろ癖がある。

隠れた入力変数がある

これが dependent type とか呼ばれる理由らしいのだけど、{} で書くと隠せる。() だと見える。ということは、

() と {} を目の子で区別していく必要がある

ってことね。これは非常に厳しいです。老眼には。Agda 作った奴があほだと思う理由の一つ。

隠れた変数は、実は {} で参照できる。わからなくなったら、全部手で{} で書いた方が良いです。そうすると何が衝突しているのかわかるので。

使われてない変数があると、黄色になります。なんで黄色になるのかよくわからなかったが、ようやっとわかった。使われない変数を消すと黄色は消えます。

Unresolved metas は、library が間違っている時に出るエラーメッセージ。

? と書くと、そこの型を表示してくれますが、あまり役に立たないことが多い。それよりも、

]] A→ A:

と続けるとエラー。大半のエラーがそれでしょう。Agda 作った人があほだという理由の一つ。() だけは許してもらえるらしい。

_[__] と _ [ _ _]

は違う。 お前なぁ〜〜 infix には英単語は使えないらしい。あと、

UTF-8 の特殊記号を使いまくるのが礼儀

らしいです。おかげで、7x14 にないグリフを随分作った。

式の変形に使う式で、中で出てくるものは引数として渡さないとだめらしい。{} にするか () にするかを気を付けないといけないってことね。

 
    A [ A [ A [ Trans μ d o  A [ FMap T h   o  Trans μ c ] ]  o  FMap T g ] o f ]
    car-eq f (car-eq ( FMap T g) ( cdr-eq  ( Trans μ d ) ( begin
           A [ FMap T h o Trans μ c ]
        nat A μ 
           A [ Trans μ (FObj T d) o FMap T (FMap T h) ]
        
   )))  
      A [ A [ A [ Trans μ d  o  A [ Trans μ ( FObj T d)    o  FMap T (  FMap T h ) ] ]  o FMap T g ]  o f ]
    car-eq f (sym assoc) 
     A [ A [ Trans μ d  o  A [ A [ Trans μ ( FObj T d)     o FMap T (  FMap T h ) ]   o FMap T g ] ]   o f 

という感じで、式の一部だけを Reasoning することも可能。ついさっき発見しました。

   
     car-eq f ( car-eq  (FMap T ( A [ FMap T h  o g ] )) (
     begin
         { }0
       { }1 
         { }2
      
   )) 

と部分を抜き出すと、

    ?1 : (A Category.~ A [ Trans μ d o Trans μ (FObj T d) ])
    (A [ Trans μ d o FMap T (Trans μ d) ])

と、0,2 に書くべき部分を教えてくれる。素晴らしい。これは便利だ。

証明チェック後の Read only を Writeに変える C-C C-X C-D を間違えて、C-X C-C C-D とすると、emacs を抜けて、xterm も C-D で抜けてくれます。

Agda を作った奴のアホ〜

と叫びましょう。

証明が終わると「何も(エラーが)表示されない」ので非常に達成感あって良いです。

だいたい手計算の10倍ぐらい時間がかかるんじゃなかろうか。いや、一週間、同じバグと格闘していただけだけど。手計算だと

( a + ( b + c ) + d )

( a + b ) + (c + d )

とかに直すの簡単だけど、Agda だと asocc 使って結構、苦労します。小学生が結合則を理解出来なくて試行錯誤するあれですね。まぁ、この辺りを自動的になんとかするものもあるんだろうが、

Agda は何もしない主義

らしい。いさぎよい。BSD 的だ。

まぁ、だいたい Agda は把握した気がする。いや、面白かったよ。Emacs と vi を交互に使って手がつりましたが。vi で、つい、同じキーを繰り返し押してたりして、だいぶ退化した感じ。

台風な夕暮れ

一日中 L [ x y ] -> x ≡ y と格闘していたが手がかりは得られず。Agda 難しすぎる。

今日明日、台風なようですが、それほどたいしたことはなく。去年も今頃は、同じようなことを言っていたはずだが、その後、強力な台風でアンテナ飛ばされたのだった。　

Video Feed Back

Tree VNC という画面共有のアプリを使っているので、結構、良く見ます。ハウリングと違って無害だが、うっとうしいかな。

だいぶ体調が戻ったので、1時間半泳いできました。そろそろシーズンなので、人もたくさん。いや、まだまだ、たいしたことはないか。夏休みとかだといもあらい状態になることも。まぁ、ご飯時とかの空いている頃を狙って。

お正月には東京のスポーツクラブの体験コースを使ったけど、結構、混んでたな〜

OS X のファイルの扱い

OS X と言えば、Time Machine なんだけど、iOS 側には、

＊ Save とか File 名という概念がない

アプリの名前はあるけどね。どうも、そういうものをなくそうという意図があるのかも。Folder とか。

OmniGraffle が新しくなって、Save as がなくなった。僕は、

＊ 今書いた図を修正して、それを Save as で名前を付ける

ってのを良くやるんだけど、Save as がないので、ちょっと困った。つまり、

＊　今書いている図をコピペして、新しい図にペーストしてから始めろ

ってわけかな。File メニューは、

Duplicate
Move to
Rename

にさらに、

Revert to

があって、任意の版に戻れる。なので、Save as で、はまっても大丈夫。これは Time Machine と連携した機能になってる。

File system 上の log

と

Time Machine 上の log の複製

と両方あるので、TM の HDD が接続されていなくても、local なファイルシステム上で残っているなら、戻れると言うわけね。そういえば、VMware Fusion も、そんな機能があった。

TextEdit も Save as ないので、そういう風に変えていくつもりなんでしょうね。Duplicate して Rename なのかな。

Agda の続き

OSC の最中にやっていた部分は順調だったんだけど、式変形を行う一種のマクロみたいなものが Agda にあるので、それを Category.agda で使えるようにしようと言う部分で、

＊　日月、二日間一歩も進まない

ってなんなの?

まぁ、そういうこともあるさ。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/2b005ec775b4/nat.agda

これの module -Reasoning ですが、誰か助けてくれるとうれしいです。とか投げてみる〜

ラグナガーデンホテルも、いよいよシーズンで、プールも、ちょっと混んできました。例年より早い感じ。やっぱり、少し景気良くなってきたみたいだね。

OSC Okinawa 当日

いつも通り、学生の発表資料がたこたこで。でも、発表当日よりは前日にぼこぼこにされた方が良いよね? ぼこぼこにすると、だいぶマシになるようです。最初から考えてやれと思うが、まぁ、それを教えるのが仕事でもあるからなぁ。

今回は Haskell 入門みたいな感じにしてもらったのですが、説明不足なスライドばかり。

「ソースコードは一つに絞って、それだけを丁寧にやれば?」

まぁ、そういうことをすれば少しは理解も深まるのではないかと。

そんな感じで、大学に泊まってしまったんですが、泊まった理由はどちらかといえば、

＊　Agda にハマったから

Agda 危ないです。詰将棋みたいな面白さがある。

(1) 型の部分(record の field) で自然変換やMonadが満たすべき性質を書く

(2) そいつのconstructorを別に作る (ここは比較的やさしい)

(3) 証明したい式を型で書く

(4) その型にあった証明を(1)や(2)で定義した関数の組み合わせdで書く

という方式。徐々に、進んでいけるのと、型が先導してくれるので、割と順列組み合わせでできる。その場で使う関数は、それほど多くないので。

コンパイラ書いている時も同じような感じなったことがあったっけ。

というわけなので、OSC 最中とっても眠かった。さて、次は懇親会か。

風樹館

なんか琉球大学の委員会の関係で、17年間一度も行ったことのないビルに行ってきました。そういえば、あれはなんだとは思っていたのだった。

Web を見ると資料館とか書いてあるけど、最近、博物館になったらしい。昆虫とか生物とかの標本がたくさんあるらしいです。それを、

＊　常勤一人

で管理しているらしく、予算も低いらしい。それでも変な装置とか置いてあって面白い。生物とか生態とかは流行の分野らしく、そういう関係の先生方は元気にどうするあーするとか話していました。

結構、Web が良くできているが(安く)頑張った人がいるらしい。ありがとうございます。

OSC Okinawa 2013

OSC Okinawa 2013年7月6日(土) 10:00-17:00（展示は15:30まで） 会場：沖縄コンベンションセンター 会議棟B　　https://www.ospn.jp/osc2013-okinawa/

今年も出展します。今年の出し物は、なんと、

＊　Haskell を使った Web Service の作り方

と、プログラミング3 の学生による

＊　学内学生追跡システム
＊　Unity によるゲーム

です。

学生は(那覇の)懇親会に参加してね。今日中に申し込もう。

録画厨

昔は、見て消しでしかビデオは使ってませんでした。一つのビデオテープを使い回していたな。あまりテレビ見なかったし。Vガンダムとかは、そういう見て消しで見てたはずです。

Hi8 とディレクTV(スカパー)を使うようになって録画するようになったみたい。Hi8は場所取らないのがすばらしい。VHSの1/5だったはず。VHS や D-VHS をたくさん溜め込んでいた人もいたはずですけど。

DVD/BD になって、昔のHi8から、移したものはわずかです。自分で撮った映像とか家にあった 8mm フィルムとか。「だいたいスカパーで再放送するし」。DVD/BD に移行したのは「そっちの方がメディアが安くなったから」 DVD-RAM 一枚1000円とかした時代だった。

DVD と Hi8 は画質的には、ほとんど同じでしたが、BD は HD だから全然違う。もっとも、

＊ NTSC とスカパーのSD

の差はないですね。なのでDVD録画したものを再録画する意味はほとんどない。ないんだけど、タイトルとかの情報が付くのは良いかな。そういう理由で録り直すことはあります。でも、スカパーのタイトルとかかなり手抜き。やる気ないのが良くわかります。そこ手を抜いてどうするのとも思うけど。

Gundam Seed とかはHDリマスターで画角が16:9 に。あれは、ちょっといまいちかも。線が太くなったりするのはちょっとね。ブラウン管じゃないので端が黒いのは気にならないから画角はそのままがいいな。でも、

＊ サンダーバード HD

は 16:9 で、かなり綺麗です。これはすごい。ただ、話を全部覚えているので見なおす気がしない。でも録画するんだけど。

というわけなので、ほとんど見ないまま録画しているものが多いね。そんなものだな。 DVDの録画をBD-Rに移すと1/5ぐらいになるので、そういうのもやってたりします。この録画になんの意味があるのかは良くわからんな。まぁ、でも、録画なんてそんなものでしょう。持ってることに意味があるみたいな感じか。

というわけで、実際に見ている番組は減ってきてる感じ。進撃の巨人とヤマト2199ぐらいしか見てないかも。あらら。

HDD だけに保存して「消えたら諦める」方式の人もいるようだけど、バックアップ抜きのHDDはちょっとね。それに「二重ではバックアップとは呼ばない」し。HDD を何十台も持っている人もいるらしい。それだと、

＊　BD-R を入れ替える

のと手間的に変わらない気がする。BD-R 安くなったが、HDDも安くなったので、今はビット単価は同じくらいかな。いや、まだ、ちょっとBD-Rの方が安いか。

そのうちにネット配信中心になるのだと思うけど、その時に、全部無駄になるぐらいのラインナップになれば良いんだけどね。今の感じだと、まだ、ちょっとなぁ。

学生が BD Box 買ったりするのは、豪華本を買うのと似ている感じ。持っているステータスが問題なんでしょう。僕は、そういうのはどうでも良いのだが、それが今のアニメを支えていると思うと、ちょっと微妙な感じ。

Monad

3年前のソフトウェア工学の授業で、Haskell の Monad をいじって敗れ去ったことがあって。いや、使い方はなんとなくわかる。

> getChar

とかすると、入力待ちになって c とか入れると c とか表示されるけど、

> let x = getChar

かすると、何も起きなくて、

> x

とかすると、その時点で入力待ちになって x を打つたびに違う物が返るとか。振る舞いは謎だし、構文も、

    getll = do 
        c <-getChar1
        if c=='\n' 
            then return []
            else do
                 l <- getll
                 return (c:l)

とか、ちょっと許してくださいという感じです。do ってなんだよ。do って。

getChar1 >>= \c -> return c

とかになると、いったいなんなのという感じ。まぁ、Haskell だからなぁ。

でも、今回は Category 特に Kleisli Category 勉強しまくったのでわかりました。

    Functor はデータ構造 F(a) は Fというデータ構造を作る
    F(f) は、fmap f のこと

で、Monad は Functor つまり、単なるデータ構造なわけ。

そして、Kleisli Category では、射は、

f : a -> F (a)

つまり、Functor である Monad を常に返す関数ってことね。return とかは単位元な Monad を返す。
で、>>== は、射の結合 g○f = μ(d)T(g)f を表す。なので、常に、

\c -> F ( f c )

というような形をしているのか。なるほど。

ただ、「だからなんなの?」ってのは、ちょっと残っていて、Kleisli Category は随伴関手とかもあるので、そっちに絡めて証明がなんたらとかやるんだろうなとは思いましたが、そこから先に突っ込むのは学部の授業では、ちょっとね。学生も Agda の証明には面食らっているようなので、その辺りをいじめると面白かったりするのだが。いや、それなりに楽しみました。

今朝もうっかり3時まで資料作ってましたが、さすがに前みたいに体調崩すということはなくなったみたい。ソフトウェア工学の授業も、やろうと思ったことはだいたいできたし。