Friday 30 April 2021

普段のingress Lv.13


まぁ、お店が早く閉まっちゃうので、夕ご飯食べたあとで歩きにでるわけですが、

  酒が入って歩くとしつこくなるのがな...

運動公園まで一周見たいな感じで。途中のコカコーラの会社のポータルが

  人気のない通り

でな〜 自分で生やしたポータルなので自分がいけないのだが。2時間くらい。

でも、翌日の夜まではだいたい落とされてました。Ingress は

  暇人 vs 暇人

的なところがあるのでね。

去年の11月にRecursして Lv13 になりました。Lv16 は自分のペースだと1年以上かかりますね。

Thursday 29 April 2021

証明書解決編

もう podman かなり忘れてて、podman-compose とかの k8s もどきもあって

  復習大作戦

的な感じで。まぁ、もともと教育的プロジェクトだからいいかとは思うんですけどね。自分の。

dockder/podman には、そういう文化があって、それに乗るのが慣れない。

  atp-get で install

とかやらないのね。container のimage上で command 一発だけ的な。Docker.io から取ってきた image 信用するのか的な。

まぁ、でも、podman network を思い出したので、その network を使って podman でlegoで証明書を取れば良いだけか。

というあたりで、優秀だったOBが入ってきてくれたので、そこからは30分くらいで片付きました。

Web server を止めずに lego で証明書をとる方法もあるらしいが、まあ、いいか。

gitlab は rails に lets encrypt の support が入ってるらしい。えらい。

偉そうな SINET のジムと対決するよりは lets encrypt が良いよね。

Wednesday 28 April 2021

証明書切

よくあるアレですが。MatterMost の方は少し苦労したみたいだが、シス管が自力でなんとかしたみたい。

いや、Lets' encrypt でいいし、MatterMost はそうして片付けたらしいし、月曜日にも同じことやってた。

なのだが、Web と gitlab だめらしい。いや、コンテナ/VMの外からではだめだと思うよ。

NIIが中間証明書をrevokeしてしまうので、期限切れではなく「読めなくなってしまう」ってのがな〜

自分の研究室のサーバには「証明書なんか入れてない」ので、こういう問題とは関係ないんですけどね。

また、夜頑張るみたいです。(他人事?!)

Tuesday 27 April 2021

石鹸派です

アルコールでちょこちょことかおまじないに過ぎない感じで嫌い。

やっぱり巨大な石鹸で泡立ててついでに顔も洗う的なのが良いな。

風呂場でもボディーシャンプーとかシャンプーとかよりも石鹸の方が良い感じ。

クエン酸リンスすればごわごわしないし。

去年の今頃も石鹸がなくなるとかまったくなくてよろしかったです。

Monday 26 April 2021

すごい硬いアイス


随分前に横浜のルノアールで。なんで横浜まできてルノアールかって言うと、

  風速20mの嵐をくらったから

です。アイスチーズケーキらしいです。ナイフの歯がたたない感じ。

結構良かったです。ルノアールは、自分の年には便利な感じの場所だな。

Sunday 25 April 2021

レンタル自転車



琉大にも四月から登場したので使ってみました。宣伝皆無。やる気ゼロだな。バスの中くらいなんか出せば?

15分80円は安いとは感じないな。バスに合わせるみたいなくそな基準なのではないかと想像します。
1時間使って400円。琉大北口からキリ短往復くらい。

アプリのアカウント登録はクレカ/PayPayが必要。日本人/学生はクレカ嫌いだからなぁ。
年齢とか聞いてくるが skip 可能。登録はマイナンバーよりは簡単です。学生は無料くらい
やらないと誰も使わないんじゃないの? むしろ、逆に使うとローソンのポイントが付くとか。
エコとか言いながら発想がけちくさい。沖縄だと戦ってるのは車なんだから金かけないと。

