香港

牧港にあるお店ですね。割と軽い感じ。これでお粥とか亀ゼリーとかあれば。ないんですけど。

看板がちょっと面白かったので。チキンにしましたが量は日本人向きか。

この前から妙に役に立ってるケーブル

RD-Z1 片付けた時に、かなり捨てたんですが、

　　ま、一本ずつ取っておくか

で置いてあったケーブルが妙に役に立っている。まぁ、これが最後だろうけどな〜

テレビ側に端子があるのがすごいといえばすごい。

信号生成も楽なので、自作派にはうれしいものだったが。

いまはラズパイにもHDMI付いてるからな。

Sony BDZ FBT1000

そろそろ4K BDレコーダ欲しいかなと思っていたのでカタログは持ってたんですが、ソニーにこだわりはないが、移行は楽だから。

カタログは女性モデルの「お前は80年代から進歩してないだろ」的なもの。もっとも、80年代は、もっとメカとデザインを表に出してたか。

もはや、BDレコーダとかは世界的には衰退しててガラパゴスなものなんだよな。実際、

　　BSアンテナは生きていて、画面は映らないが録画は進んでいた

ってのを発見してなければやめてたかも。でも、なんかこう

　　録画整理する楽しみ

ってのあるじゃん。自分たちの世代には。

クロスバーはPS3からだったと思うけど、割と使いやすかったが大分前に廃止。でも微妙に残っているっぽいぞ。

リモコンの機能はほぼ同じ。SKP75は2011年なのに。ただ、

　　チャプター分割のボタンが廃止

ならしい。これは残念だな。いや、最近は、CM切りもめんどくてあんまりやってないんですけどね。(少しはやってる

でもレスポンスは良いです。10年差があるからな。　

自動録画は SKP よりはまし。SKP は「アニメギルド」とかあると、それに引っ張られてしまうっていう欠点があって...

画質は、まぁ、あんまり関係ないよね。4Kはまだ見てません。HDMIはAVアンプの方が4KはOkなんだが、なんかの新しい規格に追随してなくて

　　HDMI三本つかって平行配線しろ

とかあるが、やんないよね。やらないだろ?

何回もしつこく書いてるが、スカパーが字幕焼き込みしなければ、まだ取っていたと思うんですよ。そして、

　　Amazon Prime は字幕焼き込み

ってのを発見したしな。なんかそういうのを強制している人たちがいるの? Netflix は、まだがんばってるが、そのうち字幕焼き込みになるの?

やっぱり、米国アカウント欲しいかなぁ。

オープンキャンパス

ごたぶんにもれず、オンラインで。いやさ、

　　オンラインだと、リアルタイムでは観ないだろ?

自分だったらそうだからな。なので、動画も作っておこうとシス管には言ったのですが

　　オンラインの時に動画流すだけ

にしろと言ったつもりはなかったのだが。最近の学生は合成音声ですまして、それで良いと思うのだろうけど、

　　それだとライブ感に欠ける

と思うんだよな。オンラインで見るなら、その面白さみたいなものがあった方が。

二回目は動画にコメント入れてもらいましたが、そっちの方が良かったかな。

ゲーム班の方は、毎年学生に準備してもらうんですが、今年は油断してて忘れてました。

何となくやらんでよいだろと思ってた。ま、そういうわけにもいかんか。なので自分でやることに。

　　それもいいかな

午前午後で20人20人ですが、録画を見てくれる人がいれば、まぁ、いいかなくらいです。

例年だと結構人が来てたが...

雷の後始末の続き

結局、SonyのFBT1000を足したんですが、

　　まさかと思った、ビデオ端子から画面が見れた

ので、BD経由で録画の取り出しは可能。いや、手間が増えただけな気もするが...

新しいのは例のクロスバーUIをやめたやつね。中身は Andoroid?

D端子とHDMIで画面が出ないってことは、著作権関係の回路が飛んだってことかもな。

ちなみに新しい機材はビデオ端子なんかないんで、そういうわざは使えないみたいです。

お引越しダビングなるものがあるらしいが、2014以降か。SKP75は2011だからな。

超準解析を Agda で

うっかり書き始めてしまったわけですが、わりと順調。

超自然数は

　　HyperNat = ℕ → ℕ

整数は差を取れば良い。

　　data HyperZ : Set where
　　　 hz : HyperNat → HyperNat → HyperZ

で分数と。

　　data HyperR : Set where
　　　 hr :　HyperZ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR

等号とか不等号の決定はTrichotomous は排中律な仮定になるわけですけどね。

　　record _n≤_　(i j : HyperNat ) :　Set where
　　　 field
　　　　　≤-map : Bijection ℕ ℕ
　　　　　≤-m : ℕ
　　　　　is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (fun→ ≤-map　k)

ってな感じか。これで、できそうなんですが、

Transfer principle ってのがあって「実数で証明できる性質は、超実数でも証明される」ってのがあるらしい。

確かに、自然数から上の方法で分数まで作って体になるので、そうなるんだが、それ自体をどう Agda で書くのかわからん。

　　transferN : ( p : ℕ → Set ) → HyperNat → Set
　　transferN p n = (k : ℕ ) → p (n k)

　　transfer : {R H : Set} → ( p : R ∨ H → Set )
　　　　 → ((x : R ) →　p (case1 x) )
　　　　 → ((x : H ) →　p (case2 x))
　　transfer {R} {h} p rp x = ?

ってなのを思いついたが、それで通るのかは謎だな。

David Byrne's American Utopia

沖縄では二週間だったらしく。油断してたら最終日。がらがらってほどではないくらい。

Talking heads は90年代に良く聞いたわけですが、NYダダイズムとか呼ばれてた時代ですね。

今回のライブ映像は

　　裸足なグレースーツで、ちんどんやっぽいステージ回し

で、面白かった。裸足だと結構怪我するが、サポーターみたいなのをつけてた人も。

予習はしなかったんですが、知ってる曲の方が多かったな。ってことは

　　40年間同じことやってたのか

ま、おじいちゃんがんばってるねと、自分に言いたい感じなものだったかな。

70年代の Stop making sense も良かったが、録画持ってるだろと思ったが持ってなかった。

手に入れても良いかな。

https://americanutopia-jpn.com