Bleach 復習 #240

なんか330くらいまであるのかな。ただ、

　　大人の事情

が多くて、アランカルの本編はそんなに長くない。

　バウント、死神の過去編、現世のおまけ、浦崎の隊長時代、斬魂刀異聞

全部飛ばせば。水着回とかもあったな。いや、でも、

　そういうおまけ部分が面白い説

もあるね。 https://bleach-anime.com

水道タンクの絵

昔は綺麗な天女が描かれていたんですけどね。

確かに宜野湾(そしてどこにでもある)天女伝説がくそな話であることは確かだが、

こんなことして誰の得になってるとも思えない。

世界がださい中性化を選択するのは一種の滅びの道かもしれないな。

ワクチン三回目

PPMです。NBS沖縄、結婚式場という大変便利な会場

　　ライカムのバス停から歩いて30分

ま、Ingress Agent にとってはどうってことない距離だし、沖縄では頭がおかしい人しか歩かない距離だな。

帰りにエメラルドを通るので寄ってみたんですが、綺麗にはなってましたが

　　中身は同じ

でした。せめて、レアって言ったらレアっぽくはして欲しいけど肉的に無理なんだろうな。

Zorn の補題

Generic Filter は書けたんですが、どうも、Filter から Ultra Filterを作るのには、Zornの補題がいるらしく。

Filterってのは、Pの部分集合をいくつか集めたものなんですが、それの極大集合をとる必要があるわけね。

Zron の補題は、学部の頃、読んだんですがさっぱりわからず。その頃は選択公理無視派だったので、それですましてしまったらしい。

で、定義から見直す羽目になってるわけですが、

　　半順序な集合Aで、すべての空でない全順序部分集合L⊆Aの上界sup(L)∈Aがあれば極大元xが存在する。

で、さっぱりわからない。そもそも、x<0 とか極大元ないじゃん。と思ったんですが、

　　いや、それは x<0 という全順序部分集合に上界がないからだ

とわかった瞬間にばっちり見えました。集合ってのは順序数なんだが、それは一次元的な構造を持っていて、

　　上界がないのは極限順序数の直下にある無限鎖だけ

つまり Zorn の補題の仮定「全順序部分集合L⊆Aの上界がある」は、それを禁止しているだけなのね。

いや学部時代の自分に教えてやりたいです。実際の証明は、そこそこめんどい(まだAgdaで書けてない)。

そもそも書いてない本が多い。シンガーソープと公理的集合論にはなくて、岩波現代数学概説Iと「選択公理と数学」には長いのがある。

新井先生の数学基礎論のはなんかかっこいい証明なんですが全然読めなかったんだが、わかったら読めた。そんなもんです。

nlab の証明も結構長くてあれなんですが、もしかすると、もう少し簡単に書けるかも。

チコノフの定理が極大Filterの存在なので、

　　もしかして、Zornの補題の直積がチコノフの定理なんじゃないか?

と思ったら、そういうものらしい。プロシンでは「今年はチコノフやるかも」とか言ってたんですがなんとなくできそう。

https://ncatlab.org/nlab/show/Zorn%27s+lemma

コンパイラ読み会最終日

午前中はいつもの System FC / Haskell Core のスライドを見てました

debug build は、まだ、終わってなくて、でも、できたことはできた

ただ、

　　Singularity 作ったあと変更可能にする方法

がまだ良くわかってない。まぁ、なくてもいいんだけど。時間がかかるのがな。

あとは、Haskkell / Agda をちらちらと見てました。いじれるようになるのはまだ先かな。

コンパイラ読み会二日目

今度は GHC を singularity で、これがぼろぼろに難航

Docker iamgeからやれば簡単だろと思ったが...

　　盛大に、version が合わない

元の ghc、happy、alex。aptのは古いし、cabal が

　　/usr/bin に install しない

とか... めんどくなって cp で。

できたころには16時だった。

肝心のコンパイラは「compiler debug optionがdumpしかない」らしいです。

まぁ、Haskell 既に骨董品だからなぁ。

明日は Haskell の続きか、Agda か。

コンパイラ読み会初日 (llvm/clang)

singurality の使い方の復習から... debug build に時間がかかった

-fstandalone-debug

という怪しいフラグを見つけました。

今回はソースコードはいつものところを復習しただけ。

　　環境作りが主だったかも

まぁ、これで singularity 環境ができれば成果かな。

明日は、Haskell / GHC を読みます。

コンパイラ読み会

3/24木から土曜日まで

10:00-12:00, 14:00-16:00, 16:30-18:00

です。Zoom です。リンクは twitter かなんかで聞いてください。

LLVM clang から Haskell そして、Agda まで読みます。なので、超特急だな。

