饒波公民館 Nova

いつもの Ingress。 饒波はのはと読むらしく。要するに、ダジャレ作戦です。

車じゃないから、作戦への貢献度はゼロなんだけど、本数増やすくらいは。

南部のど真ん中からだからなぁ。リンク切りは大変だったと思いますよ。琉大は少しは整形したけど...

那覇の飲み会のあと、帰ってきてから、琉大病院までいって、そこから32本稼ぎました。琉大掃除してくれた人たちありがとうございます。

工学部側からは、微妙に入らなかったけど、入れば40まではいったかな。

久しぶりのNovaで、楽しかったです。この手のは、他の位置ゲーではできないからな。

ついでに、Recurs 後で Lv14 まで来ました。

12/7には crossfaction な首里城アートをやるらしく、絶賛、参加者募集中です。

iPhone Short Cut

これがなぁ。AppleScript らしく。まぁ、仕方ないのだが、

　　application 毎にできることが違う

やりたいのは自動的に々写真を撮るだけなんですが...

どうも設定すると、AppleScript をネットから読めるらしい。でも、AppleScript の言語的なダメさ加減はな..

　　Dictonary 死ね!

的な。JavaScrpipt 使える説あったのに。

Camera を起動して、写真を撮るのは Preview しないを選択するとできた。なのだが、

　　今どんな写真を撮ったかが見れない

ぐ。Quick look だと、抜けるのを待ってしまう。それは

　　自動的とは言わない

ですね。Quick look して何秒後かに抜けるみたいなのが欲しいんですが。

うーん、自分で書くか? なんかある?

安安

安易な焼肉チェーン店です。新しく東口にできたとかで、学生が行くと言うので付き合いました。

この手の焼肉だと、石嶺のキムチ屋を愛用していたのだが、なくなって既に2年。満福が近いのだが、最近は行ってないな〜　でも、

　　焼肉いくのに理由はいらないし。

新しくできたからと言って、特にキャンペーンがあるわけでもなく。

でも、七輪で焼くのは良いな。肉はまぁ、そんなもの。

最近はメニューが中華タブレット。TECって書いてある。ってことは、

　　コンセントがある

これが便利だな。

Agda の不等号の推論

最近いじってた Data.Fin とか < とか ≤ とか良くでてきてて、substとか<-transで適当に片付けていたんですが、

某所から降ってきたのが、結構、使いまくり。

　Agdaの特徴である推論使えないの?

だよなあ。で、

lemma1 : suc (suc m + n * suc m) ≤ suc (k * suc m) → suc (suc m + suc n * suc m ) ≤ suc (suc k * suc m)
lemma1 (s≤s lt) = s≤s ( s≤s (subst (λ x → x ) (
　 begin
　　 suc m + n * suc m ≤ k * suc m
　 ≡⟨⟩
　　 suc n * suc m　　 ≤ k * suc m
　 ≡⟨ ? ⟩
　　 m + suc n * suc m ≤ m + k * suc m
　 ∎ ) lt ))　where open ≡-Reasoning

とかやってみる。でも、これはだめ。suc n < suc m と n < m は等しくないから。

Bool で Setoid すればできるんじゃないかと思って agda-stdlib 見てたら、

　　agda-stdlib/src/Data/Nat/Properties.agda
　　-- A module for reasoning about the _≤_ and _<_ relations
　　module ≤-Reasoning where
　　　open import Relation.Binary.Reasoning.Base.Triple

なんだ、そこかぁ。

　　 lemma : {n k m : ℕ } → n < k　→ suc (k * suc m) > suc m + n * suc m
　　 lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
　　 lemma {suc n} {suc k} {m} lt = begin
　　　　　　　　 suc (suc m + suc n * suc m)
　　　　　　　≡⟨⟩
　　　　　　　　 suc ( suc (suc n) * suc m)
　　　　　　　≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
　　　　　　　　 suc (suc k * suc m)
　　　　　　　∎　 where open ≤-Reasoning

