Tuesday, 20 June 2017

土砂降り

今日は土砂降りで酷い目にあいました。

沖縄だと台風以外だと珍しいんだけどな。周回道路が川になってました。

まぁ、僕の移動がすんだら止むんですけどね。

Sunday, 18 June 2017

小澤の不確定性原理

昨日のOSCの飲み会でビール飲みまくっていたら「先生どこですか」的な呼び出しが研究室OBから。なんで沖縄戻ってきてるのと聞いたら、

* 科学基礎論学会/科学哲学/科学史
http://phsc.jp/conference.html

ぐ、懐かしすぎる。ぜんぜんアンテナに引っかかってませんでしたが、琉大でやってるのか! で、プログラムを見ると、

*  出口弘
*  小澤正直

ぐ、懐かしすぎる。東工大の吉田夏彦先生配下な人たちではないですか。

なんですが、さすがに三日連チャンで早起きは無理でした。遅刻しつつ、小澤さんの発表を聞くことができました。

*  σ(P)σ(Q) + ε(P)σ(Q) +ε(P)ε(Q) > hoge

だったかな。Hiesenberg のドイツ語の論文のアブストラクトとかが出てるのが吉田研っぽくって面白かったです。不確定性は indeterminancy から来ているのだけど、元のドイツ語は inaccuracy に相当する言葉だったらしい。それを英語の共著者が inderminancy とまずい訳をしたと。それにEinsteinが引っかかって、あんな議論になったかと思うと、まぁ、そんなことはないと思いますが。あの議論は量子力学の定義の精密化には訳なったわけだし。

というわけで、懐かしい面子に会えて良かったです。

Saturday, 17 June 2017

OSC Okinawa 2017

いつもの内輪の展示会ですね。そういえば、両親も業界の内輪の展示会では暇そうにしていたっけ。

展示はいつものなんですが、セミナーのネタがなくて。なので、

* 2月にいじっていた cmake の入門をやろう

と思ったわけですが、聴衆は自分の学生以外は三人でした。ま、まぁ、地味な話だからな。

cmake は、mavenとかgradleとかに近いかな。make が、わりと魔境になってしまっているので、

add_target ( target_name source1.c source2.c )

だけで、いい感じにやってくれるのは便利。まぁ、そこからいろいろやろうとすると、どうせ魔境なんだけど。

今回は自治会館。コンベンションセンタ、あるいは、OISTよりは、はるかに便利なところ。特に今日は雨だったので、沖縄では珍しい「駅から濡れずにいける会場」なのはうれしい。

Friday, 16 June 2017

GPU VDM

https://groups.oist.jp/external-events/event/gpu-accelerated-vdi-international-conference-2017-asia

いや、まぁ、琉大にはGPUクラスタないし。システム更新でも「GPUは毎年新しいのが出るから」で見送られたりしたので、いや、だったら、毎年なんか買えよ〜

と言うわけで、少し場違いなわけですが、まぁ、全然関係ないわけでもないしなぁ。今年の2月ぐらいはMac ProのGPUと格闘してたし。というわけで、プレゼンもすることに...

OISTなので、学生に車で送ってもらうわけですが、

8時と言ったのに、ぜんぜん来ない

間に合わないよ、で、かなに「すみません、送ってください」と頼んで階段を降りたら、下から登ってくるうちの学生が。「道が混んでて8時に出たのに30分かかりました」って、いや、そこ「8時に迎えに来て」って言ったのが「8時に迎えに出る」になっているところが、沖縄なんだよな。

まぁ、僕も、そんな感じで、いまだに遅刻魔なわけですが。

そこそこお金取られたので、ちょっと厳しい。学生の分がな。

そして、明日は OSC Okinawa です。そっちも、よろしく。一応、うちの学生のcmakeのセミナーもあります。というわけで、学生にはいろいろ迷惑かけてます。

Tuesday, 13 June 2017

Prolog とシーケント代数

去年も今頃授業でやっていたみたいです。関数型言語と同じで、

*  プログラム中での変数の論理的関係が理解しやすいように記述する

ための指針みたいなものだと思うと良いと思う。Prolog 使うとバグがなくなるとか、そんなことではなくてさ。

Prolog のbaseになっているシーケント代数の方もやるんですが、自然演繹と両方やるのはちょっとなぁ。まぁ、たいした量じゃないから両方かな。

でも別にシーケント代数やっていたら、Prolog 理解しやすくなるというわけでもなく。でも、Prolog で使う範囲だと推論規則が少なくて良いってのはあるかな。


