Reinventing Organizations

やっと読み終わりました。Kindle Paper White でお風呂でしか読まないのですすまない。

Teal 組織の細かい詳細がいろいろあるけど、自律性を中心に見るのは良いが

　　実際のビジネスの詳細

はいろいろあるだろうな。IT利用は当然だけど、メンターはうらやましいと思った。日本の会社って

　　基本放置で、文句だけ言う

的なところがあるからな。まぁ、合わない人もいるみたいな話も。

既存の組織にどうやっていれるかみたいな話もあって「だいたい反対する人のパターンは決まってる」とかが笑えたかな。

　　Teal組織の基準は利益とか数値とかの外部基準ではなくて、組織の目的に沿っているかどうかの自発的な基準

ってのは、KPIとかがうまくいかない説明にもなってるね。

Kindle Paper White、何%読んだかと出る時と出ない時があって良くわからん。Amazon KindleのUIの最低さは変わる見込みもないな。

https://www.reinventingorganizations.com

Sets な Topos

圏論の続き。Topos の定義はだいたい合っていたので例ぐらい書くだろと、Sets (関数型言語の圏)のToposと思ったんですが...

　　全然できない

Ωが要素二の集合ってのまで覚えていたんですが、米田先生のには{1,⊥}とある。でも⊥は作れないから1と同じじゃん...
nlab を見たところ Bool だと書いてある。結局、Agda 的にはBoolが良いらしい。

　　m
b →a →Ω

で、x : b で m x : a 、つまり、b の m による像が a にできるわけですが、その像に入っていれば true そうでなければ false.

ところが、その判定には排他律が必要。なるほど、Sets なToposは非構成的なのか。

m は monic ( f m ≈ g m →f ≈g )なんですが、使い所がわからなかったんだが、像とbが一対一対応するのに必要なのね。なるほど。

まだ、技術的な問題は残っているんですがなんとかできそう。Topos ま、なんとなくわかってきたかな。

きっと internal language までいけるが、もう授業が始まってしまうな。

スエズ運河のあれ

なんか活躍してる青い船がすごい。

中にボーリングマシンみたいなのがあって、ぐりぐり回ってる。

で、操縦席がレールに乗って移動する方式らしい。

絶対、サンダーバードのテーマかけて作業しているだろ的なものだな。

https://www.nytimes.com/2021/03/29/world/ever-given-suez-canal.html

久しぶりのingress operation

久しぶりにがっつりやったかも。いろいろ

　　休みは入れてましたが

Nova は実は細かいお掃除が面白いのではないか? いや、そこら辺しか役には立たなかったかも。

自分はこういう「ばらばらに分散して、あんまり会わないで協調作業する」ってのが好きではあるけど、

　　自転車とか車で回るわけではないので

まぁ、あんまり数には入ってないです。音聞きながらやるの苦手なんだが、良くなかったな。

Turing Machine の停止問題を Agda で

割とやぶれさっていたんですが、10日くらい前にふっとできました。

record HBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
field
fun← : S → R
fun→ : R → S
fiso← : (x : R) → fun← ( fun→ x ) ≡ x

diagonal : { S : Set } → ¬ HBijection ( S → Bool ) S

