圏と集合と位相

平成最後の5年くらいははまりまくっていたわけですが、今日は、学生が本をスキャンするための裁断機を使いに来ていて、なに勉強するのと聞いたら

　　圏論だと

なるほど。本を見ると、随伴関手と米田関手、つまりrepresentable functor まで。そうだよね。でも、それだと、

　　なんのために圏論を学ぶのか

は良くわからないかも。一方で、

　　圏論勉強するには集合と位相が...


とか言っている学生もいて。いや、違います。

　　圏論勉強するには集合も位相も不要

位相空間論は微分方程式の解の表現から「実数って一体何」というところに突っ込んでいったところがあって、そこから、

実数は自然数全体の集合から作られるというカントルのアイデアがあったんだけど、

　　選択公理で迷走

ところが、ボレルとか測度論やってる人たちが結局、選択公理に突入。そして、ゲーデル、コーエン先生による

　　選択公理の独立性

つまり、集合から実数の性質には証明では決定できない自由度があるってのが判明していまいます。

その辺で、結局、なにが起きたのかを

　　数学を構築する記号論理を、対象(命題)と射(推論)

から構築するという一種の反省から出てきたのが圏論だと思う。そして、それは、

　　型付きλ計算

と関係がある。なので、プログラミング言語を作る時には圏論が一つの指針になる。そういうことなんじゃないかなと。

型なしλ計算に否定をいれると矛盾するとかを圏論の言葉で明確に記述できるのはわかりやすい。プログラミングの基礎としての圏論を
学ぶなら，その辺が一つの目標かも。もう一つは随伴関手と表裏一体のモナドかな。

所詮は道具だと思うので、さっさと通り過ぎるべきだとも思いますけど Agda 結構面白くて時間かけてます。

元号が変わってもだいたい同じことやっているんじゃないかな〜

Ingress Dark XM event

白ぽを40万個埋めて、リンクの累積長さでメダルばもらえるってなものです．

　　5km, 50km, 250km

なんですが、普段でも2-3kmの(くそ)リンクは通すので50kmは普通に通るだとと思いますが、250km はなんかやらないとだめ。

沖縄だと離島リンクがあるので、350kmとか楽勝らしいです。なので、やりといえば終了的なところもある。陣営の競いもありますが、

　　あれは別次元

だからな。

自分的には白ぽ埋めは性に合ってる感じ。うちの陣営には umiatcher という「必ず白ぽを埋めに来る人」がいるわけですが、

　　浦西あたりとか宜野湾海浜公園とか

風邪からは回復したしCCCも一段落したので、そっち方へ。白ぽを埋めながら、そこから

　　適当にくそリンクを引く

だけで60kmまで楽勝。IngressのCFは「段取り」が重要なんですが、

　　あんまり考えずに，ふらふら歩く

人なので、そのあたりはあんまり。でも今回は海浜公園の20個以上あるのを埋めたらどこからか引くつもりでした。

なんとラグナガーデンの前から北谷までいく一日数本のバスの時間にあったので、そこから美浜までいって、

　　海浜公園までの4kmリンクをUltra link 使ってお代わりで

で、210km までいったようです。楽勝じゃん。この手のぼっち Nova は自分らしい気がする。

APには長さは関係ないから，普段はあまり気にしてないかな。でも、いつかは千キロリンクしてみたい。

CCC from Graph の続き

なんか朝起きて、少し頑張ったらできました。

証明が繋がることは繋がるのだが、同じ式でも穴開けると通ったり。

　　fmap で型の指定が足りないみたい

なので、fmap のmoduleの指定を増やしていく方向に。

　　Graph にCCCの構造を足す　　　　data Arrow
　　それから圏を作る　　　　　　　 data Chain
　　その圏からSetsへの関手を作る　 fmap

という手順だったんだけど、 Arrow と Chain の関数を分離できることに気がついたら一発でした。

ところが、その後、 「これも要らない」「あれも要らない」になってどんどん証明が小さく。


　 amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
　 amap {G} (arrow x) = smap G x
　 amap (○ a) _ = OneObj'
　 amap π ( x , _) = x
　 amap π'( _ , x) = x
　 amap ε ( f , x ) = f x
　 amap < f , g > x = (amap f x , amap g x)
　 amap (f *) x = λ y → amap f ( x , y )
　 fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
　 fmap {G} {a} (id a) = λ z → z
　 fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ]

