プロシン2日目

温泉浸かってます

意外に暖かい。東京の方が寒かった

バオバブ
https://baobab-trees.com

の社長さんが、やってきていろいろ話てくれました。ビジネス関係の発表って聞きづらい...

まぁ、部分部分は面白かったかも

他の人は「そんなに話は飛んでない」とかいってたので、そうだったのかも

「Gemini の日本語部分を担当してて納期厳しい。アノテーション甘く見るな」とかが印象に残りました

プロシン1日目

なんか、正規表現の話が最初に。まあ、いろいろあるなとは思うが、微妙に興味を維持しにくい

次は Zen 大学のオートマトンの授業の構想の話。僕も、オートマトンの授業を持ってたが

　Agdaの証明で、オートマトンの授業やる

っていう話で、まぁ、うまいくところもいかないところも。学生がどの程度まで理解するかは、あんまり気にしてなかった

なので、オートマトンの授業を

　学生の興味を切らさずにおこなう

ってのは重要なテーマだと思う。自分の授業とは、まったく違う方向でってことね

正規表現とRegex は別ってのは、Regexはプログラミング言語で実装されるような具体的で高速な実装という意味

その実装を課題として出すのは確かに面白いかも

ITビル

池袋西口の丸井のあとは、IT Tower になってました

まぁ、池袋っぽい名前ではあるかもね

まだ、開いてないのね

しばらく東京

今日明日は東京で、その後は、那須のプロシンにいってきます

東京はさすがに寒いな

普天間のテレビ

なんか、液晶テレビの偏光膜がびろびろに

ずーっと放置か

まぁ、見れるからいいのかな

圏論と Agda の続き

Sheaf の方は、6月にできそうとか思ってたんだが、Γ と L の随伴関手を示すんだが、Γはできたんだが、L が...

https://github.com/shinji-kono/category-exercise-in-agda/blob/41031f5d52ff5563888262ae6619aa4ba582fda4/src/Sheaf.agda

それでも、かなり、うまってきて、随伴関手の自然変換まで行き着いたんだが

　Agda が止まらなくなってきて

どうも、implict variableを書かないと止まらなくなるらしく

そこで、少し飽きたので、別な方を始めました

＊ 圏とグラフの随伴関手

ね。CCCでやるんだが、難し過ぎるので圏とグラフで。二週間くらい戦ったら書けた
https://github.com/shinji-kono/category-exercise-in-agda/blob/41031f5d52ff5563888262ae6619aa4ba582fda4/src/CCCGraph.agda

で次は

＊ Polymonimal 圏と、関数完全性

なんだが、こっちは、なんかだめ。

1) Polymonimal 圏ってのは、x : 1 → a を付け加えた CCC で、演繹定理で作れる
2) だが、その時に x の違いを無視する同値類で考える
3) すると関数完全性が成立する
4) それは実は coklisli 圏で、Polinominal 圏は、それに iso

いや、なんかPolymonimal 圏っぽい CCC は作れる。coklisli圏も。だが、関数完全性がだめ

同値類がうまく作れない。coklisli 圏で関数完全性を記述する方法がわからない

https://github.com/shinji-kono/category-exercise-in-agda/blob/41031f5d52ff5563888262ae6619aa4ba582fda4/src/Polynominal.agda

ちっとあきらめかな

また Sheaf をやるかと考え中

パルコのパプリカ

なんか、大きなポスターが

一応、録画は持ってました。Perfect Blue と千年女優もあるらしい

録画がないのは妄想代理人かな。8mmではもってたはずだが

パプリカ

今敏監督のですが、20周年らしく

観てなかったらしい。夢の中で大行進する話ですが、台詞が大変そうだった

話は怒涛で進むわけなんだが、終わり方はよくわからず。まぁ、勝ったみたいな話

途中の刑事の学生時代の8mm映画の話が、なんとなくいい感じに終わる

筒井康隆の声の出演? え〜どこ?

まぁ、パプリカが可愛いので許す的なアニメ映画だったかも

あけまして、おめでとうございます。blog は、さぼってました