打ち上げ花火

なんとなく見てきたのですが、

　　こんなに子供っぽいのでは、ちょっと残念すぎる

「君の名は」を期待してはいけないってな知識はあったんですがね。

この手の繰り返しものには「繰り返しを通して成長する」ってのがあると名作になるのだが... それがまったくないと尻切れとんぼで終わるしかないってことですか。

女の子とがかわいければ良いんだよと開き直るのがせいぜいかな。男の子の妄想の世界でしたで終わってるわけだし。

P.K.Dick の Eye in the sky 的な脱出ものにすれば良かったのか?

Ingress Mission

順調に片付けていて、Misshon medal black までは来ました。

沖縄だと車前提なミッションが多くて。那覇まで出ればそれなりにはあるんですが。

池袋のはやポチだけで192あるそうであす。楽です。

夏の大三角は駅周辺30だったかな。今は「かえるさんの洗濯バサミが見た風景」をやってます。帰るまでには終わるでしょう。

このミッションは、緑がよってたかって削除したポータルを記念して作られたらしく、「全部 No で」といわれたので、だいたいそうしてます。

いつものお見舞い

母の妹のいる施設に母を連れてお見舞いに行ってきました。これをすると東京に来た用事の半分ぐらいが片付いた気がする。

まぁ、ボケは進んでいるようですが、仕方ないかな。でも顔色は良く食欲もあるようでした。車で送ってもらったので楽でした。半分寝てた。

　　 最果ての銀河船団
　　 http://amzn.asia/54pYPhx

は、施設にいる老人に人がやってきて星の見える丘に連れ出して「あれが、これから出発する船団です」ってやるんだよな。

超準解析

学部時代に存在を氏って、斉藤先生の本とか買っていたんですが、

　　肝腎のモデルの話がない

で、ロビンソン先生の元が読めるわけなので、そちらを読むわけですが、超フィルターとか出てきて良くわからなかった。

今回は、

　　https://math.berkeley.edu/~jhicks/links/SOTS/koneill030514.pdf

を読んでみました。何回か集合論勉強したので超フィルターだいぶましになってる。

　　If A, B ∈ F,then A∩B ∈ F
　　If A ∈ F and A⊆B⊆I,then B ∈ F

フィルタ自体は割と簡単。ある集合Iの部分集合の集まりFで、その要素の共通部分もF含まれていて、ある要素を含む集合も含まれているというもの。ブール代数のイデアルの双対みたいなものらしい。

超フィルターFってのは、Iの部分集合Aを取ると、AかAの補集合がFに含まれるもの。これを使ってIの部分集合を二つにわけて、いろんなモデルを構築するわけね。簡単な例は、あるIの要素aを撮って、それを含む集合とそうでない集合にわける。そうすると超フィルターになりまう。a がA入ってなければ、Aの補集合にはaは入っているから。これを Principal filter というらしい。

超実数は、実数が整数の無限列なのと同様に、実数の無限列として作ります。
四則演算は、実数列それぞれで行えばよい。
問題は、こいつに順序が入るかどうか。それぞれの列の実数を比較して、1と0を割り振ると、

　　1と0の無限列ができる

で、1が多い方が勝ちにするわけだけど、特定の列で決まってしまうと具合が悪い。1と0を逆転させると結果は逆転して欲しい。つまり、1,0の無限集合の部分の集合が non principal な超フィルターFに含まれるかどうかで勝ち負けを決めると良いらしい。

で、問題は、non principal な超フィルターFが存在するかどうか。non principla ってのは、

　　どんなIの要素aを取ってきても、それを含まないFの要素の集合がある

ってことね。フィルターの要素の共通部分はフィルターに含まれるので、

　　有限個のIの要素を取り除いた集合はすべてFに含まれる

ということ。有限集合はぜんぶ含まれない。問題は無限集合で無限個の要素を欠いたものだな。これを全部含むと超フィルターではなくなってしまう。そこで、

　　有限個のIの要素を取り除いた集合をすべて並べて、その共通集合を取っていく

そうしてできたものをFとすると。選択公理があるなら、これが可能。で、選択公理を仮定しないとないとしても良いらしい。

要は整数の部分集合の集まりであるnon principal 超フィルターを仮定すると、超実数に全順序が入るということらしい。

ここまで来るとあとは簡単で、

　　どんな小さい正の実数よりも小さい正の超実数を無限小とする
ある超実数は、ある実数と無限小分だけしか違わない

無限小だけの差しかないを、 ≃ とすると、これが同値類になり、実閉体で成り立つものは、= をこれで置き換えるだいたい成り立つというわけですね。

デルタ関数とかも普通に関数として定義できるらしい。便利。

　　http://planetmath.org/constructionofdiracdeltafunction

でも、超実数に対する直観は、やっぱりモデルの直観だと思うので、εδとかよりわかりやすいかどうかは。