　　　 distr : {a b c : Obj (DX G)}　{ f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
　　　 distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = adistr (distr {a} {b} {d} {f} {g} z ) x where
　　　　　adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
　　　　　　　( x : Arrow (graph G) d c ) → fmap ( next x (g ++ f) ) z　≡ fmap ( next x g ) (fmap f z )
　　　　　adistr eq x = cong ( λ k → amap x k ) eq
　　　 distr {a} {b} {b} {f} {id b} z =　refl

え、こんだけ? あんなに苦労してたのなんだったんだ。

要するに、CCCで拡張した部分は「一つの射」なので、その部分はグラフから圏を作る部分とは独立らしい。

今までダメだったのは、fmap で Arrow と Chainが一緒になっていて、Agda が混乱していたせいみたい。
fmapとamapで分離されていて、fmap の再帰の部分が amap の再帰から切り離されているのでうまくいくみたいです。

amap の部分を見ると、

　 amap (○ a) _ = OneObj'

とかで、「とにかく a から T への射は全部同じ」とか

　 amap π ( x , _) = x

で「積から積の要素への射は、これ一つ」になるのがわかりやすい。

やってみると「smallest equivalence relation between proofs」ってのがどういう意味かわかりました。
そんなもの。

module をまたいだ再帰はだめってのは鉄則みたいだな。

CCC gererated from Graph

いつもの Higher order categorical logic には半ページで「○とかπとかの射を足して、CCCになるように射の同値類を入れればできる」とか書いてある。

けど、ぜんぜんできないです。グラフは、

　　vertex (ノード、グラフの点)
　　edge (vertexの二つ組)

の集合。これは record で普通に書ける。これに、id と edge のつながりを表す data を入れてやると、

　data Chain { g : Graph } : ( a b : Graph.vertex g ) → Set where
　　　 id : ( a : Graph.vertex g ) → Chain a a
　　　 next : { a b c : Graph.vertex g } → (Graph.edge g b c ) → Chain {g} a b → Chain　a c

　_++_ : { G : Graph} {a b c : Graph.vertex G } (f : Chain {G} b c ) → (g : Chain {G} a b) → Chain {G} a c
　id _ ++ f = f
　(next x f) ++ g = next x ( f ++ g )

これでGraph から生成した圏のできあがり。簡単。これに、CCC の構造を足して、

　 data Objs {G : Graph } : Set where
　　　atom : (vertex G) → Objs
　　　⊤ : Objs
　　　_∧_ : Objs {G} → Objs {G} → Objs
　　　_<=_ : Objs {G} → Objs {G} → Objs

　 data Arrow {G : Graph } :　Objs {G} → Objs {G} → Set where
　　　arrow : {a b : vertex G} →　(edge G) a b → Arrow (atom a) (atom b)
　　　id : (a : Objs ) → Arrow a a
　　　○ : (a : Objs ) → Arrow a ⊤
　　　π : {a b : Objs } → Arrow ( a ∧ b ) a
　　　π' : {a b : Objs } → Arrow ( a ∧ b ) b
　　　ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
　　　<_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
　　　_* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )

この二つは vertex と edge に使えるから、

　 DX G = GraphtoCat ( record { vertex = Objs {graph G} ; edge = Arrow {graph G}} )

こんな感じで、CCCの構造が入った圏まではできました。おそらく Positive Logic とか言われるものなはずです。

あとは同値類を入れれば良いわけなんだが、なんか難しい。data CCCeq みたいなのを足すと結構組合せが爆発。

そこて、

　 DX G から Sets への関手を作れば、Sets は CCC だから証明終になるんじゃないか?

ってのを思いついた。確かに、自然数から剰余への関手を作れば同値類な部分圏が作れる。で、順調だったんですが、

　　fmap の定義の termination を Agda 理解してくれない
　　関手の分配則の証明が難しい

なので結局できてないです。

それでも、最後の二つ以外はだいたい通ったので、まったく外れというわけでもないみたい。

_* なしだと、Cartesian までいくけど、Closed でないってことになるらしいです。

あともう少しだな。_* だけ data でなんとかするってのが良さそうだが...

もう夏

バス一つ早く降りて ingress とかやると汗びっしょりで。着替えを置いてあるので着替えるのですが、

　　その間にお客様が〜

ちょっと待って〜

Black hole の中

Evernote にお絵描き機能があるでの、それで書いた図です。