Σ |- Q, Γ Σ' , Q |- Γ'
---------------------------------------------------------- (cut rule)
Σ , Σ ' |- Γ , Γ'

これだけだものな。

実際のProlog programmingだと多用(つうか濫用)するのは単一化の方なので、単一化を詳細にやらないのはどうなのとも思うのですが、やろうと思うと結構煩雑。

Clausal form への変換のプログラムも少し探してみたんですが、結構、複雑で、授業で紹介するにはどうなのかな。確か、Clockskin and Merish の教科書にも変換プログラム載っていたと思うんだけど、割と大変だった。

アセンブラのマニュアルとかは「ちょっと論理式かプログラムで書いてくれ」と思うことはあります。

Sunday, 11 June 2017

メッセージ

観てきました。原題が Arrival で、元の小説のタイトルは「あなたの人生の物語」ですね。

元の短篇が割と何も起きないタイプの話で地味。で、その通りに極めて地味に始まって「どーすんのこれ」だったのですが、ハリウッド的な拡大解釈が入っていて、そこそこ盛り上がりました。よろしかったです。

こういう、どうしようもなく人類が変わってしまう話って割と好きかも知れないな。正解するカドとか。

異世界言語の学習という視点ではどうなんだろう。深層学習使うシーンとか欲しかった気もするけど。一応、データの視覚化はやってたか。
アメリカ人的には、異星人がテレビとかラジオから英語勉強して、いきなり流暢な英語を話すとかを期待してるのかな。この手の言語習得は18-19世紀にはたくさんあったはずなので、そのあたりの蓄積があるはずなんだけどね。今はもう需要はないのか。

Friday, 9 June 2017

Emacs 25 の続き

というわけで、Emacs 25 と Agda 2.5.2 は、xterm/Terminal.app 上では完全に壊れてしまって。C-C C-L するたびに→が増殖する始末。気持ちはわかる。Emacs は昔の端末流に描画の最適化ってのをやるわけ。この位置だけ書き換えればよい的な。それを、Unicode 上でやると、どうしても位置がずれる。Terminal 上での描画幅は正確には知り得ないから。でも、行頭から順に描画すれば良いはず。なので、vim とか Emacs 22 では問題ない。壊したのがいるってことね。

しょうがないので、GUI版を試してみようと思うわけですが、どうinstallするのかが謎。結論的には Mac OS X では、Homebrew で、

  brew tap caskroom/cask

  brew cask install emacs


とすれば良いらしい。また、Emacs 入れ替えか。

Agda 側は

brew install agda

で良いらしいです。Haskell は brew install ghc らしい。

で、GUIで立ち上がるわけですが、

Font が小さい

いや、 2880x1778 で k14 使っている僕が言うんだから、かなり小さい。文字幅1mmないだろ。でも、Agda は動いているっぽい。

で、Emacs の文字の大きさを変える旅に出るわけです。

C-X C-+

で一時的に大きくなるのはすぐにわかりました。そして、Option Menyu に Set Default Font... がある。大きくして、Set Default Font か。

もちろん、再起動で元に戻る

あ、あーん? で、見つけたページがこれ。

Emacs:一発で文字サイズを変更する方法
http://lioon.net/emacs-change-font-size-quickly

つまり。「GUIから文字サイズを変える手段はない」ということらしい。.emacs か! そこで、

Set Default Font... を押すと Font Menu は出てる

というのには気がつきました。でも意味はないらしい。 Set Default Font... ってのは嘘ってことね。Font Menu は閉じないと再起動でも開く。なんだよ。

なんですが、このページに書いてある通りにしても動かない。Twitter でぐちっていたら、

.emacs があると、.emacs.d/init.el は読まないよ

って、ばっちりそれでした。mv ~/.emacs ~/.emcas.d/init.el か。

それで動いたんですが、翌朝になるとまた動かない。なんだよ〜

そのうち、

fontset-standard undefined

とか言われて、New window もできないように。

で、init.el の中で frame の font を指定してみたら、

VL Gothinc not found