環境的には学科のサーバの singurality 上に作るので、手元のマシンが非力でもまぁ。

LLVM clang は何回かやってるので、ざっと。自分の変更点を見直す感じで。つまり、

　技術継承のためです

Haskell / GHC はなんかやって、やぶれさってるんですが...

　下位に LLVM / C-- / native generator

の三種類があります。Haskell 構築には Haskell compiler が必須。

Agda は Haskell 上に作られているので、

　　Agdaと少し違うHaskellと混乱しなければ大丈夫

自分的な課題としては、Agda からの CbC 生成の方法を探す感じか。

読みづらい

そういうのをかっこいいデザインだと思うのはださい

まぁ、某銀行の「毎回番号を並べ替えるタッチパネル」よりはましだと思うけど。

Agda で書く Generic Filter の続き

いや、なんか、かなり難航してて。

　　順序構造なんだけど、それを集合論のモデルの集合Mのなかに作る必要がある

あぁ、じゃぁ、部分集合の⊂でいいじゃんというわけで、順調だったんですが...

方向が二通りある。そして、大きい方小さい方両方に開いている必要がある。さらに、

　　書き下す時に方向がいりじまってて...

結局、Power P ⊇ L な L でやれば良いってわかったのが、今週になってから。

まぁ、骨子は2年前に書いたもので良かったんですが。で、それは片付いた。めでたい。

なんですが、

　　それを超フィルターに拡大する必要があって
　　すると、¬ G ∈ M が言える
　　それには Zorn の補題が必要

らしいので、まだ少し距離があるみたい。

Zorn の補題は、集合上の二分法みたいな話だというのを発見しました。まだ書いてないけど。

でも一時期みたいに

　　変更点が数十あるのか思いつかない
　　一箇所書くのに午前中潰す

みたいなのはなくなったみたい。でも、少しお休みするべきかもな。来週はコンパイラ読み会だし。

Ingress Event

なんか、さぼる気、まんまんだったんですが、

　　近所にBBを設定されてしまって仕方なく

といっても、まったく準備はせず。

　　隙間をぬって一つ取りました

沖縄も長いので

台風で木が倒れたあとに、植えられた木が、そんな大きさに。

最近は、そんなに大きなのは来ないんですけどね。

何もしてないのに壊れました

ぼくのせいじゃないも〜ん

固定電話やめました

沖縄に来てから、覚えてないくらい番号変わった。ISDN/ADSL/光/引越し

全然、困らない。役に立ったのは沖銀の口座作る時くらい。政府関係のアンケートとか。

クリーニングの問い合わせとか。

月千円くらいだったみたいです。千円も何に取ってるの? そこら辺の若者に聞いても

　　固定電話持ってないです

だよな。電話債権紙切れにされたのを恨んでるわけでもないけどね。今から返してくれても契約はしないだろうな。

モデムももうお役ごめんか〜

原神の現状

均等に育てるのは、あんまりやっちゃいけないとか言われてますが、主要なキャラをLv90/Lv80まであげて、
週ボスを Lv70 なら倒せるようになったので、こんなものかな。

まだ倒しきれないのとかいるんだけど、武器とか天賦とか上げていくと適当に倒せるようになるんでしょう。

遺物堀はめんどうなので進めてません。

タルタリアとかシニョーラとか倒せなかった頃が懐かしい。むしろ、そういう時の方が楽しいんだよな。

タルタリアと言えば、サイクロプス工場の話が面白かったかな。7+ では絶対に飛べなかったのが13では楽勝に。

光学メディアとBleach

まぁ、ほとんど死につつあるわけですが...

　　NASのメンテが面倒すぎる

問題が。Bleach の復習は200まで来たんだが

　　BDでいいじゃん

というより、25GB 割とちょうど良いのかも。

一枚の容量が増えすぎてもあれだし。

新隊長編は少し残念だった。ウェコムンド編はドラゴンボール化してるな。

最初の復習だけ見て飛ばしていくのでも良いらしい。

Generic Filter

なんか、やっと Agda で構成できたんだけど、

　　生成手順のしょうもないミスでした

三週間くらい無駄にしてしまった。いや、元にしてる公理的集合論のタイポがな...

林先生の本を見て、やっと気がついた。できないはずだよ。

いやでもフィルターのあたりは学部1年でやってたはずで、

　　簡単じゃん

とか思った記憶があるんだよな。その時はイデアルの双対とか知らなかったわけですが。

できたあとで、そんなのを思い出しました。

やっと Agda で集合論を扱えるようになってきた感じ。

コンパス

発掘シリーズ

なんであるのかわからないです。父のかも。父はドラフター持ってたはず。