一般相対論普通に時間対象なので入る線があるなら出る線もある。別に事象の地平線でおかしなことが起きるわけでもなく。

おかしなのは無限遠で平坦な空間な座標系から見るからなので、まあ，曲がって入るけど普通な感じです。

そこだけ真っ暗に見えるかというとどうかなぁ。まぁ、明るいってことはないか。

中の方がなんとなく広いっては面白い。

Deduction Theorem

昨日のOSCではまっていた奴です。CCC やってたはずなんだが、その直前に置いてあって、短い割に良くわからない。簡単そうだし。

えーと、

　　a を仮定して、b → c が証明できたなら、(a ∧ b) → c が a の仮定抜きで証明できる

ですね。当たり前っぽいけど、b → c のどこで仮定を使っているかがわからない。b → c の証明は推論の積み重ねなので、それを解析する感じ。

Intorduction to Higher order Categorical Logic には Positive logic の場合の証明が載っていて、五つの場合があるとか書いてある。

その場合分けにそって、

　　a を仮定した b → c の証明 φ(x) つまり、φ : a → (b → c)

を分解していく感じらしい。で、φ(x) から (a ∧ b) → c の証明を返す関数 kx∈a を作れば良いんですが、ぜんぜんできなくて。

　　kx∈a : {a b c : Obj A } → ( x : Hom A ⊤ a ) → ( φ {a} x z ) → Hom A (a ∧ b) c

と

　　data　φ　{a : Obj A } ( x : Hom A ⊤ a ) : Set ( c₁　⊔　c₂ )

かと思ったんですが、まったくできず... そうだよね。これだと、分解していく式がない。、b → c　の形をした式みたいなのでないと。

結果的には、

　　data　φ　{a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁　⊔　c₂ )

　　kx∈a : {a b c : Obj A } → ( x : Hom A ⊤ a ) → {z : Hom A b c } → ( y　: φ {a} x z ) → Hom A (a ∧ b) c

でできました。

要するに、場合分けの関数を書く時には、

　 data 関数　入力 : 出力 → Set

という風に書けば良かったらしい。なるほど。

これで、ほぼ教科書の式通りに証明できました。

　　data　φ　{a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁　⊔　c₂ ) where
　　　 i : {b c : Obj A} {k : Hom A b c } → φ x k
　　　 ii : φ x {⊤} {a} x
　　　 iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x < f , g >
　　　 iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
　　　 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }　(ψ : φ x f )　→ φ x ( f * )

　　kx∈a : {a b c : Obj A } → ( x : Hom A ⊤ a ) → {z : Hom A b c } → ( y　: φ {a} x z ) → Hom A (a ∧ b) c
　　kx∈a x {k} i = k ・ π'
　　kx∈a x ii = π
　　kx∈a x (iii ψ χ ) = < kx∈a x ψ　, kx∈a x χ　>
　　kx∈a x (iv ψ χ ) = kx∈a x ψ　・ < π , kx∈a x χ　>
　　kx∈a x (v ψ ) = ( kx∈a x ψ　・ α ) *

超短い。

教科書通りにできるのは、書いてる先生の頭が Agda だからだろうと思います。というか、Agda が圏論に合わせて作られているわけだな。

Open source conference Okinawa 2019

シス管と一緒に出展してます。

なんか、ラズパイ配ってるブースがあるな。もしかして初代ラズパイ?

ヘタな就活するよりも業界の情報が取れるような気もする... なので学生には積極的に参加して欲しいかな。

琉大の方では GCP, Google Cloud Platform の勉強会もやってます。Kubernetes Engine も面白ろそう。

OS9 の展示もやってます。実機は間に合わなかったが。

https://okipug.connpass.com

CCC の続き

いろいろさぼりながら。

　(1) Hom A a 1 ≈ {*}
　(2) Hom A c (a × b) ≈ (Hom A c a ) × ( Hom A c b )
　(3) Hom A a (c ^ b) ≈ Hom A (a × b) c

ですが、1対1を表す(行って帰ってくる写像二つとその二つが元に戻ることを示す二つの等式)だけでは足りなくて、

　　写像の合同性を表す cong x ≈ y → f x ≈ f y

と、あと二つの naturality ( 可換性 commutativity )が必要でした。たぶん、1-3 全部、natural iso なんでしょう。

cong が必要なのはちょっと不思議。等号が集合としての等しさ(要するに項として等しい)場合は自動的に成立するけど、