とか言ってる。そうか、
    (set-fontset-font "fontset-standard"
              'ascii
              (font-spec :family "VL Gothic" :size 20) nil 'prepend)  ;; ここでサイズを指定
    (set-fontset-font "fontset-standard"
          'japanese-jisx0213.2004-1
          (font-spec :family "VL Gothic") nil 'prepend)

    (setq default-frame-alist
          (append (list 
                   '(font . "fontset-standard"))
                  default-frame-alist))

そのままコピペしたのがだめなんだな。VL Gothinc を monaco に変えたら動きました。あ〜 疲れた。

vim 版の Agda を試してみるべきだな。

Thursday, 8 June 2017

新しい Agda

Sets (集合を対象、写像を射とする圏)の Completeness としばらく格闘していたんですが... Compleness ってのは Limit があることで、Limit ってのは、与えられた関手で示された対象と射のグラフ上の可換関係を代表する対象みたいなものらしい。

直積とかは二つの要素の代表なんだけど、それがあれば、その二つの要素にできることは全部できるじゃないですか。そんな感じ。

なんだが、なかなかできなくて。結局、

record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ )
( smap : { i j : OC } → (f : I ) → sobj i → sobj j ) : Set c₂ where
field
snmap : ( i : OC ) → sobj i
sncommute : ( i j : OC ) → ( f : I ) → smap f ( snmap i ) ≡ snmap j
smap0 : { i j : OC } → (f : I ) → sobj i → sobj j
smap0 {i} {j} f x = smap f x


という record を作れば Limit の uniquness 以外は簡単に示せました。なのだが、uniquness が堅い。要するに、field 二つが等しければ、record 自体が等しいという合同性の問題らしい。

でも、ググってたら、にたようなのを Stack Over Flow で見つけました。(良くある)

https://stackoverflow.com/questions/37488098/equality-on-dependent-record-types

なのだが、こいつの例題が通らない。もしかして、Agda の version の問題か? 確かにちょっと古いんだよな。

で、update をかけたんですが... なんか、emacs も update。あ、てめーちょっと待て。

emacs 25 に上げられてしまったおかげで、xterm 上の色とかUTF8がずれまくる。vim は大丈夫なんだけど。くそ、unusable だ。しかも。Agda は 25 でないと動かない。

GUIでしか動かさないあほが手を入れて xterm 側を壊してるんだよな。

で、肝心の例題は Agda のupdate で通ったんですが、Sets completeness の方は通らず。くそ〜 どうも問題は Agda のrecord の合同性の扱いそのものにあるっぽい。僕のせいじゃないらしいです。

snat-cong : { c : Level } { I OC : Set c } { SObj : OC → Set c } { SMap : { i j : OC } → (f : I )→ SObj i → SObj j }
( s t : snat SObj SMap )
→ ( ( λ i → snmap s i ) ≡ ( λ i → snmap t i ) )
→ ( ( λ i j f → smap0 s f ( snmap s i ) ≡ snmap s j ) ≡ ( ( λ i j f → smap0 t f ( snmap t i ) ≡ snmap t j ) ) )
→ s ≡ t
snat-cong s t refl refl = refl

が通るはず。だけど、通らない。これはあきらめた方が良さそう。

なので、Agda 壊れちゃったので、ちょっと困ってます。vim で編集して emacs でチェックみたいな感じ。

Friday, 2 June 2017

iPhone 7

このあいだ、また、iPhone の画面を割ってしまって。ワイシャツのポケットがほつれれてでかいiPhoneだと落ちやすい。落ちどころが悪いとわれるらしいです。

で、5月で2年しばりが消えるので、ソフトバンクからは抜けようと思っていたのでちょうど良かったんですが、MNPとか面倒くさすぎる。かなのauの家族割に入るのがやすいらしいが...

まあ、格安SIM試してみるんじゃないの?

っことで、IIJ MIO に。めんどくさいけど、ソフトバンクにで電話して、うだうだ話してMNP予約番号をもらう。こんなのWebから一発発行でいいのに。IIJの方はWebから申込。で、iPhone 7 plus は Apple から買うと。はい終わり。

と思ったが、IIJの認証が通らない。免許証の写真を upload する方式なのだが、そもそも普段使いのクレカでは通らないとかわけわからん。で、サポートに電話したんですが、

コーノとコウノ

の違いだったらしい。いや、コーノで統一しているんだが、通らないあほシステムが若干あって、そこではコウノにするしかない。ローマ字側を kouno で強制するのとかも見たことがあります。もしかすると、免許証がそれだったかも。

免許証には漢字しかない

はずので、おかしな話ではあるな。

と言うわけで、ネックはIIJ側だったらしい。SIMがくれば、

iPhone を最新iOSでバックアップ
SIMをactivateして、新しいiPoneのOSを最新に
そこに restore

という手順で動いたみたいです。まぁ、しばらくいろいろあるだろうな。