みたいに使うらしい。使い方は stdlib を grep して見つけました。

傘

超雨男なので、傘は必須。いつも、持ち歩いてます。「こんな天気に傘ですか?」とかいってる人が、僕と一緒だと1時間後に顔色変わるとか。

さこ飯のさこさんもそうらしい。農連市場の土砂降りはすごかった。

この間、大学にお客さんが来てる時に傘なくしてしまって探しまくっていたんですが...

いつものお昼の佐真下のコートドールで見つけました。この傘割と調子良いのでうれしい。

バス停でなくした時には見つからなかったので残念だった。

年末の予定

12/27-1/13 東京で、1/9-12 はプロシンなはずです。年末、東京にいくのは久しぶりかも。

もっとも実家に行っても特にやることはないのだが。それは、家事やらない人のセリフか。

この時期だと飲み屋さんもやってないので、実家に閉じこもってたり。

Finite Set

今週末は、Agda でそんなのやってました。首里で Ingress で遊ぼうと思っていたのに。結婚式の帰りは公栄あたりを廻ってました。

NFAの受理を調べるのに、有限集合から検索ってのをやるので、書いたんですが、Agda だと

　　Data.Fin

だけでやるものかも。これにdata とか、いろんな集合(Agdaでは関数の型だ)を対応させるわけ。

Automaton だけでも、Finite Set の和集合、'積集合、Q → Bool と一通りでてきてしまう。個数はそれぞれ、足し算、掛け算、exp 2 になります。

その結果が、Data.Fin つまり個数制限のある自然数に写像されるわけだ。小学生でもわかる内容なんですが...

これが思ったより、はまる。Data.Fin との写像には「ちゃんと範囲に収まっている」というのを示す論理式があって、それを持ち歩くことに。

それに対する ISO つまり、

　　record ISO (A B : Set) : Set where
　　　 field
　　　　　 A←B : B → A
　　　　　 B←A : A → B
　　　　　 iso← : (q : A) → A←B ( B←A q ) ≡ q
　　　　　 iso→ : (f : B) → B←A ( A←B f ) ≡ f

を確認することに。超絶面倒くさいです。

和集合とか仮定してすませてたんですが、まぁ、そういうわけにもいかないかと思って始めたんですが、結構難しい。

和集合は足し算なので、Data.Finの加減算と格闘する羽目に。ほとんどできたんですが、そこで、

　　要素を一つ付け加える操作を∨で定義して
　　それをn回繰り返して、A ∨ Fin n を作り
　　Fin n に B を対応させる

というのを思いついた。ISOがあれば同じ Finite Set だからな。これで、加減算とはほぼおさらばできた。素晴らしい。

和集合ができれば、積も同じように、∨をn回繰り返せば良い。

次は、Q → Bool ですが、List Bool でも良い。これも空列から始めて、一つ増えると、∨で倍に。倍々なので exp 2 。わかりやすい。

なんですが、Q → Bool と List Bool のISOが難しかった。プログラマって、

　　要求される入力よりも広い範囲の入力を受け付ける関数

を書くよね。でも、これが ISO の範囲をはずれて調べる羽目に。当然、そこではISOは成立しない。

結局、範囲を正確に受けとる関数に変換する羽目に。しかも、行きと帰りと両方。

これで、Q → Bool までできた。

そこで終わりにすれば良かったんですが、部分集合欲しいなと思って。m 個の Finite Set から n < m 個のFinite Set を作るわけですが...

個々の要素を Q と Q に付いている番号が n よりも小さい条件を一緒に持ち歩けばよい。結果的には、

　　data fin-less { n m : ℕ } { A : Set } (n<m : n < m ) (fa : FiniteSet A {m}) : Set where
　　　elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less n<m fa

というdataを持ち歩けば良いわけですが、A←B で生成した条件を、iso← 側で検算することになる。そこその大きさの項を検算する羽目に。

そこで、積やListと同じでzeroから増やす方法もやってみたのですが、複雑はほぼ変わらない。まぁ、どの方法でもできそうなところまではいったのだが。