　　関係として等号を定義する時には自明でない

らしい。この辺の厳密さが何に影響するかは知らないんですが、仮定に入れてやれば良い。

二つの naturality は結構複雑。(2)の b を b から c への写像 f : b → c あるいは、f : Hom A b c を使って変更するのが
一対一を表す写像と可換というだけなんだけど。(2) は二つの射の組になるのがわかりづらかったかな。
(3) は対象が構造((a × b) c)を持っているので，その中を操作する操作が必要なので複雑になるみたいです。

いや、こんなの難しいうちに入らないか。

次は、λ a → a × b と λ a → a ^ b の組が随伴関手になっているのを示すみたいです。

で、CCC に新しい対象(新しい仮定、あるいは公理)を足すとどうなるかという Polynominal categoriies 、それから、

　　Functional completeness

かな。なんか名前がかっこいい。型なしλ計算がSKIで表されるのがFunctional completenessの一種とか書いてあるんだが、あんまりピンと来ないな。

プログラミング3

なんかつまらない名前な授業になるらしいんですが、中身は同じ。プログラミング3という名前が面白いかと言うと、

　　なんか、第三段階レンズマン

みたいだよね?! カッコ良くない?

今年は専門の授業の開講が少ないらしく、人が多い。ちゃんとシラバスに、

　　自分のやりたいプログラミングをやる授業

と書いてあるのに「やりたいことがない」のはなんでだ。そういう意味では若干醒めてるのが良い世代なのかも。

最初はWeb sevice作ってもらうのですが、最初の一週間の勝率は10%くらいか。手を付けてないグループも。

実は割と、一人プロジェクト率も高い授業です。今年はどうかな。

CCC

圏論の方ですね。TL/1 少し飽きた。Cartesian Closed Category 。デカルトも自分の名前がこんなに使われるとは思ってなかったに違いない。

　１ : Obj A
　_*_ : Obj A → Obj A → Obj A
　_^_ : Obj A → Obj A → Obj A

の三つの要素(True と積と Apply かな) があって、

　(1) Hom A a 1 ≅ {*}
　(2) Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
　(3) Hom A a (c ^ b) ≅ Hom A (a × b) c

というもので、わかりやすいとえばわかりやすい。λ計算と、推論システムの両方のモデルになってます。

(1) は True は何からでも推論できるし、それ唯一しかない。(2)は c → a かつ c → a なら a ∧ b　で、逆に c → a ∧ b なら、 c → a かつ c → a 。最後は、

　　a →　c <= b と a ∧ b → c が同じ

というもの。curry 化にも見えるかな。引数二つと a -> b -> c は同じ。

なんだけど、集合で扱おうとするとうまくいかなくて。要素一つの圏と、圏の積を考えた方が良い。圏論はそういうところあって、なんでもかんでも圏でやった方が良いらしい。そういえば、

　　部分圏を定義するには自己関手が簡単

ってのもあった。部分集合とか面倒くさい。

で、これを等式ベースに定義する方法があって、それとこれとが同値なのを示すというのがお題です。

　 １ : Obj A
　 ○ : (a : Obj A ) → Hom A a １
　 _∧_ : Obj A → Obj A → Obj A
　 <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)
　 π : {a b : Obj A } → Hom A (a ∧ b) a
　 π' : {a b : Obj A } → Hom A (a ∧ b) b
　 _<=_ : (a b : Obj A ) → Obj A
　 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b)
　 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a

そもそも登場する演算子が多い。さらに等式が...

　 e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ]
　 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o < f , g > ] ≈ f ]
　 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o < f , g > ] ≈ g ]
　 e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ < A [ π o h ] , A [ π' o h ] > ≈ h ]
　 e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ]
　 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ]

ちょっと量多いが、Hom → 等式はできたし、反対もなんとかなりそう。(e1 は圏の公理)

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

Netfelix

風邪で寝てた時に暇だったので。ただ、

　　風邪で根性が尽きているので見る気が起きない

というバグが。ウルトラマンを少し見ましたが、ガキに使わせると危ないと思うんだけど。

字幕を自由に制御できるのは良い。

色んな似たものが出てるみたいだけど、

　　どれとっても同じ物が観れる

ってのが望ましいです。考えるの面倒くさい。アクトビラってまだあるんだな。

今週末は Open source conference

