広告まみれ

いや、まぁ、広告 Blocker は入れるでしょ? なんだが、

　　facebook が直接見せるやつの広告がすり抜ける

なので、普通は facebook 内でみないで、別途、ブラウザで開けます。

一時期の「いきなり男の裸連発」みたいなのは少なくなったような気もするが気のせいか。

スパムと発想は同じで「何万人の中から馬鹿が二三人引かっかれば良い」ってやつだよね。

自分から積極的に探しにいくもの以外にまともな情報は存在しないわけで...

GAFA でも仕事している人たちが頭が良すぎるので

　　とにかく量、人に見せれば良い

的なことするんだよな。本当は、

　　ネットの情報を人類全体が向上するように見せる

みたいな主義が必要なんだが、そんなことを目指す人は馬鹿認定なので、まぁ、仕方ないか。

人類のネットは本来は、人類全体の脳であるべきだけど、

　　馬鹿増幅器

みたいになってるのがなぁ。21世紀は馬鹿の時代ってのが自分の認識ですけどね。もっとと、こう

　　情報の根拠を自由に検証したい

そこでプライバシーみたいなことをいうのは金持ちだけでよくて、貧乏人はプライバシーの切り売りでいいかな。

スーパーの裏

怪しい。父の工場もこんな感じだったな。昭和なイメージ。

石嶺というより経塚のゆいレールのところのサンエーですね。

ここは交差点を行き過ぎて、裏道からはいる方がよい。

坂田のマックスバリューの品揃えが割とダメなので、こっちによってみました。

ゆいれーる運転席

いや、そこは、もうちょっと本物志向でお願いします。

iPhone の血圧入力

AppleScript の支離滅裂さは相変わらずというところですけどね。ショートカットで入力して、

　　ssh で server に command 経由であげる方式

いろいろ使えるわけですけど、この入力で

　　血圧の下を入れるのか上を入れるのかどっちかを判断するのは難しい

なんか、こういう

　　上下を間違えやすい用語が好きな人たち

いるよね。左辺値右辺値とか。

まぁ、ないよりましか。今までは、Terminus で command line 打ってたりしたので。

あっとんの話

いや、自分も何も知らないので、単に思い出話を書くだけです。

たまに、いる超優秀な学生で1年からずば抜けてるというパターンですね。後輩の面倒見もよくてな〜

学生のPC管理/DNSのを Rails で書き直してくれて、それが今も使っている Akatsuki ですが、
この前、PowerDNS 用に書き直したのだった。既にどう書き直したのか覚えてないですが。
BIND9 と両立させたかな?

でも、それも片手間だったりするわけですけどね。うちの研究室で、

　　Proofs and Types と Agda を一緒に学んだのも楽しかった

もちろん、得意なシステム関係とか実装やっても面白かったんだけど、

　　だからこそ、違う方向にいくのが面白い

実際楽しかったんですけどね。2016くらいだったので、

　　京都とか松本城とか

に遊びに、いや、研究発表にいったのも良かったな。

ゼミ中とかに学生に「トランザクションとは何か」とか「同期キューと普通のキューの差」とか聞くのが好きだが

　　常に適切な答えが返ってきたのは、あっとんだけ

いや、まぁ、なんかすごかったな。M2くらいから体調崩して、ペースは落ちてたんですけどね。

一昨年のシステム更新でも、手伝ってくれたり。

　　沖縄に戻ってこいと言ったんですが、「先生に捕まってしまうのはいや」

ということだったらしいです。自分的には、あの時のあっとんの研究方向がだいぶ進んだので、また、一緒にやってみたかったが。

Zornの補題の続き

　　全順序部分集合 B には上界 sup B ∈ A があって、∀ x ∈ B → x < sup なら極大元 m ( m < x な x がない) がある

なんですが、

いや、思ったより難航してて... この前の三択はあともう少しだけどだめだった。可算鎖ではやっぱり取りきれない。

1961年の岩波現代数学概説を取り出して読み直したら、

　　非可算上昇鎖と、最大全順序部分集合は別に作る

のね。半順序なので、一点 x ∈ A から
＿
＿/
　　/ \__
　　\_____

みたいに木構造で広がって「枝同士は比較不能」。なので枝を選ぶ必要がある。それには枝を選択する関数 f がいるんだが、