結局、この data に対する合同条件

　　get-elm : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → fin-less n<m fa → A
　　get-elm (elm1 a _ ) = a

　　get-< : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → (f : fin-less n<m fa ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n
　　get-< (elm1 _ b ) = b

　　fin-less-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
　　　 → (x y : fin-less n<m fa ) → get-elm {n} {m} {n<m} {A} {fa} x ≡ get-elm {n} {m} {n<m} {A} {fa} y → get-< x ≅　get-< y → x ≡ y
　　fin-less-cong n<m fa (elm1 elm x) (elm1 elm x) refl HE.refl = refl

を書いて頑張って検算する方法でできた。

ここでわかったのは、この fin-less の data は、集合のLimitiを作るものと同じ。Data.Fin の構造を保つ部分集合を作るということは、結局は、'

　　圏のLimit、つまり、随伴関手

を作ることと同じことらしい。どうりで難しいわけだよ。

結果的には割と短い証明でできたので良しと言うことにしよう。


http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/automaton/file/tip/agda/finiteSet.agda

結婚式

吉浜さん、おめでとうございます。

この年になると結婚式に呼ばれるのは普通はないんだけど。まぁ、あの沖縄流の三百人呼ぶやつですね。

入場、かじゃで風から花束贈呈と言う、伝統芸なのは、もはや珍しいかも。

超上品な加奈よ〜が観れたのが良かったです。

料理は中華系ですが、なんか、でかいフォアグラが... 新郎の趣味だな、きっと。

グランドキャッスルは日航からヒルトンで、ダブルツリーブランドになったわけですが、レストランのレベルは維持できてる感じかな。

今時は、外資系の方が人を大切にしてるかも。

成美おばさん

東京に行くたんびに顔出すようにしていたんですが、昨日、息を引き取ったようです。四人姉妹の三女。

子供の頃からかわいがってもらったからなぁ。キャラクター物が好きな人でした。

次女の母のクモ膜下出血の時にも、いろいろ助けてもらいました。母と一緒にいてくれるだけで助かった。

施設にいたのも長かったような短かったような。

8月に会ったのが最後だったけど、穏やかな晩年だったかな。いや、そんなことはないのだろうけど、そういうことしよう。

今年の年末はそんなわけなので、東京にいるようにします。

引き潮のとき

先日亡くなった眉村卓のおそらく最大の著作です。随分前に司政官シリーズをまとめたものと消滅の光輪を読んだので読みたいとは思ってました。

が、ハードカバー五冊。もっとも当時2,500円x5だったので買っておくべきだった... 今は古書で一冊一万円近い。でも、文庫でるんじゃないか説。

宜野湾図書館にあるのをWebから検索してもらっていたので、Ingress で寄ったので借りてきました。

　　倉庫にあるけど、5分で持ってこられる

お役所っぽくない。素晴らしい。5冊は重いので取りあえず2冊。図書カードも作ってもらいました。コピーは一部までとか書いてある。そういえばそんなことになっていたっけか。

400 x 5 ページかぁ。ひたすらモノローグが続くのは、80年代当時、SFマガジンの立ち読みで知ってはいるんですが...

司政官はロボット官僚を使って植民星を管理するみたいな話なんですけど、どちらかと言えば、

　　司政官の黄金期の話を読みたかった

気もする。もっとも。人類史上、成功した官僚制度とか一つもないわけなんだ3けど。でも、SFなら、そういうものが読みたい気がする。武器店みたいな。

歯医者さん

今年は結構いってる。今回は右下のブリッジのところ。「前の方ははずれてますね」で、中がやられてしまった。

割と調子が良かっただけに残念すぎる。前の方の神経抜いてブリッジ作り直しですか。もっとも9年使ったのでそんなものか。

でも、前歯の方は20年以上使ってるんだよな。

麻酔が抜けないまま昼飯食ったら、口の中をかみまくりました。

いろいろ壊れる

昨日の夜にシス管が「321のMac Miniが死んでます」で、見に行ったんですが、超熱くなっててだめぽい。TreeVNCが暴走するってのがあってなぁ。

しばらく電源切って冷やしてと思ったんですが、やっぱりだめ。Rescue mode からのOS再インストールからでもこける。あとは PRAM reset くらいか。

もっとも、これは現システムの一部なので修理してもらえるかもしれないな。こいつ経由で画面共有に使ってるだけなんですけどね。

Apple TVでも接続はできるのだが、学生への配信がな。

まぁ、自分のMBPから配信することもできる。ただ、プロジェクタに接続する必要はある。あるのだが、

　　HDMI display adator が反応しない

あれ。教卓に汎用のを置いてくれてたので、そっちを使うと写る。戻すとだめ。そういえば最近使ってなかったからなぁ。

あと、自分は使ってないんですが、ケーブルを使わない充電器が

　　充電できないわけじゃないけど遅い

と言う技があるらしい。置いといたら使えないから意味ないじゃんとか思うけど、学生は便利だとか言ってます。

でも、最近はイベントとかでDeNAとかが配ってくれてるので、それを回収しました。

Adaptor どうしようかなって話題は、Facebook でもみたな。

てだこ浦西の乗り換え(続き)

今度は高速バスの下りに乗り換えてみました。雨男なので、スーツが絞れるくらいの土砂降りくらったが...

いや、この坂は無理だわ。これは滑落したら死ぬだろ。ちなみに最短距離は私道のようです。

県庁前から直接高速バス使うのに勝てるとは思えないな。97には余裕で勝てます。

まぁ、選択肢があるのは良いか。古島からやんばる急行とか。

だんだん出てくる

まぁ、猫だからなぁ。オス猫二匹は、あんまり、そういことしなかったんだが...

Automaton の結合

Automaton で受理される言語(文字列の集合)の個々のものをつなげたものを受理するAutomatonがあるって話。

途中でどこでわければ良いかわからないから非決定性Automatonを導入するってやつです。で、非決定性Automatonは決定性に変換できるから証明終了と。

なんだけど、ちょっと待て。確かに非決定性Automatonは作ったけど、それが正規言語AとBの結合に等しい言語を定義しているかどうかは調べてないよね。

いや、確かに、図を見ると自明なんですが。でも、そもそも非決定性Automatonの受理のルールが複雑だからなぁ。

で、実際に Agda で証明に行くわけですが、予想通り、かなりはまった。

　　split : {Σ : Set} → (List Σ → Bool)
　　　　　→ ( List Σ → Bool) → List Σ → Bool
　　split x y　[] = x [] /\ y []
　　split x y (h　∷ t) = (x [] /\ y (h　∷ t)) \/
　　　split (λ t1 → x (　h ∷ t1 ))　(λ t2 → y t2 ) t

　　Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
　　Concat {Σ} A B = split A B

こんな感じで言語の結合は定義できるわけですが、 contain A x で Automaton A が x 受理するとして、

　　closed-in-concat :　{Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )

こんな感じで Concat が、でっちあげたNFA である M-Concat A B と等しいことを見に行きます。すると、

　　　(1) closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true

と

　　　(2) closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true

とを示すことになる。まぁ、そうだよな。

finiteSet 有限集合の∃関連の述語は一通り書いたし、split の逆とか使って、(1)はスムースだった。仮定から二つの入力が
あるのがわかるので、それが実際に受理されることを NFA をたどって示せばよい。

なんですが、(2)が良くわからない。

　　　ずーっと A で動いていて、Aが終わりで残りが B なら Ok

つまり、A until B 見たいな時相論理式を証明にいくわけだな。

　　aend (automaton A) qa) /\　accept (automaton B) (δ (automaton B) (astart B) h) t