Open source conference Okinawa 2019
4月20日(土) 10:00-17:00（展示は16:00まで）

沖縄県市町村自治会館(OSC受付:4F)(ゆいレール 旭橋駅から直結通路で徒歩約5分)
　 https://www.ospn.jp/osc2019-okinawa/

それまでに体力が回復すると良いんですけどね。割とぼろぼろです。

徐々に平常運転かな。授業が少ないのは助かる。

Bluray の入れ物

48枚入りを割と愛用してきたんですが、

　　DVDと違って不織布の痕が付く

と文句をつけた人がいるらしく。いや別に水平に積み上げるわけでもないし。そんなトラブル今までないけど。

そんなものよりはメディアそのもののトラブルの方が多いと思う。

「細かくしました」って、10倍も違わんだろと思うんですけどね。

おそらくは売る方の都合ではないかと想像します。

体温計

今日も一日寝てました。来週は大丈夫そうだ。

熱とお腹を壊したのから始まったわけですが、その時にお医者さんで使った体温計が妙に早い。

　　20秒

らしい。今回は結構お世話になったのでマツキヨで探して買ってみました。

ボタン押す手間が増えてるけど良い感じ。電池も交換できるのか。

今まで使っていたのは1分。電池交換不可。ずいぶん使ってるんだけど電池が切れる様子はない。

耳で計るのとかもあるみたいね。

fmemopen

最近追加された C の API らしい。メモリの領域を fgetc とかfprintfとかでアクセスできるようにしてくれるすぐれものです。

OS9のVRBFでも使いました。

TL/1 の機能の低さはすごくて、配列は256byteまで、変数はbyteのみなので、

　　Self compiler どうやって書くんだよ

ってわけなんですが、mem($80,0) = $ff とかはできる。でも、それは辛すぎる。でも

　　 write 文は充実してる

まぁ、Pascal 由来なんですけどね。 なので、

　　メモリを read/write できれば write(2:"while",ascii(27))とかで予約語定義できる

なるほど?! TL/1 は辞書を線形サーチするし、コード生成は1 passだから、putしていけばよい。

offsetを後で埋めるとかもあるけど、seek できれば良い．これならできそうな気がする。

こういうデータ構造抜きでいろいろ作っていくのは、前にやった coinduction に似てるな。

まだ、もう少し風邪で自粛するつもりなので、もしかすると書いちゃうかも知れないです．

TL/1 続き

風邪でお休みプロジェクトですが、だいぶ良くなった気がする。で、平常運転してこじらせたので
今回はもう少しお休みモードで。

　　OS9:tl1 -c tl1/test/t1.tl1
　　OS9:t1　　　　　　
　　Do 1
　　2
　　3
　　4
　　5
　　6
　　7
　　8
　　9
　　10

　　% os9/os9mod os9/level1/t1
　　Offset : 0x0000
　　Header for : t1
　　Module size: $2B6　#694
　　Module CRC : $56548C (Good)
　　Hdr parity : $9D
　　Exec. off　: $020B　#523
　　Data size　: $0003　#3
　　Edition　　: $0D　#13
　　Ty/La At/Rv: $11 $80
　　Prog mod, 6809 Obj, re-ent, R/O

楽勝楽勝。メモリ上でmodule作るので runtime や開始アドレスのoffset計算を完全に試行錯誤で作りました。

CRC計算はOS9のsystem callあるし。でも、初期値が0xffffffで、最後にbit反転するとか言われないとわからないよ。
当時もそれが neck だったはず。

あれだな、白いジグソーパズルで全部の組合せを試す奴みたいなものですね。

ついでに for 文が実行時stackを使っているのも治したので for文途中で return もできるはずです。

あとは self compiler だが、実在するかどうか怪しい気がしてきた。1 byte の変数と配列しかなくて、
他には MEM(HI,LO) ぐらいしかないから...

TL/1 os9 module generation

まだ熱は引かないんですが、動けないほどでもないので授業のイントロは片付けてきました。

後期のコンパイラの授業はTL/1のセルフコンパイラやろうとか思っていたんですが、どうも「ない」らしい。

なので寝込んでいる間に、OS9 の module 出力でもやろうかなと。

　　モジュールヘッダを作成
　　ライブラリをコード部分にコピー
　　生成コードを PIC に
　　CRCを計算
　　ファイルに書き出す

簡単じゃん。まだ動いてないですが。

大きなプログラムだとリンカーが問題になるんだけど、

