cell を使っていて良いなと思うのが、DOM 構造を変えないで Component の切り方を変えられる点。

あとから、もう少し管理範囲を広げたいとか、2個のコンポーネントを1個にしたいとか、React だったら大手術過ぎてやる気が起きないような変更も、割と簡単に出来たりする。

測度論の本に非可測集合とかバナッハタルスキの定理が出てきて、久しぶりに選択公理についてあれこれ考えてしまった。

バナッハタルスキは1個の球と2個の球という特殊な形で述べられているけど、もっと一般的な形で証明出来るはず(おそらく任意の図形が合同なんじゃないか)。そうなると、合同という言葉自体に意味がなくなって居るのではないか?

エアコンをドライにしたらちょっと寝れた。体が弱くなってる気がする。

久しぶりに測度論の本を読んだら気分がリフレッシュされて良かった。丸善、ちょっとだけちゃんとした数学の本を置いてくれてる。

趣味プロ じわじわ進捗中。とりあえず、キャラが動けて、キャラ移動に合わせて背景が動くところまで。通行できない地形に入ろうとすると押し戻される機能も入れた。

モバイル環境では4方向スワイプで方向を操作できるようにした。スワイプのセンシティビティの調節がなかなか面白かったのと、スワイプの方向をとるのに atan2 が使えて楽しかった。

cell を使って、新しい frontend の趣味プロを始めた。

2d canvas に 60 fps で色々描画するタイプのプロジェクト。main ループで取れた fps 値を遠隔地のラベルに表示するというところで、cell 制作時構想していた pub/sub パターンが綺麗にハマってとても気持ちが良かった。

capsid と capsule の後継プロジェクトとして cell を作った。

capsule の interface を組み替えてより自然な形に組み立て直したもの。関数1個を1つのコンポーネントにするというアイデアは、最近の React から拝借した。

React に限らず Solid や Qwik なんかも、1コンポーネント = 1関数というデザインを踏襲するようになってきていて、フレームワークを超えて共通のパターン言語のようになって来ている気がしたので、このデザインにしたかった。

一番実装が難しい on helper とか初回登録時のロジック部分はほぼそのまま capsule から拝借して来ているので、フレームワーク自体はほぼ1日ぐらいで完成。テストケースを追従するのにさらに1日。TodoMVC を移植するのにさらに1日ぐらいの作業量でほぼ完成できた。

TodoMVC を cell で実装してみたところ、全体のバンドルサイズが 2.38 kB になって、capsule の時よりさらに 1kB 程度小さくなった。自分が知る限り飛び抜けて最小サイズで TodoMVC が実装できていてとても気持ちが良い。

AI のサブホスティング的なサービスは基本全部はやらない気がするなぁ・・・

AI を使っていると分からないように AI を裏で使っているサービスは強そう

ただ、実際の数学の教科書の証明を見ていると「○○の定理より〜」みたいな感じで、既存の定理を推論規則として使っている場面が良くあって、定理をただコピーするだけじゃなくて、推論規則として使えるようにするみたいな仕組みもあった方が便利そうなのだけど、定理が推論規則になるっていう状況があまりきちんと定義されていないような気がする

証明を static な木として記述させるとして、証明済みの定理をどうやって適用させるかがなかなか悩ましい。一番単純にいくなら、証明済みの定理をそのままコピーすることのみを許可する方法かな・・・

NORQAIN って全然ピンとくる時計がない。その割に OMEGA ぐらいの値付けがされてて、全然理解が出来ない

Many books try to capture a proof as a sequence of inferences on statements. It looks natural at first because it is similar to how we make arguments in natural languages, but it is not natural as it looks.

If you try to formalize a proof in that way, the proof internally have to have a lot of backward references to indicate what inference uses what statements. This backward reference structure instantly becomes hugely convoluted, and it makes the proof cluttered and unreadable.

A proof should be considered as a static tree, instead of a series of dynamic operations on statements.