母とIngress

いや、まぁ、母はIngressはしないわけですが...

朝、起きて、お散歩。
お昼の後に、お散歩。
夕食前に、お散歩。

らしいです。おかげで、要町から椎名町、立教までを制圧できてうれしいです。一回、35位に入りました。

一人で出ると、いろいろ怪しい買い物をしてしまうらしい。ジャンクなものが家にたくさん... 今川焼きとか、苺とか、大福とか...

まぁ、元気で出歩けるうちに自由にお散歩してください。

しばらく東京です

今回は特に何があるわけでもないので、のんびりしているはずです。少し、Ingress Mission でもやりたいところ。

呼び出されなければ4/7まで東京の予定。

思ったより寒くなかったが、夜は寒いのかな?

飲み会などは適当に呼び出してください。

カレーパーティ準備中

12月にやったばっかりですが... 年二回目標です。

今年は11時に学生4人に来てもらって。わりと順調です。やっぱり経験値上がってるからな。いや、学生が優秀だからか。

Google Spread Sheet に、材料とかスケジュールとかがまとめてあるんですが、

　　やっぱり、どんどん大きくなっていく

まぁ、記録ないよりは良いんだけど... レシピはあるんだけど、5倍量とかだと、比率も変わるので。

表を作るなら、Schema も作るべきで、コメントとかを表に入れてはいけないんだろうな。複数の表が同じコラムで制御されてしまうのも残念な感じ。

僕は、HTML直書き(あるいはTeX)で表を作るのが好きだけど、HTMLのは、ちょっと見づらいかな。

あなたの人生の物語

テッドチャンですね。なんか映画化されて「メッセージ」というタイトルで5月に公開されるそうです。

なのだが、

　　　　どんな話だったっけ?

さっぱり思い出せないです。なので、本棚から引っ張り出すわけですが、奥様に聞くと「それはこの段の奥」で、そこにある。どうも、ちゃんと著者名順に並べているらしい。えらい。

だいたい読んだ本は、ネットに書くのだけど、blog にない。そうか、ネットニュースの時代に読んだんだな。それを見てみる限り、非因果的な言語ってのは面白いけど使いこなせてないみたいなことしか書いてない。

で、読み直す気になったんですが、短篇なので瞬時に読めるんですが、

やってきた宇宙人とテレビ経由で話すだけの超地味な話

でした。こんなの良く映画化する気になったな。

しかも、そこで使っている手法って、スペイン人が最初にアメリカで現地人に会った時に使うような感じで..

まぁ、地球人は電波とかで自分たちの言語や情報を垂れ流しまくっているので、向こうは全部わかってるってのがありそうな感じ。

今だったら、とりあえず、DNNに流して見るくらいはするんじゃないかな。問題は「何を」だったりしますが。DNNは何を理解したかは教えてくれないし。でも、どこを見ればよいかぐらいは見つけくれるんじゃなかろうか。

まぁ、宇宙船でやってきてテレビ電話で通信するあたりで、人類との共通点はたくさんあるのでコミュニケーションに問題がでるとは考えづらいが...

もっとも、自分の赤ん坊でさえ何を要求しているのかわからなかったりするし、犬や猫とのコミュニケーションもできてないからなぁ。

昔のテレビの電波だったら解読は容易だろうけど、今のデジタル方式のはどうだろう? まして暗号化されていたら。

解読されやすくするコードとかの話も70年代に「宇宙と交信する」とかが流行っていた時にあったな。それも、向こうが交信する気があればの話だけど。

そんなわけでメッセージがどんなできたかは楽しみです。

http://www.ie.u-ryukyu.ac.jp/~kono/sf/194.html

Agda の圏論の証明

まぁ、やってるのが圏論だってのが特殊ではあるんですけどね。

　極めてパズル的

帰納法とかほとんど出てこない。なので、

　証明の穴に適当に推論を当てはめる

ということになりがち。そして、それで、結構通る。それで終わってしまうのが普通。

もともと圏論が General Abstract Nonsense だからってのもあるんだろうけど。

Monad も面白いんですが、一生懸命証明したものが、

　メタ計算も関数の結合法則に従う

というだけだと、ちょっとさびしいんじゃないかなぁ。

でも、一方で、

　プログラムはちゃんと型的に穴が埋まっていれば動くんじゃないの?

とも思います。

数学や物理の理論を理解するには、数式や論理式の裏にある

　モデル

を理解することだと思う。圏論はモデルと論理式が一体になっている特殊な例なのかな。

　視覚化できるモデルとかたいしたことない

とも思うのですが、視覚化には「気づき」みたいなところがあるからな。

久しぶりにAgda

なんか、沖縄とっても寒い〜

学生の方が一段落したので、いつものように Agda いじってるんですが。今回のお題は否定。有限の射を持つ圏、つまり、たんなるグラフがうまくできなくて、

＊　存在しない射に対する結合則とかは、矛盾⊥ から導くのが良いんじゃないか?

ってことで、否定について調べてたんですが、

　 Nope : (m n : ℕ) → Set
　 Nope (suc _) zero = ⊥
　 Nope _ _ = ⊤

　 nope : ∀ m n → m ≡ n → Nope m n
　 nope zero ._ refl = _
　 nope (suc m) ._ refl = _

　 peano : ∀ n → suc n ≡ zero → ⊥
　 peano _ p = nope _ _ p

　 http://stackoverflow.com/questions/22580842/non-trivial-negation-in-agda

とかあって、結構面白い。

なんですが、

　 even : ℕ -> Set
　 even zero = ⊤
　 even (suc zero) = ⊥
　 even (suc (suc n)) = even n

　 div : (n : ℕ) -> even n -> ℕ
　 div zero p = zero
　 div (suc (suc n)) p = suc (div n p)
　 div (suc zero) ()

とかいうのもあって。()ってなんだ?

　 ¬_ : Set → Set
　 ¬ A = A → ⊥

　 data Dec (P : Set) : Set where
　 yes : P → Dec P
　 no : ¬ P → Dec P

　 EvenDecidable : Set
　 EvenDecidable = ∀ n → Dec (even n)

　 isEven : EvenDecidable
　 isEven zero = yes _
　 isEven (suc zero) = no (λ ())
　 isEven (suc (suc n)) = isEven n

　 http://stackoverflow.com/questions/18347542/agda-how-does-one-obtain-a-value-of-a-dependent-type

とかやるらしく。起き得ない入力の組合せみたいなものらしい。Agdaが、これは起きないと理解してくれれば使えるらしいです。

つまり、A x B x C -> D みたいな関数で、A/B/Cのすべての入力について関数を定義する必要はないらしい。そういえば、data で規定された範囲しかみたいなみたいなことはやっていたな。どうせ、矛盾を取れる部分は規定された範囲外なんだから、実は除外できるんじゃないか?

今までは存在しない部分は Maybe で nothing とかやっていたんですが、それがいけなかったかも。で、演算定義とか結合則とから、いろいろ抜いていくと、

あれ? なんかできるじゃん

どうも、Maybe とかで record の中に入れ込んだので、Agdaが理解してくれなかったっぽい。

というわけで、要素2の圏を記述はきれいになりました。

なのだが、その後の Limit から Equalizer の証明には、はまりました。でも、定義を二重に入れてしまって、それの同一性が取れなかっただけで、定義を一部外に出したらできた。

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

結構、苦労していたのができて、ちょっとうれしいです。

　 http://seeker-s-eye.blogspot.jp/2017/01/agda.html