くらいまではできてて、List Bool と Nat` とかと戦ってたんですが、

　　S を List Bool で良いんじゃないの?

で、確かにそう。あとは、

record TM : Set where
field
tm : List Bool → Maybe Bool

record UTM : Set where
field
utm : TM
encode : TM → List Bool
is-tm : (t : TM) → (x : List Bool) → tm utm (encode t ++ x ) ≡ tm t x

record Halt : Set where
field
halt : (t : TM ) → (x : List Bool ) → Bool
is-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ true ) ⇔ ( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) )
is-not-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x )

と書き下してしまえば、Bijection を作るだけで終わりだ。

TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool)
TNL halt utm = record {
fun← = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
; fun→ = λ h → encode utm record { tm = h1 h }
; fiso← = λ h → f-extensionality (λ y → TN1 h y ) }
where
TN1 : (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y

Halt が TM である必要はない。TMのencodingのuniqnessも不要。ただ halt は bool を返すけど、
TM は Maybe Bool なので、それを変換することが必要なわけね。確かに、そう書いてある。
理解したつもりでも書き下してみると確認できて良いです。

なんで、こんなに時間がかかったのかは謎。一つは Bijection の対角線論法と halt の定義が入り混じっててて分離できなかったからだな。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/automaton/file/tip/agda/halt.agda

LINE面談

母の施設ですが、LINE面談できる。ので先週から試してるわけですが、

　　PC側のLINE.appだとカメラが使えない

ってなわざが。設定から許可するってのがでるはずなんだが。で、諦めて

　　Big Sur にOSを上げたら、使えるようになった

やっぱり iPhone とかだとちょっとね。ただ問題は

　　女性と違って話が続かない

ヘルパーさんがいた時はヘルパーさんがいろいろ話してくれたわけですが...

なんかネタ用意しないとだめかな。

まぁ、妹と不穏な会話をするよりはましだし、顔見れるのは良いかな。

なんか叔母は娘からLINE禁止令が出ているらしく、Zoomなら使えるらしい。

Photos.app in Big Sur

恒例なんだが、Photos.app の内部DBは、またいじられてしまったらしく。笑えるのは

　　% ls ~/Pictures/Photos\ Library.photoslibrary/originals
　　0/ 1/ 2/ 3/ 4/ 5/ 6/ 7/ 8/ 9/ A/ B/ C/ D/ E/ F/

80年代のパソコンじゃあるまいし。なんだよ、このセンス。この下に

　　A/AA237B42-59E4-46E5-93EF-351CF716AAB8.heic

とか置かれる。まぁ、iPhoto.app 時代のimport時のfolder名をそのまま使うとかよりはまし。

無意味にアプリ起動時に sqlite3 を lock するってのもなくなった。あれはひどかった。

sqlite3 のtableも書き換えられてしまったんですが、一応、ましな感じではある。

　　CREATE TABLE ZASSET ( Z_PK INTEGER PRIMARY KEY,
　　　　　　 ZDIRECTORY VARCHAR,
　　　　　　 ZFILENAME VARCHAR,
　　　　　　 ZADDEDDATE TIMESTAMP,
　　　　　　 ZDATECREATED TIMESTAMP,
　　　　　　　　 ....

ここから、また link script 書くのか。まぁ、できそう。

ただ、アルバムをもはや使ってないんだけど、Google Photos の方では使ってて、その情報が取れない問題があるな。

GAS と戦いたくないが...

エヴァの復習 ネタバレ編

新劇を復習してもう一度観てきました。








ま、まずは、ちゃんと終わってめでたい。初見は、その辺り警戒しすぎて楽しめなかったよ....

新劇を通してみた感想は、テレビ版旧劇を否定してない、むしろ、レスペクトする感じだったこと。

Qの不評は説明不足にあって、その反省があるのか、

　　シンエヴァは、ちゃんと説明的セリフがある

いや、でも、予習して慣れてるからそう思うのであって、普通の人はさっぱりだろうなぁ。

漫画版を含めて、実は、どれも終わりは同じという見方もできると思う。つまらないどんでん返しよりは、

　　同じことをちゃんと繰り返し表現できる

のは良いと思うんだ。宇宙規模の親子喧嘩というワイドスクリーンバロックの伝統でもある。

　　その辺りも「ちゃんと言葉にする」というのが親切

村のシーンは綾波ファンへのサービスなのか、あるいは宮崎アニメへのオマージュなのか。自分はあーいうのにはピンと来ないけど。

シンエヴァを見た後だと、Qもなんとか見れる感じ。当時のblogを見ると感想とかほとんど書いてなくて、かなり怒っていたらしい。

初号機強奪からブンター発進で、カオルくんでしょ。しかも説明抜き。ヴィレとかは空白の14年にできたみたいですが、

　　加持が重要な役割で、しかも司令官があれらしい
　　そこでブンター強奪とかやってるらしい

なので、かなり面白そうなので、そこ書いてくれないんですかとは思いました。

https://www.evangelion.co.jp/

j5 create CA374 動作せず

MBP で使ってきた USB C/Display Adaptor/Ethernet ですが、

　　Big Sur では動作しない

らしい。まぁ、2017年から使っているけど、Apple の仕打ちに耐えて動いた方か。

Anker の二千円のでも買う? Display Adaptor は最近はあんまり使わない。

遠隔授業では安定性のために有線LANを使うのがマナーだと思うので、ないは困るな。

clang とか perl とかはだいたい動いたんですが、X11のinput method の方は格闘中です。

uim / anthy かな。しかし、ソースが古い。また考古学的プロジェクトで楽しいとは言えば楽しいです。

Big Sur

まぁ、あげたんですが... とっても動かないな。

ちょっと困ったのは、X11 は動くんだが、macUIM が動かない。2014のものだからな。

どうするかは考え中です。

工学部一号館の主

だいぶ血色良い...

駐車場ができる前は、その辺でお昼寝している野犬とかいたんですけどね。

野良を敵視する人たちもいるし、まぁ、そうではあるんだが、それほど人間様が偉いのかとも思うな。

琉大だと敷地の大半は池だし、多少大目に見ても。

過疎化で僻地だと動物に負けるようになるのが、21世紀かもな〜

Functional completeness

なんか、かっこいい名前でな〜 圏 A の任意の対象 a (つまり適当な命題)を真だと仮定する、つまり、

　　x : T → a

というの付け加えるのを Polynominal A[x] っていうだけなんですが、二年前からさっぱりわからなくて。

なんだが、なんか降ってきて、別に圏Aそのままで良くて、おまけに x : T → a を使ってる部分を付ければ良いんじゃないかと。

　record PHom {a ⊤ : Obj A } { x : Hom A ⊤ a } (b c : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)　where
　　field
　　　 hom : Hom A b c
　　　 phi : φ x {b} {c} hom

でも、そうすると、A[x]を作る部分には何もしなくて良くなる(計算はhomだけな)のでだめだろと思ったんですが、A[x]があれば、

　　Functional completeness を Agda で書き下せる

で、取りあえず書いてみたら、なんか教科書通りの証明式が...

　　なんだ、それでいいのかよ!

CCCな圏をグラフに戻してxを付け加えて再構成とか書いてあったのに使わないんですか。そんなんで良いんですか。

まぁ、わかんなかったのができたのはめでたい。

うない

首里の沖縄料理屋さん。わけわからない階段から歩くと駅から近いことがわかりました。

ありがちなんだが量が多い。ので、最初から持ち帰る気ですか、そうですか。

正統と言うよりは創作系かな。まぁ、沖縄料理は一度なくなっているから自由で良いです。

元は下北沢にあったらしく、その辺の昔話で懐かしかったです。なかむら系列ね。

下北沢の地下にある高級クラブの上にあったらしい。

先週は下北沢にも寄って、変わっているところと変わってないところの両方を見てきました。

鷺ノ宮 本丸

西武線沿線でお昼ご飯どうしようかと。こういう

　　街のステーキ屋さん

って割と良い。最近は観光業界向けの良い肉が市場に出回ってるってのもある。

これで千円なら十分かな。ご飯多いんですけど。

なんか三千円のステーキもあるらしい。

中冷たいくらいのが好きなんだがな。

幸地入口バス停入口

としか呼べないものですが。 一応、残す良心はあったらしい。ただ、

　　説明も何もなし

もっとも、ここに高速バス入口とか書くと、転んで怪我して訴えるみたいな流れが見えるな。

よほど、高速バスとの乗り換えを邪魔したい人がいるんだろうけど、実際に使ってる人がいるからなぁ。

　　僕みたいな変態が...

沖縄

戻ってきました。飛行機の時間間違えて予約してたけど、

　　最近はコロナで、どんなチケットも変更可

すばらしい。でも、結構、飛行機は満杯な感じ。一応、一席あけの努力はしてるのかな。

もっと、

　　混雑しなくても、それほど頑張らなくても、通勤しなくても生きていける

そんな世の中になると良いと思いました。

いとじゅんお墓参り

天気良かった。傘持ってきて笑われました。ま、ね。

itojun に関してはいろいろ思い入れあるな。でも、今は、花と線香とお酒か。

そこにいないのは知ってるが、思い出すよりしろみたいなのがあるのは良い感じ。

お花も新しいのが刺さってて、この季節に思い出す人は多いのだろうなと思いました。

お墓参りのあとは、いつものカフェラボエムに。居心地の良いカフェは良いね。

任務完了

今日も母の施設に行って任務完了です。LINE面談に週二回の制約があるのは、

　　Pad が一台だけ

だかららしい。Wifi ないとか、どこのIT音痴が設計してるんだよ。まぁ、特に文句は言わず。顔には出てたかも知れん。

母には関係ないとは思うけどね。

東京滞在最後の明日は、早めの itojun お墓参り説があるらしい。お昼辺りかな。雨でなければ良いが。

嵐のガンダム

今日は予定なかったのでガンダムでも見に行こうかと。しかし、そこは雨男なので、

　　元町に着いたら、風速20mの嵐

でした。風があるとガンダムは動かない。まぁ、大仏拝みに来たようなものなので問題ないです。

そういえば、ICFP 2011 の時にも台風を呼んでしまったのだった。いろいろ、すみません。

母の施設

今回の目的なわけですが、日曜日にもう一度いきます。土曜日は暇なのでガンダムでも見に行くか。

お金持ち用の施設らしく、きれい。ただ、

　　コロナの影響で入居者が少ない

らしい。在宅勤務で在宅介護しやすくなったとか言ってたけど、どうなかな。まぁ、需要は、これから増える予定なんでしょう。

なのだが、

　　LINE面談

が可能らしい。らしいんですが、

　　施設にはWifiはない

(それは残念だなと思ったが)、でも、実家のWifiは確保したので、まぁ、だいじょうぶ。

今回試してみたいのだが、どうもつたわってないっぽい。ITわかってない人は、簡単につながるとか思うからなぁ。

LINE面談が可能になれば、沖縄からつなげられるからな。

なんかゴルフ場に行きたいと言えば連れてもらうオプションとかもあるらしいです。素晴らしいです。

超準解析ファン

なんか、シラバス登録しようとしたら、基礎数学なる科目が降ってきていて。どうも、

　　高校で微積分やらなかった人たちへのサポート科目

らしいです。だったら、

　　超実数でやるんじゃないか

高校の永井先生のΔxΔtの嵐がわかりやすかった。

　d x^2 / dx = ((x+Δx)^2 - x )/ Δx
　　= (2x Δx +Δx^2) / Δ x = 2x + Δx ∽ 2x

超簡単。普通に計算するだけ。最後の　∽ は「無限小に近い」あるいは「ある実数と無限小に近い」だな。

連続の定義とかも、

　f(x+Δx)∽f(x)

これだけ。lim とか、∀ε∃δとか出てこない。

まぁ、どんな風にやるのかは面白いところだけど、この辺、斉藤先生の本があるはず。問題は手元にあるかどうかだが...

超実数のモデルとかやると大変で、filter とか選択公理とかやる必要があるんだけど、

　そっちは、Agda でやると楽しそう

でも、やらないで、

　Δx ∽ 0

だけでも、かなりできるはずです。中間値の定理とか平均値の定理とかを考えてかなり楽しかった。

ついでに、エネルギーとか運動量もやると良いかも。変分もできるのか?

久しぶりの池袋

去年の1月以来か。結構、寒い... Wifi 変えられちゃったので、ちょっと困ってますが... 聞いたから教えてくれるかも。くれないかも。

かなり寒いなぁ。

飛行機とかJalのラウンジは既に通常営業でした。

まぁ、ダメなのは大都市だけだろとも思うけど、米国はそれで放置すると地方都市に広がるパターンだったので。

移動制限すればいいと思うけど、まぁ、ある程度、来ないとどうしようもないことはあるかってなところです。

でも、今日は実家の様子を確認しただけで、あんまりやる気はでず。

ライカムの高速バス停

いや、初日からは見に行かないつもりだったんだけど、

　　ライカムならIMAXでないから安いし、空いているんじゃないか?

と思ったら予約してました。大学から高速で一本だしな。

でも、ライカムからあるいて12分。でも、そこを使ってる学生が結構いるんだよな。

しばらくネタバレなしで。

Ingress subscription

Recurse 2回目で Lv.12 です。まぁ、

　　歩くモチベ(犬の散歩)

なので、課金することに。550円/月はそこそこ高いが、そんなもんか。inventry が増えるのは便利。って、

　　それだけですか

律儀に近所を壊しに来るエージェント。そういうのがないとやることなくなるからなぁ。頑張ってくれ。

Lv1ポータル量産中です。

一時期ほどはやってないが、大学の行き帰りに寄り道してる感じです。

沖銀の One time password

別に無意味に強度上げても仕方ないのでほうっっておいたんですが、

　　振込限度額を下げる

という暴挙を食らったので、しかたなく。まぁ、スマホアプリだから、くそデバイスを持ち歩くよりはましか。

なのだが、

　　アプリを install にするのは Wifi (にしてある)
　　しかし、沖銀のアプリは Wifi だと機能制限が

いや、携帯回線の方が信用ならんと思ってますが。

例の全角攻撃にもやられました。外国人なんか全滅だよな、あれ。

　　僕よりはるかに高い給料もらってるんだから、もっともまともに仕事しろ

とは思うかな。もっとも、10年後に残ってる商売なのか? 地方銀行って...

なんか、まともなところが、あれはそこに移りたいです...

原神 Adventure Rank 45

ちんたらやってるんですが、iPhone 7+ がかなり律速な...

　　World Level 5

とかなんだが、Adventure Rank 35 から上げたら、ボスが倒せなくなったので、ちょっと行き詰まってるかも。

ボスが倒せないと character の Ascend ができないので、ちょっと間違えたかなという感じです。

Adventure Rank があがると雑魚(とボス)の強さが上がるのは勘弁して欲しい。

まぁ、別に急ぐ必要もないのだが、Golden House とかもクリアできないので話が進まん。

東京 3/10-16

なんか、母の環境も変わったみたいなので。もしかするとガラス越しかもな。

　　もともと仮想的な人なので、ネットで構わないんだけど

でも、母はそういう使わないからな。

Topos 一段落

定義の直後にある N≈N+1 まで片付けたので。この後は internal language つまり型つき高階λ計算になるので戦略が異なるはず。

いつものことだが、定義が微妙にずれてて少しはまりました。夜中じゅうやってて眠い。

基本は以下の pull back で、
　　　　○ b
　b ─────→ 1
　|                           |
m |                           | ⊤
　↓       char m     ↓
　a ─────→ Ω
　　　h
　monic m に対して Subobject classifier Ω への char m
　h に対応した equalizr m = Ker m

の二つの方向があると。これで equality とか　∨　とかをなんとかできるらしいです。

char m は唯一つで、m は iso だという定義が微妙だった。

あと

　　f     g
　1 → a → a

の自然数図式の始対象を持っている(単なる for 文)ってのから、N≈N+1 がでるところまでやりました。

集合の濃度の話っぽく見えるけど、そうなのかも知れん。

一階述語論理だとこういう議論は難しいので、圏論/直観主義論理ベースで数学をする方がわかりやすい。

まさかとは思うけど、一時期中学高校に集合論が導入されたのと同じような感じで、圏論/推論が入る可能性もあるかな。

沖縄自粛解除

なんか既に飲みかいで捕まった中高生が... 沖縄っぽいと言えば、そうなんだが。

3月4月で、また増えるってのが簡単に予測される世の中だな。

宜野湾の飲み屋さんも平常営業に...

全世界的に収まり傾向ではあるんだけど、まだまだ波はくるんでしょう。

普天間宮の前の交番

まぁ、なんか街作りでやってるんですが、交番が残るのは良く見る光景ではあるな。

右側の方も何とかするのだろうなぁ。それなりの観光名所になると良いけど、コロナ後の今ではどうなるんでしょうね。

成人の日は、屋台は出てたな。