割と色んな場所に返せるらしいけど、平均化みたいなのはやってないらしく「0台」が結構ある。
任意の場所、あるいは登録可能にするとかもありだろうな。

電動アシストだけど、1時間はそこそこ疲れる。1時間歩くより疲れる感じ。ぴーかんで出たはずなのに

 雨が降ってきた

のは笑いました。そういう雨男なので。

昼間乗るには帽子が必須か。あるいはメット。
自分は自転車とか少し危ないんだよな。周り見ない人なので。

Ingress で取りにくいポータルとかに行くのは便利。
大学内のポータルを取るには便利だと思います。車使うか普通は。

Friday 23 April 2021

ひとなべ


まぁ、狙いはわかるんですけどね。

その語感なんとかならないの? お一人様な時代が来てるとは思います。

Thursday 22 April 2021

VSCode Mathjax

Markdown にかっこいい数式が書けて、しかもLaTeX互換。でも VSCodeだといくつか落とし穴が...

  Markdown+Mathを入れれば良いが delimitor を gitlab にする必要がある
  変な小さな○が付いているボタンを押さないと preview できない
  new file してもファイル名がないから .md で save as して開け直す必要がある

macOS で backslash を入力するには環境設定のkeybordのinoput source/日本語から¥をbackslash に。

最後に、

  VSCode で backslash は¥と表示される

え、それはないでしょ? なにそれ。フォントの問題か? 自分のは問題ないぞ。でも

  表示されるだけで Mathjax 的には問題ないらしいです

面白いね。

Wednesday 21 April 2021

筋トレグッズ


まぁ、男だからな。卒業する時に研究室にゴミ捨てるのも許すよ。

週二回くらいでもいいから、筋トレ。ただ、血圧に響かない程度に。

Polynominal

Lambek/Scott の Higher order categorical logic の続き。

  Polynominal  変数として使う射x : Hom A 1 a を追加した圏Aの拡張 A[x]
  Functional Completeness x を使った推論の正規形 a ∧ b → b の unique な射ψ(x)
  internal language 集合を含む直観主義論理を表す A 上の record

で、ψ(x) が { x∈a | ψ(x) } : Hom A 1 (P a) になるってことらしい。これで internal language で集合が扱えるようになります。

結果的に全部つながってめでたいのだが、いろいろ大変だった。

  そもそも、x は A に入ってないはずだろ? しかし、x : Hom A 1 a と書いてある....
  Hom A 1 a は複数あるが、それは変数名なので同じものを指すはず
  Hom A 1 a があるとは限らないじゃん

x を使った推論は5種類しかない(証明なし)。これで場合わけする。これは data φ で表す。