を調べて真なら、それで成立。成り立たなかったら次の状態に進む。

なんだけど、M-Concat A B が非決定的なので、

　　　途中、B になりそうになるが、いつか B でなくなる

ってのがある。つまり、 accept (automaton B) s x ってのが、その時点では判明しない。この辺、専門なはずなんだけどな。

　　ab-case : (q : states A ∨ states B ) → (qa : states A ) → (x : List Σ ) → Set
　　ab-case (case1 qa') qa x = qa'　≡ qa
　　ab-case (case2 qb) qa x = ¬ ( accept (automaton B) qb x　≡ true )

　　contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
　　　　　→ (qa : states A )　→ (　(q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )

とかいうのを思いついて、ようやっと突破できた。

いや、でも、ちょっと複雑すぎるだろ。NFAに閉じれば簡単になるかも。co-induction とか使えれば面白いんだが。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/automaton/file/tip/agda/regular-language.agda

てだこ浦西駅のバス乗り換え

幸地(那覇向け)側から乗り換えてみました。まぁ、夜は暗いんだが、最近はスマホを懐中電灯代わりにしてるので平気。

思ったより近い。3分くらい。坂の上り下りはあるけど。車椅子でもいけるかというと、階段があるのでだめです。

125/56/97から便利な道の方は、やっぱり私道でチェーンが張られてました。が、まぁ、歩きなら通っても怒られないかも。

途中には異世界へ続く道が。上の会社かなんかをどかして道にするらしい。

もう琉大までは来ないかも知れないけど、来るとすると、坂田でまた90度曲がるのだな。

終電が遅いのは便利なんですが、だいたい半分くらい歩いたところでめげてタクるパターンですね。全部歩けばバスより安いけど。

ストレスチェック

紙で URL とパスワード送ってくるってどうなの? まぁ、うちの学科でも学生の初期パスワードは紙で配っていたりするわけですが。

いや、教職員は全員メール持ってるわけじゃん。メールで送れよ。

　　読まないから

まぁ、そうだよなあ。メールで送ってくるストレスチェックなんてSPAMかウイルスに決まってるからなぁ。

で、まぁ、入力したのですが

　　ボタンがおせない

え、ちゃんと11/15金からって書いてあるじゃん。え、

　　今日は金曜日じゃない

あ、そうですか。あ〜　ストレス貯まった〜 こんなんでも、どうせ役人の引退先だろと思うと余計。

Libretto 50

Mobile Gear とかの話が出てたので、思い出しました。東芝のノートPCの名機。たぶん3年くらい使ったかも。

CPU は Pentimum 75MHz / Memory 32MB / 640 x 480/ 24 bit true color なはずです。もちろん、英語キーボード。

日本語キーボードだと少しきーが小さくなって右寄りになって打ちづらい。

電池は持たなかったので二本持ち歩いていた記憶がある。

当時、このTFT画面は綺麗に感じたな。ピッチが細かいので写真が綺麗。これで取り込んだ写真が結構ある。この時は DVR PC7 かIXY 200 か?

このPCMCIAにPHSを刺して使うわけだな。だいたい remote login でメールとかは処理していたはずです。

これで予算申請通していたりとかしてた。kernel build とか OSの課題作りとか。

Libretto 20/30も使っていた(当時はお金持ち)けど、HDDの換装のせいか結構不安定になった記憶。50はそういうことはなくて、

　　4GB HDD

まで増やしたはずです。これくらいあると平凡社の世界大百科とかが入る。いろいろ便利だったな。

OS X PB が Dula USB iBook と一緒に出て、そちらに乗り換えるまで使いました。あれは重かったのだが、その後、もっと重いのを使う羽目に。

今の、MBP 15inch は、それに比べると軽いな。

HTMLの中の写真

研究室紹介で、いつものHTMLを使ったら写真が巨大に... 去年も一昨年も同じことやったんだろうか?

ググると「pixcelで指定しろ」とか。それはないな。まぁ、ポスターみたいなWebなら、そうかも知れないけど。

width="80%ぐかいが普通か。変換系使ってるので、なかったら付け加えるくらいしても良いかも。

貧乏くさい話シリーズ ピコピコサンダル

ビブラムソール使ってるんですが、靴の底が減ってくると、ゴムに穴が開く。別に貫通しているわけではないので問題はないんですが、

そこに小石が入って、歩くたんびに「からから」言う。まぁ、穴を大きくして、石をだしてやればいいんで8すけどね。

なんと、沖縄の靴屋さんだと靴底を張り替えてもらなくて、東京のいつもの靴屋さんに送ることに。これが割と高く付く。

まぁ、靴なのでたかは知れてるし、毎日使うものなんだから、ちょっとは良いもの、手入れの行き届いたものと思うんですけどね。

え、続くの?

http://www.ne.jp/asahi/jibiki/seika/

Data.Fin と∀と∃

NFA 非決定性オートマトンの条件は、非決定的というだけあって集合から適当に取り出すということをします。

無限集合だと選択公理とかあるんだけど、有限集合なら全部調べればよい。というのをAgdaで書くのだが、これがはまる。

Fin n で n 個の自然数が取れるので、n から始めて 1 で終わるわけなんだけど、実際の要素は i-1 を使う。ややこしい。

条件に合うものを見つけて終わりなんだけど、なぜか、

　　0 に行った時にどうするか

が問題になる。それは起きないはずなんですが「それを証明する必要がある」。あぁ、まぁ、確かに。そうだよね。

あるとわかっていて探しているので「なかったら矛盾」で良いわけですけどね。なので、

　　「i>mの時はない」ってのをnから始めれば、m=0になった時に「あるって言ってたのにないじゃん」

と言えるというのに、昨日、Bar で飲みながら Agda を書いてた時に思いつきました。これで解決。

なのだが、これはテンプレだからライブラリにあるはずだよなと、Agda の Data.Fin を見ると、

　　¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
　　　　　　　¬ (∀ i → P i) → (∃ λ i → ¬ P i)
　　¬∀⟶∃¬ n P P? ¬P = map id proj₁ (¬∀⟶∃¬-smallest n P P? ¬P)

とか三行で書いてある。いや、そこまで来るのに、いろいろあるので、これを使うかどうかは微妙なんだけど。

Agda まだ、知らないことたくさんあるらしい。

もう一つはまったのは、Data.Fin とData.Natの変換。

　　toℕ-fromℕ≤ : ∀ {m n} (m<n : m ℕ< n) → toℕ (fromℕ≤ m<n) ≡ m
　　toℕ-fromℕ≤ (s≤s z≤n)　　　 = refl
　　toℕ-fromℕ≤ (s≤s (s≤s m<n)) = cong suc (toℕ-fromℕ≤ (s≤s m<n))


これだな。自力で証明できるところまで来てライブラリにあることに気がつく、いつものパターン。

遭難中のルンバ君とコタ

どっちも同じくらいの年齢なんじゃないか説。敷物巻き込んだようだ。

新入りと比べるとコタのアホさとヨボヨボさが目立つこの頃です。

ルンバは猫毛掃除機としては優秀。

Subset Construction

なんか去年苦労してた気がするんだが... NFAからDFAを作るってやつですね。作ったものが元と一致する証明さぼってたんですが...

授業が終わった後、書いてみたら一発だった。どういうこと。やっぱり、Agda力が上がってるってことか。

　　　　(NAutomaton Q　Σ ) → (astart : Q ) → (Automaton (Q → Bool)　Σ )

状態Qの非決定性オートマトンを、状態(Q→Bool)な決定性オートマトンに読み替えるだけだから、入力をたどれば一致することは自明。

FiniteSet は Q が Fin n (0..n)に isomorphic (1対1)だってのですが、ちょっとださいかな。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/automaton/file/tip/agda/sbconst2.agda

読書会

高校時代も高2高3辺りで読書会とか良くやってました。友人の趣味でエーリッヒフロム。僕はラッセルの方が好みだったが。

大学に入って、 すぐ友人が読書会やろうというのでやろうと言ったのですが、それが

　　ベルグソンの自然の弁証法

なんで、そんなものだったかと言うと、まぁ、当時の生協がそういうところだったからなんですが、これがクソな本でな。

読書会では、もっぱら本の内容で大爆笑シリーズだったはずです。だれだよ、こんなのお題に選んだの。

で、その後もいろんな本を集まって読んでました。吉田夏彦先生の哲学の授業と研究室の周辺の人たちですね。日本語英語手当たり次第にいろいろ読んだ。

　　浅田彰
　　事的世界観への前哨
　　ノーベル賞受賞論文集
　　WVO Quine 経験主義のふたつのドグマ
　　力学の入門書
　　観測問題論文集
　　量子力学
　　Diracの一般相対論
　　Diracの量子力学
　　資本論 (1-4)
　　経哲草稿
　　連続群論
　　回転群の表現
　　層圏トポス

まぁ、楽しかったな。全部理解できたわけではないですが、計算を追うくらいは。この辺にいろいろ影響されていたことは確か。

院生時代は、分厚い英語の教科書を朝集まって問題解いていくとかやってたみたいです。データベースとかオートマトンとか。

もっとも、これらに一貫したものはないわけですが。たまにうちの学生も勉強会とかやってるようですね。

浦西駅

125番のバスで行ってみました。前田入り口つまり紫雲閣からだと駐車場経由で行けるんですが、ちょっと遠い。エレベータ付き。

西原入口だと、なんと駅前に降りる道ができてました。これは車も通れそうだが...

125/56/97 が駅経由で乗り換えできるようになると便利なんですけどね。こいつらの相互乗り換えもかなり不便なので。

この道、バスは通れないこともない気がするが... 私道っぽい。そもそも西原入口を通れなくする必要あったの?

まぁ、いろいろ未完成ではあるけどさ。バス会社側のやる気のなさっていうか悪意っていうか...

琉大まで来るとしても10年後でしょう。

ズボン破れた

これ、Ingress で一番やせてたころにつくった奴じゃないかな。でも生地もけっこうぼろぼろ。Ingeess も結構長くやってるからな〜

新しいScannerが、どんどん遅くなってて残念。サーバーとの同期がよろしくないらしく、詰まったりずれたり。どうせ、サーバレスとかだろうけど...

はっかーずちゃんぷるー

いや、一応、きたんですが、

　　昨日飲みすぎて、二日酔い

なので、さぼって、Agda をいじってます。すみません。

なんかヨガやってたり、トラブル対応の演習やってたり、わりとカオス。

民間英語試験

なんか延期になってしまってがっかり。うちは院試には最初からTOEFLを使っているんですが、割と便利。先生が問題考えなくていいから。

採点基準も安定しているので「今年は英語のできが悪い」的な評価も可能。ただ、PBTで400の下の方が多くて、

　　それでは使い物にならない

って方が問題。高校の教科書の語彙は2千くらいらしいんですが、大学生レベルだと6千は欲しい感じ。PBT 550からが実用的なんですが、語彙的にはそんなものかも。

僕も高校時代はあまり英語は勉強しなかったんですが、理由の一つは勉強しなくても通るから。あの受験校でもそんな感じ。

まぁ、おかげで浪人時代にだいぶ勉強する羽目になって、受験のレベル的にはそこそこまでいった。でも、

　　それでは使い物にならない

哲学の本とか論文とかSFとか知らない単語ばかり。先生には「なんだ、こんなもの読めないの?」とか言われちゃうし。 実は

　　語彙2千から6千まで上げる

のがつらい。2千まではそんなに大変じゃない。学生を見てると千ぐらいな感じ。コードに書く変数の綴りが怪しいレベル。

　　コメントに日本語書くな! ベトナム語でコメント書いてあったら困るだろ

っていうんですけどね。卒業までに英文5千ページ読めと言ってます。

言いたいことは、

　　大学受験の英語レベルが低すぎて早めにサチってしまうことの対策には民間英語試験が良い

だろうってことです。

まぁ、必須にするには準備不足だったようだが、お役所の「受験スケジュールに合わせろ」的な指導がダメだった説も。もう少し落としどころなかったのか?