もう使わない。父のノギスを回収するべきだったが、それも、感傷的なものに過ぎないな。

iPod 10GB

発掘シリーズ

なんと、まだ動きますね。初代は5GBだったけど、それでも楽しかったな。

LPを取り込むのも楽しかった。カセットもやる気があればやったんですが、

いろいろ黒歴史もあったので気が進まなかった。

そっちの方が重要だった説もある。

ローソンでプリント

なんか確定申告が... うちは印刷して送る方式なので。ingress の途中でメールで送るとか言われて。

なんか、iPhoneから印刷する時は専用アプリがとか。で、そいつが

　　ローソンのプリンタのlocal wifiにつなげろ

とかで、うまくいかなくて。で、MBP経由USB Cなメモリ経由で印刷。いや、最近、そういうの多い。

　　通らないネットのセキュリティを、USBメモリで突破

そういえば、昔のingress eventでもチケットを印刷して手渡しなプロトコルだったのを思い出した。

カレイドスコープ

発掘シリーズ(続くのか?) 割と地味。白黒なの?

回転するんだけど、iPhone で手で撮るのは難しな。治具を工夫すれば。

黄金宮 クガニナー

嘉数高台にある楼閣あと。沖縄戦の激戦区。

ここからの眺めをみた米兵も多いかも。

ハクソーリッジに、こういう光景が出てこないのは少し残念だったな。

昔ほど、ingress の激戦区ではありません。

やっぱり、野菜炒めでしょ

しかも、肉とか入ってないやつ

YAPC Japan と cpm

いや、本編、ほとんど見てないんですが...

　　内輪受け苦手

ってのが少しあるな。で、本編とはぜんぜん関係ないですが

　　CPAN 最初でえらい (PerlのmoduleのWeb上の集大成みたいなの
　　cpan install でよい

なんですが、

　　cpanm まではたるい

ってのを見かけて。で、cpanm ってなに? になって、

　　brew insatall cpanm

したら、cpanminus ってのが入って、違うかなと思ったら、別にそれで良いらしいが、

　　いや、cpm 使う

ってのがあって、と思ったら、それは既に入っていた。で、Perl/Tk / NKF くらいしか使わないわけですが

　　 /opt/homebrew/Cellar/perl/5.34.0/lib/perl5/site_perl/5.34.0/darwin-thread-multi-2level

に Tk.pm が入ってるってのはわかったんだが、

　　どうやって入れたか覚えてないです

もしかすると、cpm だったかも。

　　Perlのmoduleを入れた履歴とか取れないの?

blog を見ると、cpm でやってるみたいだな。

blog の勧め

ねたにつまった時のネタの一つ

Facebook とか、twitter でもよいんだけど、検索性が悪くてな

そして「消える可能性が常にある」。mixi にも残骸はあるけどね。なので、

　　Facebook は Blogger と併用
　　さらに手元にコピー

ま、そこまで残す価値はないわけですが。でも、

　　自分で見直す楽しみ

はあるかな。そういうものを書くことで自分を確認する感じか。

全然文章書かない学生も結構いるので blog くらい書いてほしいかな。

技術blogではなく毎日が良いです。

ゲーム

自分も割と好きだし。原神微妙にやることなくなりつつあるけど。

修士の学生で、すごくゲームが好きな学生がいて、まぁ、良く思ってない先生もいるらしいんですが、自分は

　　研究もやるならゲームはやってよい

的な感じ。どうせなら、せっかく買った65 inchでやれと。なんだが、

　　また、スマブラ? お前ら何年それやり続けてるんだよ

と思わなくもないです。で、卒業ハリーズの時に、彼に最近どんなゲームやってるって聞いたら、

　　月5クリアしてる

的な話が。エルデンリングとか。で、

　　就職してしばらくやらなかったけど、まったく趣味がなくなってしまう
　　なので、意図的にゲームすることにしてる

なるほど。そんなものか。若いんだから、いろいろやることあるだろとも思うけど、

　　コロナもあったしな〜 (まだまだ続く〜

明白の続き

Generic Filter 一週間格闘したんですが、できなくて。いろいろ考えてたら、寝る時に

　　どうも反例があるっぽい

ことに気がついた。なので、そのままでは証明できないらしい。

順々に集合を数え上げるんですが、そこで飛ばしているのがあって、そこですり抜けるのを止められないっぽい。

「選択公理と数学」の方だと、差分を使っているので、すり抜けたぶんは、そのままで良いらしい。

というわけで、最初の

　　やる気をだすところからやりなおし

らしいです。

卒業ハリーズ

去年と同じで、現地組と研究室とオンラインに分かれて

今年はOB組は捕まからなかったか?

出し物特にないので、内職しながら