おいしいあられ、ありがとうございます

Cocoro あげもちらしい

昔、気に入った会社のをたまに買ってたのだが、おそらく代替わりで、かなり劣化してしまって...

ここのは、その昔のに近い感じ。

あぁ、でも、クッキー入れるのは微妙。おそらく、そういうものなんだろうな。

もちろん、箸で。

hugo

WordPress で作られたものを「安易に static に変更」したままだったりするので、

　　Perl script で HTMLから *.md を生成

いや、いいんだけどね。そこから、hugo で生成するんだが

　　学生がやると、なんか生成されないものが

なんでだ。自分で、server 上で、 apptainer hugo すると、特に問題無し。

学生の「おまかん」か。

Hugo って、生成されなくても「全然文句言わない」結構困ったちゃんだよな。

やっぱり、自分の俺俺 Markdown (Emacs outline mode)がいいかなぁ。

たこな ingress server

しつこくやってますが... 最近、サーバの調子がな。

　　れぞさしとかで、止まる

たぶん、CPU下げるとかで sleep 入れてるんじゃないかと。それで、

　　プログラムがたこなので、dead lock する

そんなところではないかと。バスに乗りながらだと、わりと致命的。まぁ、あせってもね。

あと、幽霊ポータルとか、最近は表示のバグも。まぁ、いろいろ劣化してるな。

でも、歩くモチべなので、ほどほどに頑張ります。

Bernstein の続き

相互に injection (単射)な写像があれば、bijection (双射)があるって奴です。

もちろん Agda でやるわですが、可算版の方が結構手間取った。

　　ℕ ↔　 A　→　B　→　C　↔　 ℕ

でやるんですけどね。Cの中の B を下から数えて番号を付ければ良いだけなんだが、induction するには最大値を見つける必要がある。

　　Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ
　　　　 → (fi : InjectiveF A　B ) → (gi : InjectiveF　B C )
　　　　 → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c ))
　　　　 → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c)　)
　　　　 → Bijection B ℕ

それは n 番のBが欲しければ, A の方で、n 個取って、それに対応するCの番号の最大値m を取る。すると、m以下には n 個以上のBがある。

なので、m から induction で下がっていけばよいってだけですけどね。さらに、

　　bijection を示すには、Bの個数の injection を示す必要がある

これは、数えた個数が同じなら、同じBを指すってやつだが、これがけっこう微妙。ま、面白いとも言うか。

これで、
　 List (Maybe Bool) と　ℕ との bijection

とか、

　 List ℕ と ℕ

とかを(比較的)簡単に示せます。

ゲーデルナンバーみたいなものね。

　＊　＊　＊

　 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b

本家の集合論の方も、いろいろ苦労したが、結局、教科書的な証明が良いらしい。f : A → B , g : B → A で、

　 Injection と Image を定義して、
　 C 0 = A \ Image g　に対して、g (f x) の閉包を定義して、その Union (C n) を取る

すると、C n 上では f と g が　C n と f (C n) のbinjection になり

X \ C n とf (X \ C n)　の bijection には g をその逆写像が bijection になる。