　　OS9のlink module system callとか使えないかな?

OS9 level 2 のメモリ空間をまたいで使えたりすると面白い。

進撃の巨人

一日寝てました。 37.7度くらいだと動けちゃうのがな。

進撃の巨人の2/3 part 1を見てないのを思い出した。part 2 は4/29 からですか。

どちらかというと馬鹿ばっかりな話なので、そんなに好きではないんだけど、

立体動装置かっこいいし。

お腹痛いのは治ったのだが

なんか咳が...　こんどは歯が... どうも細菌の巣が移動している感じだな。良くあることではあるんですが。

少し熱もあったのでおとなしくしてました。

QNAP は43xを2台で運用してますが、firm update とか Perl のinstall とか溜まってたので、少し片付けました。

録画も面倒くさくなってきてるが整理終わり。

スカパー

アンテナトラブルで一回線減らしたんですが、まぁ、快適に動いてます。困ってるのが、

　　映画は固定日本語字幕

か吹き替えなこと。WOWOWも。いや、テレビには字幕と音声切替付いてるんですが、

　　絶対に使わない
　　英語字幕は死んでもやらない

らしいです。日本語字幕邪魔なんだよな。特に日本語nativeでない人には致命的に邪魔らしい。

どっちかっていうと欲しいのは英語字幕なんだが...

なので、外国人は全員スカパーやめちゃったんじゃないかな。Netflixあるし。つうよりは。やめちゃった結果がこれか。

今はBS11あるからアニメもスカパーである必然性ないしな。

安易に subscription に移行しているのを快くは思ってないんですが、あんまり抵抗してもなぁ。

まぁ、今の録画環境は便利なんですけどね。Netflix でそれを全部放棄してやり直しのがちょっと。

coinduction

論理、特に演繹系は、命題と命題を結ぶ矢印である推論からなる圏になるわけですが、

　　矢印を全部反対にすると双対圏が得られる

ってのあります。

数学的帰納法を induction というわけだけど、その矢印を全部逆にしたのが coinduction 。逆帰納法かな?

AIM で Automaton の構成を見せたら、いや、有限性抜きでできるんだよと論文送ってもらったんですが、それが、 coinduction でした。

その辺、あんまり近寄りたくなかったんだっけどな。逆数学とか。まぁ、圏論触ったから仕方ないか。

数学的帰納法は、p(0) を示して、p(n+1) を p(n) から示すみたいな感じ。実際には証明するのはp(n)だから、

　　p(0) = ?　
　　p(s(n)) = ? p(n)

と言う感じで、data (場合分けされたデータ構造)を分解しながら処理していく感じ。

そうすれば、問題は一段小さくなるから、小さい部分では証明はできてるから再帰で。

coinduction だと、徐々に record で表される直積で作られたデータ構造を構築していく感じ。終わりは自分で終わりという。

オートマトンの言語(文字列の部分集合)だと、

　　　　record　Lang (i : Size)　: Set　where
　　　　　 coinductive
　　　　　 field
　　　　　　　ν : Bool
　　　　　　　δ : ∀{j : Size< i} → A → Lang j

こんな感じ。文字列なのに List とかない。Size は Agda に coinduction の停止性を教えるためのものらしい。A は仮定された文字の集合。

文字を与えると、δ (derivative 微分か?) 新しい少し小さい Lang j が作られて、もう終わりにしたい時には ν で判定する感じ。

　　　　_∋_ : ∀{i} → Lang i → List i A → Bool
　　　　l ∋ [] = ν l
　　　　l ∋ ( a ∷ as ) = δ l a ∋ as

単なるListではなく長さを持つ List を自分で作らないといけないらしい。 δ l a 自体が状態だと思えば、状態遷移そのもの。

確かに、Automaton と相性が良い。逆に、 List i A → Bool が与えられたら、

　　　　trie : ∀{i}　(f : List i A → Bool) → Lang i
　　　　ν (trie f) = f []
　　　　δ (trie f) a = trie (λ as → f (a ∷ as))

という風に作れば良いらしい。f の引数がどんどん貯まっていく感じだな。実際には f は有限状態だから、部分評価できると考えれば良い。

　　　 trie f = record { ν = f [] ; δ = λ a → trie (λ as → f (a ∷ as)) }

を、こんな風にかけるのか。いろいろあるな。

で、状態を明示したければ、