本には「分解してgraphで再構成」とかご無体なことが書いてある。結論から言うと、

 record Poly (a c b : Obj A ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
  field
    x : Hom A 1 a
    f : Hom A b c
    phi : φ x {b} {c} f

という record がψ(x)に相当する。そもそも x は局所変数なので大域的に持ってはいけないらしい。

Functional Completeness は

 record Functional-completeness {a b c : Obj A} ( p : Poly a c b ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
  x = Poly.x p
  field
   fun : Hom A (a ∧ b) c
   fp  : A [ fun ∙ < x ∙ ○ b  , id1 A b > ≈ Poly.f p ]
   uniq : ( f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b  , id1 A b > ≈ Poly.f p ]
     → A [ f ≈ fun ]

で良いらしい。fun には x は関与してないし、使う時にはxは既に存在する射 Hom A 1 α に置き換えられる。

これの存在を示すのは fp まではφの場合わけで良いだが、uniq は

  f ≈ g → k f (ψ(x)) ≈ k g (ψ'(x))

が必要になる。locally smallなら単なる cong だが、そうでないと自明には成立しそうにない。特に、
ψ(x)と ψ'(x)の x は型が合ってるだけで値が同じとは限らない。これは「分解してgraphから再構成」
からしかでない。そして、それはまだ書けてない。なので、仮定してしまうのが早いらしい。
locally small からは出るので矛盾にはならない。

internal language と接続はこんな感じ。まだ正しいとは限らないが。

  select : {a : Obj A} → ( φ : Poly a Ω 1 ) → Hom A 1 (P a)

あとは、これを internal language で使うε形式に直せば良い。

 -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) → f ∙ x ≈ φ x 
 record Fc {a b : Obj A } ( φ : Poly a b 1 )
     : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
  field
   sl : Hom A a b
  g : Hom A 1 (b <= a)
  g = (A [ sl o π' ] ) *
  field
   isSelect : A [ A [ ε o < g , Poly.x φ > ] ≈ Poly.f φ ]
   isUnique : (f : Hom A 1 (b <= a) ) → A [ A [ ε o < f , Poly.x φ > ] ≈ Poly.f φ ]
    → A [ g  ≈ f ]

とすれば良い。g は変わった記号を使うんだが、k14にないので作らないと...

これを示すには、そこそこ計算が必要。CCC の計算練習みたいなものだが。型を書いてみて分かったのだが、

  εは型を持つ

なので、CCCで変換する時にεを生成する型を間違えると当然致命的。型変換 s・s ⁻¹ を挟んで途中で
切って合わせてやると良いらしい。

そこまで気がつけば、Fc の生成できました。長いけど時間がかかるだけ。これ全体がそんなものではある。

A[x]をある意味で構築できたので、coMand な関手S(a) : a ^ b → b の Kleisli 圏S(a)を考えれば普遍問題になる。
つまり、任意のA[x]がS(a)に iso になるというのが functional completeness で、それはS(a)が CCC関手である
ことを示せば良いらしい。ただ、record Poly は技巧的なので、それに使えるかどうかは謎です。

でも、とりあえず、これで、Polyniominal 圏、Functional Completeness、Internal language まではつながりました。
まだ、直観主義論理の公理はチェックしてないけど。CCCのは成立するので集合分、つなり、fuctional completeness
の確認作業になるはずです。

https://github.com/shinji-kono/category-exercise-in-agda/blob/master/src/Polynominal.agda

Tuesday 20 April 2021

猫バス


あの、そんなに広く開けちゃうと、猫は気に入らないんじゃないかな。

キーボードの横には箱を置いておくと、キーボードに乗らないっていう説を聞いたけど、実践してません。

Monday 19 April 2021

お医者さんのはしご

といっても、歯医者さんのクリーニングはお布施だし、血圧の薬は税金みたいなものだな。

バスで両方にと思ったのだが、午前中って

  内科は割と混む

そうね、お年寄りは早いのだった。なので思う通りにはいかなかったんですが、任務完了。

最近、体重を維持できてるせいか、血圧も低め。そもそも、お医者さんだと低めな方だし。

あと気温かな。寒いと上がるね。80-140 くらい。

-

Sunday 18 April 2021

カセット



まだ、普通に売ってるんだよね。ありえんだろって思うけど。一つは、

  デザインの敗北

だと思う。最新機器、スマホとか録音機のUI設計がカセットに負けてる。

  大きくてわかりやすい

を捨ててしまったからか。たまに、

  昔のソニーのラジカセ (CF-1500 とか)

を使ってみたいなとは思います。カセットは捨てられちゃったけど。

回収することは可能だったし、iTunes に取り込む機材と時間がなかったわけではないのだが、

  なんとなく、もういいです

的な感じで。カセットの生録は割と黒歴史だしな。生々しくて。

Saturday 17 April 2021

ゆいレール作業所


ここに停まっているのをみるのは割と珍しい。

中途半端な屋根が謎ですが、工事費削減かな。

Friday 16 April 2021

最後の発掘




この前から残っていた VHS の最後のですが、総情センタに用事でいったら

  いろいろ古い機材が置いてある VHS/DVD とか VHS/DV とか

VARDIA とか懐かしすぎるんですが。しかも、ちゃんと動く。ところが、

  もはや、HDMIでないディスプレイがない

ふふ。こんなこともあろうかと、Video/S端子なディスプレイがあるのだ。

なので、わざわざそれを持ち込んでダビング。

  「ディプレイ置いておく? 他の人が使えるように」

まぁ、それはお断りだったのでディスプレイは回収。VHSも無事HDDに収納できました。

ま、ものは大したことないんですけどね。

Thursday 15 April 2021

基礎数学

というと、あの岩波の基礎数学の苦い思い出が...

蓋を開けてみると

  受講者は一人!

なくなるのかなと思って「登録しなくても受けていいよ」と言ったら三人に。

1から勉強するというのはなんか魔法な感じがあるね。

初日は

  gitlab の README.md に Mathjax で数式を書く

だったんですが、それで一杯一杯だな。そんなものです。

まだ全然できてないが...

https://ie.u-ryukyu.ac.jp/~kono/lecture/basic-math/math01/lecture.html

Wednesday 14 April 2021

歯医者さん

1年くらい空いたかな。詰め物少し空いたかなと思ったけど、そんなことはなく。

なんか新しいCTが。なのだが古い方が大きく映るので使いやすいらしい。で、

  あ、ここ虫歯ですね

げ。先生、見落とし多いんじゃないですか? ま、僕は

  医者は少しやぶの方が好み

なので。今時は麻酔も削る道具も詰め物も便利なものが多い。光凝固で1時間も掛からず終了。

神経に引っ掛からなかったし。前回はブリッジで引っかかってさっさと神経抜かれたのだった。

来週クリーニングで終わりみたいです。

Tuesday 13 April 2021

体重

Omron の体重計を使っているんですが、アプリが最低で... データを抜き出すことさえできない。
この手のもので直接サーバに通信するのやめて欲しい感じ。せめて有線で抜き出せるとか。
アプリのスクロールを動画で撮って画像認識で抜き出すってのを考えたんですがやる気ゼロです。
アプリ変わるみたいな話なんだが...

もっとも、この間の胃酸過多(2/10)で60kg/166cmになったので、お昼ご飯控え目 + 筋トレで
それを維持できている感じ。
まぁ、筋トレはたいしてやってるわけでもないので関係しているとは思えないです。

筋トレ頑張りすぎると血圧のせいか気持ち悪くなるので、そこまではやらないという対処なので、
負荷が足りないんだろうな。

Sunday 11 April 2021

数学の授業の準備

二桁の足し算からやる授業ですが、だいぶ資料は進んで、整数、有理数、多項式、そして、

  方程式

と。で、その解を作るのに原子根で代数的拡大すると複素数が入るってな感じですね。

方程式の解を作るのに数を拡張していくってのは面白い。どっかの本にもそんな解説があった。

Wolflam alpha に方程式を解かせるみたいな課題もだそうかと思ってます。

超準解析も順調だが、積分は区間の無限分割をやらないとだめなのか。natural extension? え〜

でも、そこが終われば微分方程式の解として不定積分やって、exp/sin を級数でだして終わりかな。

もちろん、いろいろ足りないが... 教科書は分厚いから。

Saturday 10 April 2021

黒いパネル


そういうの見ると液晶Displayっぽい。まぁ、なんか表示しておいても良いかな。

写真スタンドみたいな感じで。でも、いざ、点いてると

  うっとうしいと感じる気がする

消さないといけないし。スマートスピーカーは導入してないんだが、

  それも、うっとうしいと感じるかもな

特に大きなDisplayを普段どうするべきか...

Friday 9 April 2021

Internal Language


圏論の続き。竹内外史先生の層圏トポス、Lambek/Scott の Higher order categorical logic の
両方の中心的なところ

  圏のトポスから直観主義論理を導出する

ってところですね。やっとここまで来た的な。ところが、Lambek ではInternal Language は1 page。

これが難い。そもそもAgdaは直観主義論理なので、自分自身を書くようなことになる。万能Turing machine
みたいなものだが、気をつけないと書けなくなったり、逆に変数を番号で表して詳細を展開するような羽目に。

論理をdataで構文木に展開したりするとかなり大変。竹内先生の方ではそうしていて十数ページ。なぜ、

  1 page に収まっているのかが謎 definition 3.5

でも「型は圏A/Toposのそれ(対象)」とか書いてある。ToposはCCCだしN(自然数)も入っているので
* 0 Sn <a,b> はそれをそのまま使って良いんじゃないか? 残るは三つ。a=a' と a∈αはそこに書いてある
ように射を組み立てるだけでできた。 要するに直観主義論理の要素を圏Aの射に変換するだけなので、
マクロみたいなパターンで書いて良いらしい。

これは簡単。つまり、Topos と同じで、CCCな圏に射を付け加えるrecordとして inernal language を作れる。
これだと、Topos <=> Internal Language は、ほぼ対等になるのでよろしい。

問題は最後なんですが

{x∈a|ψ x} is λ (x∈a) →ψ x , the unique arrow α : 1 → P a such that x∈a ≈ ψ x

ってなんだよ。その the ってなんですか。ψ x ってなんだよ。で、さっぱりわからない。なんですが、
そのページの上の方を見ると、「λ (x∈a) →ψ x」がそのままある。そこか。

この前、格闘した Functional Completeness を使うとある。ところが前にやったのは割とインチキでなぁ。
そのままでは使えない。要するに、「λ (x∈a) →ψ x」なので x : 1 →a (aの要素を一つ指し示している射)
は引数(仮パラメータ)なわけだ。でも、x : 1 →a は仮定なので圏Aにあるとは限らない。なので、
A[x] とか coKleisli圏とかの工夫が... 層圏トポスの方だと別なものを使ってる。でも、ヒントが。

そうか、ここで使える用に Functional Completeness を仮定してしまえば良い。それを実際に証明できる
かどうかは後回しで良い。

結果的にはかなり短くできたみたい。使えるかどうかはこれからだな。

record InternalLanguage (Ω : Obj A) (⊤ : Hom A (CCC.1 c) Ω) (P : Obj A → Obj A)
: Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
field
_==_ : {a : Obj A} (x y : Hom A (CCC.1 c) a ) → Hom A (CCC.1 c) Ω
_∈_ : {a : Obj A} (x : Hom A (CCC.1 c) a ) (α : Hom A (CCC.1 c) (P a) ) → Hom A (CCC.1 c) Ω
-- { x ∈ a | φ x } : P a
select : {a b : Obj A} (α : Hom A (CCC.1 c) (P a) ) → ( (x : Hom A (CCC.1 c) a ) → Hom A (CCC.1 c) Ω ) → Hom A (CCC.1 c) (P a)

Thursday 8 April 2021

中学校の時計





バス停の目の前にあって、微妙に便利だったんですけどね。壊れちゃって。

でも、この仕打ちですか? 公共の建物でしょ? 景観とあるじゃん。

  その貧乏くさいの、なんとかならないんですか?

Wednesday 7 April 2021

Mathjax の続き

自分の授業のページは、Emacs の outline mode から生成してます。流行りのMarkdownだが、

  自分の方が早い

と思わなくもない。でも、Mathjax は入れんとあかんのか。自分勝手なのだから自分で直すしかない。まぁ、

  </script>
  <script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
  <script type="text/javascript" id="MathJax-script" async
   src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
  </script>

を入れるだけらしい。たぶん、Browserでキャッシュされるんだろうから、そんなに重くないだろう。
とは思うが、年寄りなのでなんか残念には感じる。だからといって使っているかどうか判断するのを入れるのもな。

これだけで動いたみたい。

Facebook でも、\(a^2+b^2=c^2\) ぐらいでてもバチはあたらないとは思いますが。

Tuesday 6 April 2021

代数学の基本定理

n次方程式には必ず複素数面上の解があるというガウスのあれですね。1年次の授業用になんかあるかなと思って。

5次方程式には代数解がないというガロアのと重なって大惨事。なんて事件も。

自分の好きな証明はシュワルツに載っていた

 (1) 零点がなければ逆数を取ると全域で有界
 (2) 全域で有界なら定数関数と一致

なのでで矛盾ってやつです。(2)は最高次の係数が0でなければ、どんどんでかくなるはずなので割と自明。

なので、3Dグラフでガウス平面上の関数を表示すると、x³+ 1 の三つの零点が見えるんじゃないか?

と思ったのだが割とめんどい。|(x+yi)³+ 1|だけど... いやでも、1年次が面白がってやるかも?

Monday 5 April 2021

j5 374 復活

BigSur update で使えなくなっていた j5 なんですが、代わりのものを物色してたら

  SIP切れば昔のdriverが入る

ってな記事を見かけて。Driver入れ直しはやったんだけど、そういえば、BigSur install したから

  ばっちりSIPが再設定されてる

Recovery mode から csrutil disable の driver の再インストールで、セキュリティでの許可を入れて再設定

  ばっちり認識しました

もう、一日の仕事終わった気分だよ。やっぱり、無線LANの Zoom は不安定だからな。

まぁ、これも使えなくなるのは時間の問題だとは思います。

Sunday 4 April 2021

BDのケース

そろそろ録画もやめちゃえ的なところもあるんですが、録画の整理の季節。

エレコムの48枚ケースを愛用してるんですが、ある日、Goodwill から消滅。どうも、

  不織布ケースはメディアに跡が付く

とかいうblogを書いた奴がいるらしく。そういえば、HD-DVD陣営はBlu-rayは記録域が浅いから弱い的な主張をしてた。

で、Blu-ray側は硬度があるから大丈夫的な反論で。まぁ、もともとケースとか流用できるからCD/DVDと同じ大きさなわけですが。

で、その後、エレコムはBD用と称する「不織布の目の細かいケース」を200円高で発売(30%くらい高い)。なるほど。

でも、Goodwill で復活することはなく。ま、そうだよな。狙い通りだったんですかね?

ま、水平に積んで圧力かけるぐらいでないとな。もっとも、そんなことすればDVDでもだめなわけだが。

もともと縦におけば問題ないし、DVD-Rの信頼性の低さの方が問題。Blu-rayもたまに「スピンドルごと不良」を喰らいますが。

最古のDVDが2005くらい? BDは2010からかな。特に問題ないかな。どっちかっていうと

  多重音声がレート変換で落ちる

って方が困ってて、それが原因でスカパー使っていたんですが、スカパーも多重音声軽視なのでやめてしまいました。

で、そろそろ録画もやめちゃえになってきてるわけだな。

Saturday 3 April 2021

 数式を書くには...

1年次向けだからな。Renderingがいるってのがネックなんですが、

  gitlab 上の Markdown

が良いんじゃないかと。そう言われ見ると、自分の使ってる Emacs Outline にはそういうの入れてない。

自前勝手ツールの悲哀だな。ま、markdown に降っても良いんですけどね。

  athjax example
  ===

  third
  ----

  This math is inline $`a^2+b^2=c^2`$.

  This is on a separate line

  ```math
  a^2+b^2=c^2
  ```

https://gitlab.ie.u-ryukyu.ac.jp/math/basic-06/e215799/-/blob/c79b278ea044b2603acf6db788efd220c2414d95/m01/ex01.md

Friday 2 April 2021

新学期

なんか新しい授業が入れらちゃったけど、学生に数学の問題解いてもらうくらいらしい。

今の学生の数学能力は英語の能力と同じくらい怪しいからなぁ。二桁の足し算から始めようかと思ってます。

MathJax? それもいいかな...