超フィルターが存在するかどうかは選択公理に依存するので、そんなものあるのという疑問は正しい。なので、ちょっとやっっかいな感じ。でも、

　　超実数に全順序がある

ということ自体はわかりやすいかな。これを認めれば良いかもしれないですね。

ハクソーリッジ

見てきました。東京では午前中の上映しかなくて、なかなか見に行く根性が。日曜日のロサ会館だがガラ空きでした。

浦添ようどれの戦いですね。普天間から嘉数高台の激戦の直後なはずです。高台からはえ割と平坦で、そこから長く崖があるので、そこですね。 何故、米軍が裏からはさまなかったってのは議論があるらしいです。

銃を持たずに衛星兵と戦うわけですが、そこまでの話が面白いかな。扱いに困る廻りと、プライドのために戦う人という構図。彼女がとってもアメリカンでいい感じ。

戦争シーンは、もう少しという感じ。日本兵の歩兵戦略をもっと描いて欲しかったかも。まぁ、あれがハリウッドの期待しているものなんでしょう3ど。ようどれのてっぺん自体は広くないので、ちょっと違うんじゃないかな。そこにこだわる監督はもういないですかね。

嘉数高台にはトーチカ跡がありますが、ようどれはお墓が復元されただけで、戦闘の跡はあまりない。でも、艦砲射撃で地形は変わってしまってます。

今では眺めの良い Ingress 激戦区か。いや、ようど3れあたりは、割と平和で白ポがたまにあるかな。自分の守備範囲という認識ではあるんですが。

fj 同窓会

今回は新宿ルミネの中のベトナムアリス。良く、土曜のお昼に予約取れたな。

電子メールとネットニュースは初期のバケツリレーメカニズムでの実装はほぼ同じで、電子メールを繋げるとネットニュースも付いてくるという感じでした。

企業と学校、日本語と英語が入り混じっていて、独特な雰囲気だったかな。今のFacebookと、それほど差がない気もする。入れ物が変わっても中身は変わらないもの。

Know how が貯まらないってのは、ネットニュースでも2chでもSNSでも同じか。Wikiとかにしがみついている人たちも。Stackover flow も本質的な差はない気がする。

ということは、まだ、改良の予知はあるんでしょうね。

それと今回の集まりとは、まぁ、あまり関係なく。緩い昼ビールな食事会でした。また、呼んでください。

母との日々

実家で母とのんびり過ごしています。ヘルパーさんが来てくれる日と、デイサービスの日と交互に。

たくさん連れ出してくれるヘルパーさんとか、家事をいろいろやってくれるヘルパーさんとかいろいろいて面白い。

母もぼけは進んでいるようですが、にこやかに過ごしていただければうれしいかな。4人姉妹も、だいぶお年を召してきたわけですが、4人それぞれだな。

Ingressで洗濯物は多いのですが、洗濯機廻しておくと、ちゃんと干しておいてくれます。たたむのは、そろそろめんどくさいらしい。

今日は研究室の東京にいる卒業生たちと食事です。行ってきます。

東京のIngress

西8池袋は割と青いです。立教が夏休みだから、そういう影響もあるだろうな。

要町までにバス通りに8ポがたくさん。千早フラワー公園にはFF後が放置されていたり。そんなわけなので、補給には苦労しない感じ。というか、X8が300すぐに貯まって、あまり使えないんですが。まだ、本気で緑の所を荒らしてないからなんだけど。

ミッションはたくさんありますね。池袋西口ぶらり旅ってのを片付けたので、次は、

　　夏の大三角

という30連をやろうかと。池袋周辺なはずです。まぁ、のんびりと。元気な人は一日で終わらせるんだろうけど。

Ingress、ミッションの検索性の悪さはなんとかならんのかなぁ。

東京は暑い

そんなわけでしばらく東京にいます。(-8/30)

実家の一階のクーラーは壊れているっぽいな。二階が外よりも暑くて、

　　冷えるまで外で飲んでるか

で飲みに出て帰ってきたらクーラーは切られてました。まぁ、少しはましになっていた...

今回は、東京のIngressミッションを少し追求したい。

免許更新

もう、5年たったか。相変わらずのペーパードライバーですが、今後、運転する機会のないことを祈るだけだな。嫌いってわけでもないが、廻りが危ない。

で、バスで南風原までいくわけですが、宜野湾から1時間、大学まで2時間ってなところですね。

なんだが、

　　病気で気を失いましたか

とかいう問診票が。そういえば手術したし、麻酔中は意識なかったな、と思ったが、'もちろん、「いいえ」

だが、

　　日付が読めない

とか言う文句が。

　　くだらん意味ない書類か書かせて、さらに文句言うのか? 誰も見ないだろ!