　　record DA (S : Set) : Set where
　　　　field ν : (s : S) → Bool
　　　　　　　δ : (s : S)(a : A) → S

　　lang : ∀{i} {S} (da : DA S) (s : S) → Lang i
　　Lang.ν (lang da s) = DA.ν da s
　　Lang.δ (lang da s) a = lang da (DA.δ da s a)

こんな風にするらしい。Size はどこにいった? 初期状態はDAそのものなのか。NDA はこれから考えます。

むらなが吟 at Bar Teada

2009年にも Bar Teada でライブやったみたい。10年ぶり。木曜日は、少しお客さん少なかったけど、まぁ、今のBar Teadaっぽいか。

おっさんのブルースって良いよね! 福島にも寄ってきたらしく、風評害の話とかも。前回の時よりは政治の話は少なかったかな。

テネシーワルツとか自作の曲とか。なんとなく、70年代っぽい感じもするのは、そういう年代だからですね。

バスの時間

97の終バスが早くなったのは去年なんですが、今年は98の終バスも早くなってしまいました．21:30

ついでに、330の終バスも早くなってるな。22:00

困ったなぁ。本数減らしても終バスは遅くして欲しかった。前はもう少し遅かったんだけど。

まぁ、あんまり人が乗ってないってのはあるんだけど。

さっさと帰れって人もいるけど、そういう職業ばかりじゃないんだよな。

東京でも地下鉄は本数少なくても良いから24時間にして欲しいところ。

α6000

NEX5 も別にまだ動いていたんですけどね。液晶ボロボロだし。れでも父のレンズが使えるのが欲しいかなと思って。

iPhoneの補助に使うならズームなコンデジが便利で、実際、WX350が壊れるまではそうしてました。

壊れたので買い換えようかなと思っていたんだが、同じもの買うのもなぁ。

池袋なのでカメラ屋さん見てたらα6000の中古で2万9千円というのが。

だったけど、割とボロボロで。で、いくらと聞いたら2万5千円だったので、それならいいかなと。

今はα6400とかいうのがあるらしく。10万円も出せば買えます。でも、そこまではなぁ。α6000もまだ売ってるらしい。

α6000は5年前のカメラだけど十分かな。NEX5よりはだいぶ明るいはずです。ファインダー付いてるし。ファインダー無しだと昼間はつらい。

最近は iPhone のカメラが結構良いのでNEX5のズームレンズとかだとあんまり差がないかも。特定の構図ならば。

と言っても40mm固定が使いやすいわけでもないので、やっぱり趣味の問題でしょう。ピント合わせがそこそこつらい。

iPhone に無線で写真を送れるのですが、そこそこ速いけど、UIが最低なのはソニーっぽい。

M6のボディが50万円で売られていたりいろいろ面白かったです。

学年歴

昔は、ical のを作っていたんですけどね。本部の方が作ってくれるようになったのでさぼっていたんですが、

　　なくなった

まぁ、良くある話だ。なので、昔の ical を生成する script を引っ張り出してきて直してみました。

あぁ、でも本部の学年歴、table だな。だから、こういうの値段ケチるとだめだって言ってるでしょ。

前は、ちゃんと css base で抜き出しやすかったんだけどな。

いや、もしかすると、うちの学生が作っていたりして...

前期の授業

去年度の後期は「一つ新しい授業が追加される」だったので、結構、きつかったんですが、今年は、

　　どうも一つ少ない

らしい。それとは関係なく前後期に一つずつプログラム読み会を入れてるので、もしかすると特別講義にするかも知れません。

前期は修士の授業で、

　　QEMU

を読もうかと思ってます。要するに VM だな。世間様の流行からは10年くらい遅れているかも。

なんか他にあるって聞いたら、grep とか Emacs とか。

　　Emacs?! あの undump でもめてて、その後、音沙汰ないあれ?

まぁ、面白いかな。いまだに入力がどういう過程でテキストに反映されるのか謎。テキストはB-Treeみたいな感じだし。

と思ったら、tmux の方らしい。あ、そっちの方か。通信は pseudo tty 経由で、おそらく自前で curses の制御を見てる感じなはず。

そっちは、そんなに時間かからないだろうな。

後期は言語処理系なはずですが、例のRubyのCに変換するVMとか面白いかも。

元号は平成の時にはテレビ見てた気がするけど、今回は特に気にしてませんでした。令嬢的な感じが良いですね。