　　x < f x (極大元がない仮定から選択公理で作る無限上昇鎖
　　x ≦ f x (この条件での任意の関数、割り込まれない ( x < z < f x になる z はない

と使い分けるらしい。確かに、上で枝を選択すると最大整列集合は作れない。作るためには別な関数が必要なのか。

　　最大整列集合が作れれば、その sup で、下の f で、sup ≡ f sup となる

で、極大元がないと上の関数が下の条件を満たして sup < f sup と sup ≡ f sup で矛盾がでるので、極大元があるという流れらしい。

最大整列集合の作り方は

　　C0) s < f s < f (f s) < f (f ( f ...
　　C1) 0) の全部よりも大きい x1 < f x1 < f (f x1) < f ( f( ( f ...
:
:

なんだが、可算鎖を飛ばすところが何が書いてあるのかわからなかった。ですが、Zorn の補題の仮定の

　　全順序部分集合 B には上界 sup B ∈ A があって、∀ x ∈ B → x < sup

ってのがあるので、 sup C0 ≡ x1 とすれば良いらしい。つまり、

　　なにか y ∈ A があって、x ≡ f y
　　y < x となる y がなくて、超限帰納法で作ってるその時の整列集合 C にたいして、sub C ≡ x

その二つの条件を満たした x を超限帰納法で足して作っていけば最大整列集合が得られる。

理解できれば、簡潔かつエレガント。いや、

　　現代数学概説、岩波のいつものわけわからないやつ

で苦手だったんですが、「わかってみるとわかる」といういつものパターンだな。文句いってすみませんでした。

まだ少し穴は残ってるが、なんとかなるっぽいです。


現代数学概説〈1〉 (現代数学 1)
詳細情報: https://www.amazon.co.jp/dp/400005290X

既に壊れました

ま、そんなもん。使いえないこともない。

猫毛

まだ若いからなぁ。今頃の季節はね。年寄り猫にこれやりすぎると、

　　はげるらしい

です。気をつけよう。まぁ、一通り取ってやると気持ちよいらしい。

Diverging diamond interchange

なんか新しいタイプのインターチェンジらしく。もしかして、大平インターにも使えるのか?

途中で左右を平面交差で入れ替えるというわけわからなさ。しばらく考えてわかったんですが、

　　これって一般道側の橋が短いと通り抜けは交互通行になる

まぁ、どうせ一般道は信号あるからそれでいいのか。そもそも大平のだめな原因は、

　　左から入った右折車が橋の上に溜まる

のはだめなので、それがまっすぐ抜けるように信号制御するなら、

　　別に途中で左右車線を入れ替える必要はない

かなと思うんですけどね。もしかすると流行るかも知れないな。

https://gigazine.net/news/20180312-new-intersection-design-ddi/

Hugo の .md の置き場所

いや、どこ探しているのかくらい教えてほしいんですが。おそるべきことに、

　　使う theme によって探す場所が違うらしい

しかも、

　　If your content is in content/posts the .Type is posts (plural).
　　If your content is in content/post the .Type is post (singular).

なんで、わざわざ「中の type: post 」を見て、content/posts にそれがあっても排除するみたいなことするんだよ。

gitlab のは posts 以下だったらしいんだけど、plugin によって

　　content/posts
　　contents/post

とかばらばららしい。ひどいなぁ。draft: true をと書いてあるのを排除するのは、まぁ、わからなくもないんだが...

current directory 以下は全部の .md をみる仕様じゃないのか。

NetlifyCMS で書き込むのも悪くはないんだけど、gitlab 依存なのがなぁ。

修士のソースコード読み会

なに読もうか考え中

　　Emacs の portable undump

ってのはどうでしょう? マニアックすぎか?

コンパイラの続きやるって言うてもあるが。どっちかっていうと、

　　singularity で開発環境作る練習

的な感じでもあるかも。最近の

　　malloc 系

を読んでみても良いかな。

Bleach 復習 311

やっと、アランカル編の終わりまで。まだ、もうちょっとあるんだよな。

ドラゴンボール化するのは、まぁ、仕方ないんだが。

ウルキオラのあたりが良かったけど、宝玉覚醒のあたりからは、そんな感じ。

こういうのは勢いなので。

謎の怪人

まぁ、趣味なんだろうな〜

人は入ってないようです。

なんちゃって筋トレ

ぜんぜんがんばってないです。20回の腕立てと腹筋を2セットくらい。

　　昨日やってたらやらない
　　思い出さなかったらやらない

そんな感じ。この手のものは続けてる時は効果がない気がするものだが

　　できなくなった時に差を感じるもの

かも。もっとも、一時期減らしてた体重はだいぶ戻ったんですけどね。

まぁ、気が向いたらやるくらいで続けていこう。

agda-vim

Agda は Editor と組み合わせて使うわけなんですが、

　　まぁ、VSCode でしょ

ってわけですが、自分は emacs + viper 。なんだそれ。ところが、学生に「やってみて」と言ったら

　　vim でやりたい

と。え〜。いや、それで使えるなら自分が使ってるんですけどね。agda-vim という plugin があるんだが...

　　またっく動かない。ピクリとも。

いや、前に動かした時は、まぁ、動かなくはなかったんだが。で、朝いろいろ調べてみたんですが...

　　そもそも、AgdaReload とかが定義されてない
　　そして、それは python 側にある(はぁ?)

で、発見したのは

　　そもそも、macOSのdefaultのvim は python2/python3 support を切ってある
　　brew の vim は、python2 は切ってある
　　brew の neovim は、python 側に neovim 用に python module を入れれば動作する

で、さらに

　　agda-vim は python2 (古いからな、おそらく、その頃は vim script は python2 only)
　　agda-vim の python3 patch はあるが、7年前のもの
　　agda-vim-async なるものもある

ってのを、vim 三種類、vim plugin三種類の組合せで試す感じ。ところが、

　　その間に、macOSのupdateをしたら、python2 が消される羽目に

お前らそういうことするなら「世の中のすべてのpython2 script がそのまま動くようにしてからやれ」

agda-vim の python3 patch + neovim では動いたみたい。でも、割と残念な感じ。

VSCode 側もご機嫌斜めな感じで、動いたり動かなかったり。Emacs は、まぁ、動いているみたいだが。

ずいぶん前に見捨てたものだが、agda-vim-async は何かが足りないらしくまったく動かないが面白いかも。

でも、こういうものじゃなくて、editor とは関係なく横で agda の検査結果を表示するもので良いんじゃないか?

そういうものつくるか?

それとは別に maplocalleader が、まったく動作してないのも発見したのでなんとかする予定。

ここ何回目かの「完全に理解した」

Zorn の補題は相変わらず難航中なんですが、

　　割と、逆転につぐ逆転的なところがあって...

基本の「極限順序数以下の順序を越えない限り、上には抜けない(1)」ってのは、まぁ、そうなんだけど...

やっと、極大元があるか、上に行くかだけではなくて、三つ目の選択肢があるってのがわかって...

　　極限順序数以下で、ずーっと、飛び回る

ってのがあるのね。そこで、さらに、

　　その飛び回るのは可算無限回

つまり、上には上がある程度で、仮定(完全順序部分集合の上界がある)に反する(2)ってのわかりました。

今度こそ、証明できるはず。というわけなので、二段階の証明になるわけね。

本ごとに証明が違うってのもあって、かなり面白い。いや、なんかこう、

　　Bleach のなかなか死なない強敵

みたいな感じあるな。いや、

　　まだまだ、続く

のか?! 学部時代に歯が立たなかったのは残念だが...

キャンパスバス

本当に

　　名前が変わっただけ

本数減ったのかな。そもそも、

　　てだこ浦西→公栄→真栄原→沖国→長田→琉大

なんだけど、そもそも、

　　てだこ浦西→琉大入口

が高速バスで三分なので、存在意義が不明。まぁ、98の本数が増えたのは良いんですが。

なくなってないだけましか。

　　琉大→北谷

とか

　　琉大→ライカム

とか作って欲しいかな。

初代 OS X

お金取ってたんだっけ?

PBからではなてく、Rahpsody から使っていたんですが、

　　Rahpsody がめちゃくちゃ遅かった

ってのがあって心配してたんですけどね。PBで、

　　普通の Unix (OPENSTEP)じゃん

で、まぁ、ひと安心。

　　そこから20年以上も使うとは思わなかったけど

学生が Linux をノートPCに入れるのに苦労しているのを見ると、macOSで良かったなとは思います。

頭の中で証明を作る

Zorn の補題は難航中なんですが...

　　Agdaなんだから、Agda 自体が考えてくれるんじゃないの?

まぁ、細かい部分はそうなんだよな。適当に埋めて通ったり。

でも結局は、頭の中で考えてからになるみたい。

その時、その時で学びはあるわけだけど。

前順序とか半順序とかの構造が明確になるのはよいかな。

そろそろ片付いてほしいところですけどね。

誰も取らなかった講義

一回ありますね。コンパイラ構成論で、講義室に行ったら

　　誰もいなかった

次の週も行ったんだが誰もいなかった。実は、

　　登録は一人してた

結局、その学生は、うちの研究室で修士を取ったわけなんですが。

　　いや、コンパイラ構成論取れよ

ってわけだけど。もっとも、

　　講義って知ってることを教えるだけ

なら、

　　本読んで、問題解け

でいいと思うんだよね。先生と、あるいは研究室の面子と一緒に本なり読んだりするのは、

　　自分が初めて学ぶものに対して、どう対処するのか

それを、同時に体験することなんじゃないかな。

なので、いつも「自分の知らないこと」を、講義の最中に入れるようにしてる。その方が

　　自分も面白いし

そろそろ授業が始まるわけだが、前期は、サーバ班中心になるはずです。あぁ、

　　修士のソースコード読み会

もあるな。

wordle

こんな感じ。英語っぽい単語を当てるゲームになってる気もするけど。

初めて二回めで当てたな。

我如古の歩道橋

渡ってる人とかめったに見ないわけですが... 歩道橋ってのはそんなもん。

ちょっと前に撤去してたので横断歩道になるのかと思ったら復活。

まぁ、高いところ好きなので嫌いではないです。

四角の無駄な感じも割とよい。斜路つきなので自転車も通れる。

キャベツ

これと味噌だけでお酒はばっちり

あ、いや、ごま油とか要らないんで...

インストール大会

まだ、大半の授業はオンラインなんですが、これは避けられない。

　　相変わらずMacBook

なんですが、今年は256GB。128GBだと課題のたびに何か消さないとだめとかあって。

入学式と同じ日なのでスーツ姿な学生もけっこう。まぁ、形から入るのは重要だからな。

PC詳しい学生はさっさと終わらせて、用意したものもスペック一つ上だったり。でもそうでないのはゆっくり。

センタ側の教室のWifiの非力さは相変わらず。有線並用だけど、だめな端子も多く。ま、かたづいたからいいか。

　　自分のノートPCは、自分の刀だろ、ひのきの棒で戦うのかよ

というわけですが、まぁ、なかなかね。

極大Filter と超Filter

ってのをやってました。まぁ、時間切れっぽいが、Zorn の補題もだいたいできた。

Filter は⊆で順序付けられるLの部分集合の集合で、

　　上方に閉じている(Filterの要素を含む要素はFilterに入っている)
　　二個ずつの∩について閉じている(Filterの要素二つの∩はFilterに入っている)

なんですが、極大は一番大きいやつ、超Filterは p ∈ Power L か補集合 (L \ p ) ∈ Power L のどちらかが入っている、

と思ってて全然できなかったんですが...

　　極大は「任意のFilterよりも大きい」じゃなくて、それを含む真に大きなFilterがないこと
　　Filter の条件に proper ( 空集合は含まない) がある。

ってのにやっと気がついた。

確かに、超Filterを含んでいたそれよりでかないなら、でかい分の p とその補集合の両方が入るから。
p ∩ ( L \ p ) が入るので空集合が入ってしまう。proper に反する。

逆に、Filter は入ってないもの p があったらそれを全部に付け加えればどんどん大きくなるんですが、
proper だとそうならない。 p と ( L \ p ) の両方が入ってない状態なら必ず大きくできるので最大でない。

極大Filter と超Filter が同じなのは proper っていう条件があるからなのがわかりました。

テレビを観る猫

一緒に Bleach を見てるところ

やっと刀編が終わるかな

通帳と暗証番号

最近は、口座作っても通帳ないのね。それはよいんだが...

　　暗証番号が通らない

作った時に入金はした記憶があるんだが... で、

　　暗証番号の変更は銀行にいかないとだめ

つまり、東京にいかないとだめ。うーがー。まぁ、放置でいいかぁ。

なんか口座作るのに暗証番号手書きした時、だめだとは思ったんだよな。

on line bankign 試した時に通らなくて変だとは思ったんだが、もう少し追求するべきだった。