日付が読めないぐらいで文句をつける方がおかしい。いや、下手だが読めるし。サインが読めないというぐらいおかしいだろ。

　　いや、サインが読めないって文句は海外でもあるらしい

んだけど。日本語のサインが良いという人もいるけど、そういうこともある。

といういわけで、免許更新はできたようです。次は更新するかどうかは謎です。鬼が笑うか。

X.v6 ARM を OS X のclangで作る

Linux 上のGCC ARM Cross compiler で作るのは普通にあって、それで作ったのを大学院の授業では読んでみたわけですが...

　　clang で作れるんじゃないか?

で、clang -arch arm で ARM をはいてくれるわけですが、OS X だからな。elf ではなく mach-o 。まぁ、いろいろいろ問題はあるが...

　　entry.S

が通らない。なんか命令がないとか言ってくる。


　　1:
　　　 CMP r1, r2
　　　 STLTMIA r1!, {r3}
　　　 BLT 1b

とか書いてあるんですが、しばらくわからなかったんだど、LT って、Predication か。アセンブラの命令に条件をつけられるあれですね。じゃぁ、

　　　 STMIALT r1!, {r3}

だろ? LTは後ろに付くはずだけど。これで通りました。なんだよ。

なんだが、問題は Linker か。開始アドレスを指定したり、segment の位置を指定したりしないといけないんだが、OS X の ld でどうやればいいのかがわからん。

できないってことはないんじゃないかなぁ。

まぁ、clang を elf をはくように作り直しても良いはずなんですが、mach-o でやっても面白いかな。

GCC版なCbCもあるんだが、最新版に合わせるのは大変なんだよな。

gcc なcross compilerはあるので、それでclangを作っても良いんだけど。

いろいろ方法があるだけに悩ましい。

Mendeley

論文管理サービスですね。いろいろ比較して、Papers.app を使っているわけですが...

　　お前、琉大だろ、メンバになれば容量増やしてやる

みたいなメールが来てたので、再度トライ。ばっちりパスワードなくしていたので再発行から。昔よりはだいぶ良いかも。昔のMendeley って妙に複雑でさっぱりわからなくって。

で、BibTex の読み込みってのがある。D論書いた時がLaTeXの出た翌年だったりするので、BibTeX使いです。なのだが、

　　さっぱり読み込まない

一つだけなら読み込む。じゃぁと、BibTeXのentoryを論文毎に切り分ける Perl script を書いて一括登録〜としたら、やっぱり蹴られる。やっぱり使えんな〜

でも、Desktop app があるな。で、そっちを使ってみると、

　　ちゃんと読み込めました

Webサービス側で手抜きしただけか。誰も使ってないんだろうな。読み込めたけど、それだけだな。

この手のものは、すぐにネット上に上げさせるけど、量的に無理なんだよな。2.3GBなのでたいしたことはないんですが。TB1万円台になっていて、それくらい出しても良いけど、

　　サービス毎に1万円出すのはバカすぎる

一方で、自サーバを使えば1万円で4TBぐらいのサーバを作れる。それが現状だよね。なので、やっぱり Papers かな。

Mendeley は学生との参考文献共有に向いているとかあったんだけど、どうなんだろう?

　　https://www.mendeley.com/

agda-vim

いろいろ動かなかった agda-vim ですが、なんとか動きました。

　　https://github.com/derekelkins/agda-vim

~/.vim/bundle の下に置けって書いてあるけど、それをするためには、pathogen ってのを使わないといけなかったらしい。

　　https://gist.github.com/romainl/9970697

まぁ、いろいろね。Get Pathoben と Configure Pathogen をやるらしい。

で、動いたんですが、

　　,l で reload すると、一旦、Terminal画面にvimから戻って、agdaのSkipping ... が大量にでる


これはちょっとなぁ。Emacs だと、別バッファ上でやるので、元のバッファは残ってる。消えるのはちょっとなぁ。

学生は「動画を見る限り使えるようですが」とか言ってましたが、動画でも同じ状況でした。作った人は「でっかいターミナル一つ」な人のようで、それだと気にならないんだろうな。

ちょっと、ソースを見ると、

　　def RestartAgda():
　　　global agda
　　　agda = subprocess.Popen(["agda", "--interaction"], bufsize = 1, stdin = subprocess.PIPE, stdout = subprocess.PIPE, universal_newlines = True)

ってことで、Python 2.7で実行しているらしい。　この辺でダサいことになっているんだろうな。プロセスの扱いは Emacs は最初から頑張っていた。

vim でもterminal modeとか作っている人がいるようですが...

自分で手直しするかどうかは気分次第だな。subprocess.Popen を追求するのは気が重いです。

まぁ、でも、その reload を我慢すれば、まぁ、使えます。Emacs の vipper と agda の相性の悪さと戦うよりは良いかも。