温泉浸かってます
意外に暖かい。東京の方が寒かった
バオバブ
https://baobab-trees.com
の社長さんが、やってきていろいろ話てくれました。ビジネス関係の発表って聞きづらい...
まぁ、部分部分は面白かったかも
他の人は「そんなに話は飛んでない」とかいってたので、そうだったのかも
「Gemini の日本語部分を担当してて納期厳しい。アノテーション甘く見るな」とかが印象に残りました
Saturday, 10 January 2026
Friday, 9 January 2026
プロシン1日目
なんか、正規表現の話が最初に。まあ、いろいろあるなとは思うが、微妙に興味を維持しにくい
次は Zen 大学のオートマトンの授業の構想の話。僕も、オートマトンの授業を持ってたが
Agdaの証明で、オートマトンの授業やる
っていう話で、まぁ、うまいくところもいかないところも。学生がどの程度まで理解するかは、あんまり気にしてなかった
なので、オートマトンの授業を
学生の興味を切らさずにおこなう
ってのは重要なテーマだと思う。自分の授業とは、まったく違う方向でってことね
正規表現とRegex は別ってのは、Regexはプログラミング言語で実装されるような具体的で高速な実装という意味
その実装を課題として出すのは確かに面白いかも
次は Zen 大学のオートマトンの授業の構想の話。僕も、オートマトンの授業を持ってたが
Agdaの証明で、オートマトンの授業やる
っていう話で、まぁ、うまいくところもいかないところも。学生がどの程度まで理解するかは、あんまり気にしてなかった
なので、オートマトンの授業を
学生の興味を切らさずにおこなう
ってのは重要なテーマだと思う。自分の授業とは、まったく違う方向でってことね
正規表現とRegex は別ってのは、Regexはプログラミング言語で実装されるような具体的で高速な実装という意味
その実装を課題として出すのは確かに面白いかも
Thursday, 8 January 2026
Wednesday, 7 January 2026
Tuesday, 6 January 2026
圏論と 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 をやるかと考え中
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 をやるかと考え中
Monday, 5 January 2026
Sunday, 4 January 2026
パプリカ
今敏監督のですが、20周年らしく
観てなかったらしい。夢の中で大行進する話ですが、台詞が大変そうだった
話は怒涛で進むわけなんだが、終わり方はよくわからず。まぁ、勝ったみたいな話
途中の刑事の学生時代の8mm映画の話が、なんとなくいい感じに終わる
筒井康隆の声の出演? え〜どこ?
まぁ、パプリカが可愛いので許す的なアニメ映画だったかも
あけまして、おめでとうございます。blog は、さぼってました
観てなかったらしい。夢の中で大行進する話ですが、台詞が大変そうだった
話は怒涛で進むわけなんだが、終わり方はよくわからず。まぁ、勝ったみたいな話
途中の刑事の学生時代の8mm映画の話が、なんとなくいい感じに終わる
筒井康隆の声の出演? え〜どこ?
まぁ、パプリカが可愛いので許す的なアニメ映画だったかも
あけまして、おめでとうございます。blog は、さぼってました
Subscribe to:
Comments (Atom)