Twitter CLI

いや、Perl で書いたのがむかしからあったんですけどね。

　　当然のように動かない

最近は、Perl の module は cpm で入れるんだが、こける。

　　openssl header がない

なるほど。brew install openssl が良いらしい。Net::Twitter は少し API が変わってましたが、動きました。

でも、まぁ、使わないよね。なんのために入れてるんだか。

では、よいお年を。

○○ Bar

いや、別にいいんですけどね。こういう開き直りは嫌いじゃない。

年末進行

といっても、呼び出されて飲みまくってるだけですが。

今年はzornの補題な年だった。できてよかったが。チコノフの定理とか可算モデルとかもできそうな。

それはゆっくりでいいかな。OSの採点とかしてるはずです。(つうか、それをやれ

カレンダー

あんまりスケジュールとか関係ない人なんですが、この前からカレンダーの管理が死んでて。

いや、Google Calendar でいいだろとも思うんですけどね。

　Web上の main.ics を生成して読み込ませる方式で、それをみて cron でメールを送る

みたいな方式で、30年前からそれだったりするんだよな。

Perl script で重複を消すように調整して、/usr/bin/mail を mhmail にしてとかやってたら動いたので、まぁ、いいかな。

　grep -l new ~/Library/Calendars/*.caldav/*/Info.plist

とかすると、Calendar.app の new という予定を取れるらしい。割と変わってない。

可算モデル

Zornの補題終わったので集合論みなおしてたんですが、01の可算無限列の順序を選択公理を使ったZornの補題で極大フィルターを作ってで証明するんだが、選択公理は整列定理と同値だから、それは仮定そのものだなと思ったり。

で、Power/Unionを見直して、もっと簡単な形で良いことを発見したりしたんですが、

　　可算順序数と Power ωは両立しないよな

とか考えて困ってたんですが、そもそも集合論の可算モデルって何? ってことに。レーベンハイムスコーレムで可算集合に落とすんですが...

Mが可算モデルってのは、集合論のモデル、つまり公理を満たすことを証明する時に使う値に番号を付けるみたいなものだなと。

対角線論法でも、確かに Power ωから可算個対応させて、ほら別にもう一個あるでしょで、Power ωの中の可算個しか使ってない。

Mが含まれてるZF全体の集合のごく一部がMに入っていて、Mがモデルみたいな面をしているだけなのね。

Mは可算だから、Mの中の順序数に対応するものは可算順序数になっていて、その中で Power ωは、やせほそった可算集合でしかない。

でも、それはその中のωよりは大きい。そういうことか。

現場猫案件

まぁ、実害ないならいいんですけどね。

前は、連絡橋の下部の一部が落下したことがあった。

Ingress の裏道

まぁ、歩くためにやってるわけなので。

ここから階段の下の三角を抜けて。昔の太陽市場のところに。

まぁ、危ないところは攻めないようにはしてます。

学生の装備

Fortigate/Yamaya/NEC/Cisco と楽しそう

プロシンのあと、少し東京にいる予定です(1/9-11)

ChatGPT で OS 教科書のの問題を解く

英語の問題なので英語で解答されてしまいますが、日本語でといえば日本語になるはず。

問題は、ABIとAPIの特徴的な違いはっていうShilversharzらしい問題ですが、

　　OSの教科書の問題ってのを知らないから一般的に解かれてしまう

まぁねぇ。要求しているのは

　　プログラマはAPIは探すがABIは探さない
　　コンパイラとかライブラリを作ってる奴はABIを見る

みたいなのだと思うんですよ。まぁ、先生の要求している解答とか教科書が要求している解答を当てるのは難しいよな。

キャベチャー

宜野湾330沿いのラブめんですが、

　　キャベチャー

が登場。200円は高いが、まぁ、このご時世だからな。でも、

　　そうじゃなくて、キャベツを増やしてほしい

というか、キャベツだけで良いんだが。今度はキャベツ多めでと頼んでみよう。

Zorn の補題の Agda での証明完了

いや、3月くらいからやってて、かなり難航したんですができました。詳細はプロシンで話すので興味のある方はどうぞ。

　　record SUP ( A B : HOD )　: Set (Level.suc n) where
　　　 field
　　　　　sup : HOD
　　　　　ax : odef A x
　　　　　x≤sup　 : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -- B is Total, use positive

　　record Maximal ( A : HOD )　: Set (Level.suc n) where
　　　 field
　　　　　maximal : HOD
　　　　　as : A ∋ maximal
　　　　　¬maximal<x : {x : HOD} → A ∋ x　→ ¬ maximal < x　　　 -- A is Partial, use negative

　　Zorn-lemma : { A : HOD }
　　　　→ o∅ o< & A
　　　　→ ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B　 ) -- SUP condition
　　　　→ Maximal A

