Wednesday, 15 November 2017

コインランドリー


なんか、最近、派手で綺麗なコインランドリーが流行りらしく。うちの近所にもできてました。

で、少し冷かしに行ってみたところ、

  河野先生ですよね

え? なんと、うちの卒業生が経営者らしく...

大学の勉強役に立った? と聞きましたが、普通にWebとかを使えただけで、直接には役に立ってないみたいです。

研究室にも、初期の頃のOBとか来てたな。ちょっと沖縄に戻ってくるのは早いんじゃない? とか思うけど、まぁ、それも良いか。

Monday, 13 November 2017

かばん壊れた


Twitter と同じこと書いてると言われるでしょうが、こっちにも書きます。年一回は壊れてる気がするよ。

バスから降りたら「バスっ」とかいう音とともにかばんが落下。もはや、いつものことなので驚きはしないんですが。

既に、付属の肩紐は使い物にならず実家の別なかばんの肩紐に交換済。なので、少し金具が元の違う。で、壊れたのは、肩紐側の金具かぁ。油さしておくべきだったかも。削れちゃうんだよね。

だいたい、革の方もリングになっているので、そこにOリングを通すのが良い。それが一番もつ。

  最初から、Oリングにしておけよ!

と思います。デザイン的にもそっちの方が良いと思うし。

なんだけど、Oリングあったかな。4Fの実験室にいけばあるんじゃないか? メイクマンいけばあるのは知ってるのだが... なのだが、山田さんが「ここになはない。前も買った」というつれない返事。予算で買う時には余計に買うんだよ。秋葉原で電子部品買う時には必ず余計に買っていた。すごすごと部屋に戻ったのですが、

  もう一度探したら、ロッカー置いてあったポーチの中にあった

旅行用のポーチでカミソリとか綿棒とか入っている奴。旅行には、Oリング必須だったのか。そうだろうなぁ。イギリスに行った時に既に、3.4kgのダイナブックをかばんで持ち歩いていたからな。

だた、キーホルダー用みたいな小さいやつなので、あまり保ちそうにないな。メイクマンにいくしかないか。少し余計に買うことにしよう。いや、既に買ってある可能性も高いな。

Sunday, 12 November 2017

論理式と方向

いつもの Agda の話題ですが、論理式には方向がない 例えば、

 a = b

と書いてあっても、a が出力とか b が入力とかない。一方で、関数(λ式)には方向がある

λ x → y

では x が入力で、y が出力になります。

Agda だと、数学的構造は record や data で書きます。record は積で and でつながったもの、data は排他的論理和で case 文の集合みたいな感じ。

で、Agda の library とかを見ると、record Hoge と record IsHoge とかが組で出てる。良くわからなかったんだけど、どうも、

record Hoge ( input : InputType ) where
field
output : OutputType
isHoge : IsHoge input output

record IsHoge ( input : InputType ) (output : OutpoutType ) where
field
property : ppro inupt output

みたいに使うらしい。filed は名前と型、つまり、名前の付いた変数とか論理式が来るわけですが、record の引数は入力、field には出力、つまり、その数学的構造で存在が主張されるものを列挙します。例えば、有界な実数の集合には最大値にになる極限が存在して上界というとか、そんなの。

その入力と出力は数学的構造の性質(公理)が要求されるわけですが、それらは論理式なので方向性はない。それを IsHoge にわけて書くという方式らしい。

こうすると、

lemma1 : (input : InputType) → Hoge input → ...
lemma1 input hoge = ...

とすると、Hoge i での IsHoge の性質が使えるようになる。つまり、

∀ input → ∃ output such that IsHoge input output

というわけ。Hoge の存在を示す時には、

lemma2 : (input : InputType ) → Hoge input
lemma2 input = record { output = ... ; isHoge = record { property = ... } }

という風にするらしい。なるほど。

で、今までにやった圏論(クライスリ圏とかLimitとか)を、これにそって書き直したんですが...

  仮定が余計とか、仮定が足りないとか

が若干でて、少しはまりました。一通り書き直して、だいぶ、見通しが良くなったみたい。普遍問題では入力は圏A,Bと関手Uで、それがUに対するLimitの存在につながるとか、ちょっとあやふやだったところが理解できたみたい。形式大事だな。

IsHoge のみで書くことも可能で、初期の頃のはそういう風に書いていて、必要なものは module input に書くとかしてたみたい。楽なんだけど、

Hoge → Fuga

みたいにならないで、

(x y z : ...) IsHoge x y z ... → IsFuga x w q

とかで、 x y z とかの仮定にいろいろ余計なものが入ったり、うっかり書きそびれたりしていたようです。

Programming 的には Hoge が interface で、IsHoge が実装だと言えないこともないかな。

Thursday, 9 November 2017

Twitter の文字数

日本語 vs English だと

 焼肉 vs steak

っていう例を良く出すんですが、倍くらい違うみたいです。

Agda とかソースコードとか数式とかも twitter に書くのだが、すぐ足りなくなる...

なので、言語ではなくて文字でカウントして欲しいんだが。どういうカウントなんだろう。


Tweets 106K Following 5,989 Followers 5,907 Likes 94.4K

ぐらいなみたいだな。この間、6000 まで増やしたのに、また減ってる。思ったより Like 多いな。

Wednesday, 8 November 2017

目医者さん

「良くなってますね」

ということなので、まだ、少し残ってるようですが、薬は飲まなくて良くなったみたいです。

Retina で少し眼に負担をかけすぎたってのもあるかな。

生活習慣変えなければ、どうせ再発だとも思うけど... 血圧は低めになってきますが。

  薬のせいもあるが、怪しい血圧計を新調した

のが大きいかな。

Monday, 6 November 2017

東京 short visit

既に帰ってきました。 母も歳なので、たまに長くいるよりも短くして、頻繁に行った方が良いかと思って。

でも、週末だけってのは「酒飲んで終わってしまう」なぁ...

 - * - * - * -

ついでに Agda も少しいじってました。初期の頃にやった equalizer と product から limit を作るという課題。Sets の Limit をやって、やっぱり少しおかしいことに気が付きました。

少し自力でやってみたがうまくいかず、Categories for Working Mathematician を見直すわけですが、

  お前、前に読んだ時に何を読んでいたんだ?!

ってくらいに違うことが書いてあって。まぁ、でも、大筋は合ってたんだけど。一部の等式を、仮定を強力にして安易な証明ですませたらしい。だめだな。いや、おかしいとは思ったんだけど。Sets Completeness の時に使えなくて気がついた。

元の証明に Product 二つ足して東京にいる間にできたみたいです。

あと何やるのかは、まぁ、やっても良いものはたくさんあるが、Kan Extension とか、Cartesian Closed Category の一連とか。ZFC やってみるのも良いかな。

 - * - * - * -

なんか、xterm が勝手に focus 外れるんだよな。もう使ってる人はほとんどいないと思われるので誰にも聞けないところがつらい。

Sunday, 5 November 2017

Blade Runner 2049

見てきました。なのでネタバレだいじょうぶになりました。

なんか時間の関係で4DXになりましたが、あんまり意味ないかな。4DXではまれる映画ってどんなものなんだろう?

年末にはスターウォーズも控えているのか。

こういう拡大再生産は、歌舞伎とか紅白歌合戦っぽいかな。