2026-08-20T23:48:00+09:00
システム設計のための数学 第四層: 不可能性と限界
何を諦めるかを定理で決める層。Riceの定理が検証を三極に分ける話、FLP不可能性とCAP、LTL合成の実現可能性、状態爆発とAlloyの小スコープ仮説。設計の最初期に参照する価値が最も高い数学。
SYSTEMONLINE / JST
FIELD NOTES / 2026
Tsuzuri
2026-08-20T23:48:00+09:00
何を諦めるかを定理で決める層。Riceの定理が検証を三極に分ける話、FLP不可能性とCAP、LTL合成の実現可能性、状態爆発とAlloyの小スコープ仮説。設計の最初期に参照する価値が最も高い数学。
2026-08-20T23:47:00+09:00
部品は正しいのに全体が壊れる問題に効く理論群。rely-guarantee推論、振る舞い部分型(後方互換性の数学)、セッション型、CRDTとCALM定理、圏論的データマイグレーション。
2026-08-20T23:46:00+09:00
精緻化とB-method、この連載の主役である帰納的不変条件、トレース同値・双模倣のスペクトラム、抽象化写像とデータ精緻化。仕様と実装の間の「正しさを保存する関係」の数学。
2026-08-20T23:45:00+09:00
ホーア論理と最弱事前条件、時相論理のsafety/liveness分離、Curry-Howard対応と型理論、分離論理のframe rule、代数的仕様と性質ベーステスト。仕様を形式言語に降ろすための語彙集。
2026-08-20T23:44:00+09:00
システム設計・大規模刷新・仕様の正しさに使える数学を四層+横断層の地図に整理する連載の序論。数学に何ができて何ができないか(VerificationとValidation)の区別から始める。
2026-08-16T04:24:13+09:00
先日 /works/ に公開した小説三本の話。一つは今まさに存在しているAIの視点で書いた。答えは固定していないので、考察を楽しんでほしい。これからはAIと一緒にアウトプットしていく。
2026-08-16T04:00:35+09:00
ChatGPT製のノベルゲームとGemini製の3Dブロック崩しを /works/ に公開。AIプラットフォームからの持ち出しに苦労した話と、公開前の監査・手直しの記録。ついでにサイト基盤をTsuzuriに移行した話も。
2024-01-17T17:25:00+09:00
大掃除で水槽の掃除をしてアクアリウム熱が再燃した
2023-12-04T17:29:49+09:00
現在二期放送中の「陰の実力者になりたくて!」のアニメが面白いっていう話。
2023-11-15T16:06:25+09:00
日常系。最近気になったことなど。