定理自体はこれだけ。HODってのが、今回使ってる Agda で実装した ZF 集合論の集合。遺伝的順序数定義可能集合(Heritic Ordinal Definable Set)ですね。

Kunen と田中先生の本には載ってるけど、ちょっとずれてる。ってことは、別な集合論の公理をAgda用に作ったわけ。

A上の単調増加関数 f x と、その閉包 FClosure A f x を与える上界関数列 supf x 、そして、それが定義するAの全順序部分集合列 UnionCF A f supf x
と、それらの性質を表す record である ZChain で、

　　全部で 1800行

nvim 上でチェックにかかる時間は5分。agda command だと6秒。なんなの。メモリは7GB。なんだが、ソースコードを工夫したら3GBに。

時間がかかった理由はいろいろあるが、最小上界でなくてもできると思ったのが間違いで、さらに、≤ な関数で fixpoint を示せると
思ったのが間違いで、まぁ、それではだめなのに気づくのに試行錯誤しまくったのがだめだったみたい。

その辺の証明を正確に追うことも可能なんですが、あんまり Agda っぽくないしな。整列集合の切片とかのあれですね。

でも、まぁ、証明自体は岩波現代数学概説に沿っているはずです。

これで、Generic Filter の存在とか、チコノフの定理とかが示せるはずです。

ブラウン管でのプログラミング

なんか学生が研究室にブラウン管持ち込んでなにやら。

　　PALとNTSCってなに?

とかやってる。楽しそうだな。

最初にプログラミングしたのは PC8001 をテレビにつなげてで、目が死にました。

自作のもテレビにつなげてて。父の工場の払い下げのを使ってたっけ。これはビデオ端子なので、それほでも。

でも、大文字小文字は反転で区別してた。そんなんで C とか良く書いてたよな。

安物モニタの方がましだったので、そっちの方を使っていたはずです。

今の 4K でのプログラミングも目が厳しい。

OIXの話

長田先生の置き土産の OIX が、Okit 経由で存在していて、琉大ももちろん接続されてます。

この辺は県が割り込んだりして、残念なことになっているらしい。

　　ネットワークの第ゼロ層の政治層の構築に失敗した

ってところですか。別に波風立てたいわけではないですが、仲良くやって欲しいところですけどね。

プログレ

最近、ヘンリー8世と六人の妻の冒頭だけ練習してるんですが、学生になんの曲ですかと聞かれたので、

　　ラウンドアバウトと、太陽と戦慄 part 2

も一緒に教えました。

冒頭はいいんだが、途中が楽譜が正しくないっぽい。いや、読めてないだけかも。

楽譜読み解って認識するアプリとかないのかな。

4回目

3回目打った後にコロナを食らったので、しばらくおとなしくしてたんですが。既に先週木曜日の話。

宜野湾体育館でがらがらでした。

効果のほどは期待してませんが。ただだしな。コロナは血管系、心不全とかにも関係する話もある。どっちかというと

　　それって長く残るの?

あたりが気になりますが、まぁ、それはこれからわかる感じか。

珍しく、少し注射跡が痛かったし、微熱な感じだった。まぁ、それでも飲みには出るんですけどね。

だから、打つ的なところもあるか。

かばんの修理

雨が降ってたし、少し重かったしな。久しぶりに、カバンの紐の金具を引きちぎってしまいました。

　　少し位置をずらして、ねじを締めなおして修理完了

まぁ、時間の問題だが、代わりのが見つからなくてな。

すずめの戸締り

観てきました。天気の子の別解みたいな感じですね。

東京の風景が懐かしい。お茶の水あたりとか。

予想外に面白かった。あの頃から、みんな成長してるはずだが...

https://suzume-tojimari-movie.jp

RAM

80年代初頭の、

　　ASCII/RAM/IO/Interface

が情報源だったわけですね。それと、Bit Inn に通ってた。

いやさ、

　　命令セットが載ってるだけで、かなりのことがわかる

わけ。RAMは、この他に Micro C が載ってるのも持ってたんですが、なくしてしまいました。

ROM Writer を当時の東工大の助手だった久慈さんが持ってたので

　　いきなり、ビデオとキーボードが付いているコンピュータを作れる

それも、たぶん、売ってるものの半額くらいで。しかも、最新のCPUとRAMで。そういう時代ですね。

それが

　　雑誌を読むだけで、可能だと分かった