と、そんな感じ。g (f (C n ))が、g (f a) しか含まないってのは当たり前だが、だから、
g は (f (C n ) 上で逆写像があるという論法は、まぁ、面白い。


　＊　＊　＊

で、この可算版と、非可算版が関係あるんじゃないかって話ね。可算モデルを考えれば当然なんだが。

証明的には、可算の方が難易度は高い。 可算側は構成的に bijection が得られるしね。

集合側の Union (C n) を C n を必要な部分だけ計算するとすると可算側の証明に近くなる。

k8s

久しぶりに、さくらの方のサーバーを reboot したら、いくつか立ち上がらないサービスが...

　　見てみると、podman play kube を使ってる

それを、systemd にちゃんと登録しなかったと。podman generate systemd で生成できるんですが、

複数の file を生成するので、少し扱いが異なる。その部分を手でやってそのままだったとかそんなのかな。

もしかすると、手動で podman run したのかも。

まぁ、なおすのは簡単なんだが、やっぱり、k8s でやるべきなのかな。Komodor とかいうのがあるらしい。

Apple Watch のおさがり

試してみたですが、

　　MBP使うのに邪魔すぎる

電池がヘタってるので、まともに動かん。電源コード欲しい。せめて充電中に使わせろ。

朝とかにしばらくつけて、生体データとるくらいの使い方かなぁ。

もう少し「邪魔にならないところ」につけられないの? ペンダントとか見かけたが。

バスなびの続き

唐突に昔の Bookmark でもアクセスできるように。まぁ、

　　そりぁ、文句はたくさんでたろうからな

なのだが、

　　古いので出る表示と当たらしいのと差がある

昔は、そのまま復帰させた感じか。

Web access の ReST API の概念を中途半端に理解するからそうなる。

この先なるのかは謎だな。

ERROR

出掛けに、BDのコピーを入れておこうと思ったら、これですよ。ソニーのBDレコーダー

いや、なんか「消えないファイルがあるな」とは思ったんだが。

このままフリーズ。電源長押し再起動でなおったが。

中身、Linux だからなあ。ファイルシステム関係か。消えない録画とかあったから。

雷で壊れて以来だが...

最近は、いろいろさぼってる。せめて、index くらいつくれ〜

録画を、やめちゃってもいいんですけどね。

バスナビトラブル

いや、そこを Bookmark しろって書いてあるわけですよ。なのに、なんか Cookie を bookmark に入れてくる。

それでも、アクセスできるなら許すんだが、なんか reset してきた。Bookmark 全滅じゃん。


jhttp://www.busnavi-okinawa.com/mobile/(S(gbjurqykhiypmjbxg0qkwx20))/Timetable/TimeAndApproach?stationSid=6305ee7f-5c71-4004-ab5f-a08d8796d906&fromType=stationSearch

jhttp://www.busnavi-okinawa.com/mobile/(S(gbjurqykhiypmjbxg0qkwx20))/Timetable/TimeAndApproach?stationSid=599b8085-e476-404d-b692-e6a52e826898&fromType=stationSearch&qrFlag=0

これでは、なおしようがないな。どういうことなの。

検診

割とサボってる方です。なんか今回は、非接触カードとタブレットが登場してた。

　　今時物理カードはむしろださい...

体重とか血圧とか普段測ってるもの測ってもなぁ。心電図も apple watch でいいし。

意味があるのは血液検査と検尿くらいか。問診も、どちらかといえば、ワクチン戦略とかピロリ菌とかの話を
した方が良いのかも。

配られた封筒に名前が印刷されてるのに気がついたが、そんな役に立たないものよりも

　　今回の検診の案内の QRコードでも付けろ

とは思いました。予約のWebに行き着くのに、

　　メールの添付PDFのURLから、外部サービスのフォームに取ぶ

とかアホすぎだろ。PDFに入れたハーニポットリンク送りつけられたらどうすんだ?

行きつけの内科でも血液検査と検尿くらいはできるらしいんですが、

　　あんまり気が進まないらしい

その方が僕は楽ですけどね。

昔は、献血の時にいろいろ測ってもらえたんっだが。

病院にいかなくても

自分の経験でも、コロナの感染から発症はかなり早くて、翌日とかくらい。人それぞれなんでしょうけど、

　　おかしいと思ったら、家で二三日様子見る

のが正解っぽいです。

　　ワクチンも感染を防ぐものではなくて、感染後の症状をやわらげるもの

だからなぁ。若い人のは軽いことが多いけど、微妙に後遺症もあるし。

行きつけの薬局にはこんなのが書いてありました。

コロナで良くなったことの一つは

　　風邪っぽかったら休む

が常識になったことだな。

まぁ、それでもスーパースプレッダは出てしまうわけだけど。それも風邪の進化ってことか。

人類の遺伝子の多様性の低さが裏目に出てるところでもあるな。

neovim の不具合

Agda の unicode 入力のmappingが一部動かなくて、少し、ChatGPTと調べたんですが..

　　noremap! <buffer> <LocalLeader>^r　　　 ʳ

動かないのはこれ。LocalLeadr は , なんですが、,^ を入力すると、^ がでちゃう。なんじゃそりゃ。

で、わかったのは

　　Termina.app ではでない。xterm ででる
　　Ubuntu 22.04 on WSL2の xterm でもでない

さらに、

　　^v ~ すると、<S-~> とでる

それか。

　　vim ではでない。neovim だけ

なので、neovim の version の問題な可能性が高いかな。

　　NVIM v0.8.0-dev

だからな。 めんどくさいので、

　　noremap! <buffer> <LocalLeader><S-~>r　　　 ʳ

という風に work around して逃げました。

OBたちとハリーズ

あぁ、でも土曜日のハリーズのお昼って結構混むのか。時間ずらすかテイクアウトにすれば良かったな。

入れなかった人が何人か...

コロナの関係でオンラインになったところが多いらしく、結構、戻ってきた人たちがいるらしい。沖縄だったり、熊本だったり。

まぁ、

　　せめて、コネもって帰ってこい

とは言ってるんですけどね。(自分はどうなんだ

サンエーの配膳ロボット

これって名前付けてるのかな

割とちゃんと動いてますが、人が配膳する時もあります

片付けにも使われてるが、手ぶらで帰るのが普通らしい

ボタン押せっていってくるが、全部取り終わったとかの認識は難しいのかもな

お子様たちには大ウケのようです

ただ、

　　ちゃらちゃらうるさい...

まぁ、気がつかないでぶつかるのを嫌っているんだろうけど...

Perl upgrade script

brew install で、いろいろupgrade される

と、Perl のLibrary directory がずれるので、いろんなライブラリが足りない

で、twilog で探すと

　　cpm install -g DBI
　　cpm install -g Image::ExifTool
　　cpm install -g DBD::SQLite

とかあるわけですが、

　　script 書けよ

で、書いたあとに、

　　2021/9 に書いたのを見つけました

ありがち〜 brew の hook かなんかないのかな。

通行止めしたがる人たち

いや、そこは、農道みたいなもんだし、そんなに交通量ないだろ。どうせ、

　　公共事業のあれで、ちんたら工事で、休みがち

なんだろうし... 僕もそっちまで歩いていったことはないんですけどね。

まぁ、高速バス停には支障はないんだが。

ちょっと恐れてるのは、ここにインターができたら

　　高速バスが、そのインターで降りるようになるんじゃないか

ってことね。それはアホすぎるんだが、まあ、

　　不便にすることに関しては仕事熱心な人たち

だからなあ。それよりか、高速バス停の反バリアフリーをなんとかして欲しい気がするが。

もっとも、車椅子で高速バスば無理ゲーではある。

そう言えば、この間、「満車だから、次の一時間後のバスに乗れ」を食らったな。

SDGs はバスには冷たいし。まぁ、

　　バスに乗るのは沖縄現地民ではバカだけ

という意見は認めざるを得ない。

カードゲーム

原神のカードゲームなんですが、やる気でなくて放置してたら、

　　なんか、それ中心のイベントが...

英語でやってるせいもあるんだが、

　　ターンがかっったるい

やれば、それなりに面白いんでしょうけど。

コントラクトブリッジとかにはまったこともあったんですけどね。

高校時代とか妙に複雑なセブンブリッジみたいなルールを勝手に作ってやってたな。

他のゲームがでたから意図的につまんなくしてるんじゃないの?

Kea DHCP もう一回

今日は Kea DHCP を Akatsuki に接続するのを復習してたんですが、

　　なんと、kea DCHPのgithub のWikiに reservationする SQL が書いてある

んで、それをためしたらばっちり動いたんですが

This document describes a 'back-door' editing process that
may be useful, but also risky. This information is no longer
maintained. Use with caution!

とかある。え? で、前の方をみたら

the recommended REST API

あぁ、REST APIつまり、http でやれってか。そういうことなら、最初からそういって。

ってことは、REST APIの設定からですか。まだ、少しかかりそうだな。

https://gitlab.isc.org/isc-projects/kea/-/wikis/docs/editing-host-reservations

Stable Diffusion on Apptainer

ソースコード読もうとか言う話がでたので、じゃぁ、Apptainer 上で作るかっていうことなですが、割と難航

　　そもそも、pyenv 使えとかがコンテナに向いてない

作り方が良くわかんなくって、繰り返し build するのが遅い。なのだが、去年、issei が

　　apt / pip の cache server を立ててた

これが 10倍位速い。偉い。だだ、pip に明示的にオプションしないだめ。

3分くらいで生成されるのは良い感じ。

前に、TensorFlow 読んだ時には、GPUとの接続とか勉強になったっけ。今回はどうかな。

apptainer build の中で patch -R するとか、30年前にやってたような気がする。

pip もう少しまともにならないの? 走らせないと、libraryがな一定ってくるのはなんなの。

Prolog でハノイの塔

twitter で、そんな話題が。で、ちょっと書いてみました。いや、たぶん、期待されていたものとは違うんだけど。

もともと、こんな感じで

　　変数は1文字
　　リストは [a,b,c] または [X|H]

とかで、はっきりいって

　　ほとんど読めない

しかも、差分リストが普通で「プログラムの意味」とかとも関係ない。そんな残念な感じでな。

さらに、Concurrent Prolog / KL/1 / GHC / Xtal と、さらにまったく違う言語に。A'um とかもあった。

はまっていた頃は楽しかったんですけどね。

この読めない感じが良い。ちゃんと全部表示させるにはスタックを可視化しないとだめなんだが、さぼってます。

あと、入力が正しい(降順なListの三つの分割)を見ないと正しく動かないな。ま、fail するだけですが。

move10, move12 とか六種類あるわけだが、一つにまとめることも可能。でも、

　　六種類を生成する Prolog program を作って、それを動かす

ことも可能。このあたりが Prolog の醍醐味だったが...

Berestein

いや、集合論の定理の方です。 ℕ ⊆ A ⊆ ℕ なら、A = ℕ みたいなのです。(要素の個数的な⊆です)

　　List Bool
　　ℕ ∧ ℕ

が ℕ と一対一な証明はやってたんですが、Hω2 つまり、List (Maybe Bool) はどうなのと。

List A が可算なら

　　ℕ ⊆ List A ⊆ List (Maybe A) ⊆ (List A ∧ List Bool) ⊆ ℕ

って感じなので、

　　(List A ∧ List Bool) は List (Maybe A) でないものも含んでるので
　　それをのぞいて数えなおせば良い

ってことは Bernstein で証明できるはず。 なんですが、ぜんぜんできない。

そこでわかったんですが、 Bernstein って集合じゃないとだめらしい。しかも、得られる Bijection は構成的ではないらしい。

直接証明も難しくはないんだが、そこそこめんどうではある。でも、まぁ、こういう

　　構成的じゃないけど、いきなり写像の存在が言える

のは集合論のすごいところだなとは思いました。

Bernstein の方の証明もだいぶ書いてある。両方書くのは悪くないな。

宜野湾図書館そばのカレー屋さん

結構まともでした。自分が作るカレーに近い。でも、

　　やってるのは金土日の昼間だけ

まぁ、一人だから仕方ないところか

集合論の続き

OS研究会の時にうっかり手をつけてしまって。もうずいぶん長いんですけどね。

今回のお題は、sup の公理を落として、置換公理を外す。集合の上限の仮定は最小限に。

ところが、そこで直積の定義に問題があることに気がついてなおしたんだが、

　　これで射影が簡単になるんじゃないか?

と気がついて、あさっての方向に。確かにかなり簡単になって、フィルターの直積の射影とか直積の交換とか簡単に。

と思ったんだが、

　　P x Q 上のフィルターを Q x P に変換して射影を取って使おうとすると Agda が無限ループに

おっとと。で、結局、P側とQ側は二つコピペで書くことに。まぁ、簡単になったからいいかな。

いろいろ、寄り道したが、とりあえず、そっちは諦め。

macOSのLive変換

M2 MBPになった時に、新規インストールからにしたので、デフォルトがそれで。まぁ、いいかで使い始めて、

　　それほどだめでもない

ので、半年くらいは使ったと思うんですよ。でも、

　　打ってる途中で、わけわからんところをでたらめに変換するのをいつまで我慢するのか

って思ったら次の瞬間には切ってました。もう少し打つとましになることもあるのだが...

　　Live変換は書いてる途中で画面を見てしまったら負け

(あんまりいいたくないけど、キーボード見ながら打ってる人が作ってんじゃないの?)

いまだにメインは X11 xterm だったりしで、M2 で、macUIM が死んだのでどうするかと思ったんだが、

　　うっかり、anthy を動かしてしまったので、メインはそれ

これがあほでな〜　辞書の場所が良くわかんなくって。「書く」が延々でてこないとかあるんだよな。

anthy の source は、懐かしい感じの C で嫌いではないです。

mozc + fctix に移行したいんだが、なんか成功してない。