今の学生には、また、違った地平線が見えてるだろうとは思いますけどね。

最近の原神

ナヒーダでて、80まで上げたんですが、90にしてから使おうと思ってたが、最後のつめでめんどくなって。

と思ったら、Wwanderer でるのか。育成楽しいといえば楽しいんだけど。

でも、TCG は嫌いなんだよ。勝手に決められたルールの adhoc さがな〜　なので、そっちはさぼる予定。また怒られるか。

FF8の変なミニゲームを思い出すな。

DNSのお話

PowerDNSは設定したんですが、まだ、運用してません。別に怖いわけじゃないんだが。

Akatsuki との設定に少し苦労したんだが、DHCP6 / KEA DHCP との接続とかもやらんとだめならしい。うーん。

ところが、

　　なんか、8.8.8.8 から見える時と見えない時がある

とか言ってるのが。え〜? ちょっと見せてみ。

　　え、なんで、Sakura 上のサーバに対して検索してんの? そんなの聞いてない

で、調べてみたら

　　BIND9の Master で NS で指定されていて、設定ファイルが9月

どういうこと? なんで、Slave じゃないんだよ。で、Slave 設定して終わりなんですが...

　　Master が死んだら Slave のキャッシュはどれくらいもつ?

とかの話が。Slave なのであって Cache ではないんですけどね。SOA Expire ってのがあって二週間くらいらしいです。

こっちの Master/Slave の用語は purge しないのか?

義母との食事

竜宮通りの店を使いました。最近は、東京の妹の家と沖縄の家で、二人で交互に一緒に住んでるらしい。

元気なのは素晴らしい。一緒にいる時間を大切にしたいです。

Roland SC55

どっかで手に入れたんだが、どこで手に入れたかは覚えてないです。たぶん、秋葉原のジャンク屋。

2000年の写真に88Proが写ってる。今のは、やっぱりジャンク屋で買ったSC55。

ガレバンとかでいいんだが、

　　切れてて再起動とかめんどくさい

なんとなく、ふっと手慰みに弾きたい感じだからな。

ちょうど、ハラカミ・レイの話をNHKでやってたみたいですね。道具は使い方だからな。

SC88というとカラオケなわけですが、その安っぽさが、むしろ、

　　バブルのはじけたあとのゴールデンリセッションな時代

に合ってたと思う。

いまだと箱な音源はもう使わないのかも。

開かれた大学

まぁ、動物園なので「危ないのを外に出さない」的な意味もあるんですけどね。鉄条網はどうなの?

立教大学は徒歩の通り道でもあるので、かなり自由に通れる。琉大も車は抜け道に使ってるな。

イギリスのケンブリッジ大は、街中にばらばらにいろんなところを借りてるので、キャンパスって感じと違う。

東工大は幼稚園の散歩場所になっていた印象がある。

東大は終電だと弥生門の横を乗り越えてたな。

建物の入り口でカードとか、あるいは、部屋ごとにとか、いろいろあるけど、

　　大学はむしろ治安を良くするので、敷地はオープン

なのが良いんじゃないかな。

PC8001の思い出

実家から回収したので、どっかにあるはずです。拡張ボードも持ってくるべきったか。

大学二年の時に友人(青柳氏)と半々で買いました。16万円。既にプロ電(fx502p)でプログラミングはいろいろ知ってた。
メモリ32KB。

買って、テレビにつなげて一晩でBASICでブロック崩し書いて「目が死ぬ」知ぬことがわかりました。
で、秋葉原でジャンクなモニタ(裸)を一万円で買ってきてつなげました。友人は嫌がってたが。

この頃はJISキーで特に問題なく。それまでBASICは店頭で動かすくらいだったはず。

で、MS20かなんかのシンセにつなげる DA x 4 + Z80 CTC + Z80 PIO + GPIB な拡張ボードを作りました。
なんだが、MS20って f/v で oct/v じゃないんだよね。なので、シンセの制御はぜんぜんだめだった。がっかり。
リズム出すくらいなら。GPIB は卒論で活躍したらしい。

CTCはROM Writer を back で動かすなんてのに使ってた。で、この上で GAME80 で 6809 のアセンブラを動かして
マイクロマウスを作ったわけだな。 32KB RAMで十分楽しかった。

もっとも、大学三年の時には自作6809の方を触ってたので、PC8001 は実はあんまり使ってない。
なので、 PC8001 の30万円のFDとか、PC8801/PC6001 あるいは MSX には縁はありませんでした。

まぁ、楽しい時代だったかな。自作が安上がりで性能が良かった時代ですね。

PC8001 ミニですか? もう十分遊んだから要らないです。