2017年に書いた「ほぼ絶滅 アンミラ」という記事にて： 現在のアンナミラーズ ウィング高輪店は、現存する唯一のアンナミラーズです。最盛期には20店舗あったということですが …。 最後のアンナミラーズだった高輪店も2022年8月31日で閉店したんですね。 さ…

指標に対する不完全インスタンス〈不完全モデル〉という概念を導入します。不完全インスタンスは、記号の乱用、オーバーロードなどの分析に使うつもりです。内容： 指標の例 指標のモデル〈インスタンス〉 無名のモデル ラベルの省略 不完全モデル 指標の例…

とある論文で、説明のためにHaskell風疑似コードが使われていました。そのひとつが次： data 0 a instance Functor 0 where fmap = ⊥ ウーム、わかる人にはわかるのかも知れないけど、ほぼ意味不明。いったい何を言いたいのでしょう？ 僕が説明します。$`\ne…

「自然演繹の再構築への道」という記事を書いたのは6年前です。それから折に触れて“自然演繹の再構築”について考えてはいますが、細部まで詰めているわけじゃないです。んで、また最近ちょっと考えている次第。上記過去記事では、「モノイド圏から多圏を作っ…

推論規則〈inference rule〉と型つけ規則〈typing rule〉の両方を含むシステムで使いやすいものがないかな、と探していました。僕が思う“使いやすい”とは： 意味論〈セマンティクス〉はハイパードクトリン。 カリー／ハワード／ランベック対応と相性がよい。…

年に2,3回、誰かに向かって同じ話をしている気がするので、ブログ記事にしておきます。$` \newcommand{\Imp}{\Rightarrow } \newcommand{\Iff}{\Leftrightarrow } \newcommand{\mrm}[1]{\mathrm{#1}} \require{color} \newcommand{\Keyword}[1]{ \textcolor{…

記事タイトルの「述語論理」は、昨日の記事「圏論的述語論理とお絵描き」で紹介した、ハイパードクトリンによる圏論的述語論理のことです。このスタイルの述語論理に関係する話題には、記事タイトル冒頭に「述語論理：」を付けるつもり。ハイパードクトリン…

圏論的述語論理の話は過去に何度かしたことがありますが、現時点での観点から大雑把に復習してみます。そして、「全称記号の導入」と「存在記号の消去」と呼ばれる“推論規則”の絵の描き方を紹介します。$` \newcommand{\Imp}{\Rightarrow } \newcommand{PPB}…

加藤五郎さんによると、米田の補題は「圏論の大黒柱」だそうです（「圏論番外：米田の補題に向けてのオシャベリ」参照）。どのくらい重要で強力かというと（「米田、米田、米田」より）： the category theorist's joke that "all theorems are Yoneda." ...…

「自然変換のためのラムダ計算」の続きです。$`% \newcommand{\cat}[1]{\mathcal{#1}} %\newcommand{\id}{\mathrm{id} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in } } %\newcommand{\Iff}{\Leftrightarrow } \newcommand{\twoto}{\Ri…

米田の補題をストリング図で描いておくと、米田同型〈the Yoneda isomorphism〉の作り方を忘れないんじゃないかと思います。$`% \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\id}{\mathrm{id} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\…

とある自然変換の計算をしていて、通常のラムダ計算の構文はどうも具合が悪い気がしました。視力がいい人なら問題ないでしょうが、老眼近視の僕には視認性が良い構文が必要です。また、ラムダ計算に図式順記法を取り入れます。$` \newcommand{\Iff}{\Leftrig…

「多相関数」って言葉が意味不明ですが、それは一旦棚に上げて、リストの長さは多相関数の事例だとしましょう。リストの長さの宣言を次のように書くことがあります。$`\quad \text{length} : \forall \alpha.\text{List}\, \alpha \to {\bf N}`$ここで論理の…

「落第」の意味は、例えば、なんかの資格を取ろうと試験を受けたが落ちて資格を取れなかった、とそんな感じです。落第厳密モノイド圏は、厳密モノイド圏になりたかったけど、公理を満たし切れずになれなかった圏です。実は、パッと見厳密モノイド圏っぽい落…

集合と写像の話をします。集合圏のごく基本的な用語・記法は使います（最初の節に説明あり）。写像のセクションと集合族のタプルを定義して、その関係を述べます。$`\newcommand{\In}{\text{ in }} \newcommand{\id}{\mathrm{id}} \newcommand{\Iff}{\Leftri…

群が「左から作用する」「右から作用する」という言い方があります。このときの「左」「右」はどんな意味なんでしょう？ また、「左」か「右」かはどうやって判断するのでしょう？ なにかを左（あるいは右）と呼ぶべき必然的根拠があるとは思えないので「約…

「ストリング図のテキスト化は何が大変か？」にて： [ストリング図のテキスト化は]大変なんです。大変でやる気になれないのですが、でもやらざるを得ないでしょう -- 低コストの情報伝達手段がテキスト化する以外にないので。 という事情で、テキスト化の方…

昨日の記事「ストリング図のテキスト化」で、「テキスト表示を使って、オペラッド結合の記述や計算をするのは、やる前に気力が萎える」と言いました。つまり、大変なんです。大変でやる気になれないのですが、でもやらざるを得ないでしょう -- 低コストの情…

僕はストリング図が大好きです。ストリング図の利用・応用の範囲は広がっているようです。しかしながら現状においては、ストリング図の作成・公開・交換は容易ではないので、テキストに翻訳してコミュニケーションに使用することになります。テキスト化が好…

https://news.livedoor.com/article/detail/22231951/ より： 古書店「まんだらけ」の社長ら書類送検 性的な「ビニ本」販売の疑い 2022年5月27日 11時19分 「ビニ本」 -- 懐かしい、久しく目にすること／耳にすることがなかった言葉ですね（事件の内容はとも…

スパイダー付き圏を定義したので、以前から使っていた描画技法の話ができますね(ニコ)。現実には存在しない射だけど、ストリング図では“射であるかのごとく”に描くと便利なもの -- 仮想スパイダーの話をします。$`% \newcommand{\cat}[1]{ \mathcal{#1} } \n…

CD圏〈準マルコフ圏 | GSモノイド圏〉やハイパーグラフ圏〈ダンジョン圏〉のように、モノイド圏の各対象ごとに与えられる特別な射達とその法則により定義されるタイプの圏を総称してスパイダー付き圏と呼びたいと思います。$`% \newcommand{\cat}[1]{ \mathc…

マルコフ圏を普及させた当事者であるフリッツ〈Tobias Fritz〉達は、モナドを備えたマルコフ圏の定義も試みています。 Title: Representable Markov Categories and Comparison of Statistical Experiments in Categorical Probability Authors: Tobias Frit…

昨日書いた記事「サーフェイス図のテキスト表現」に、少し続きがあります。$`\newcommand{\twoto}{\Rightarrow} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\In}{\text{ in } } \newcommand{\Id}{\mathrm{Id}} \newcommand{\C}{\mathop{;}} \newcomman…

最近、ラックス・モノイド関手の記述と計算のためにサーフェイス図を描いているのですが、サーフェイス図をきれいに描いて公開するのは手間がかかり過ぎて無理です。致し方ないのでテキストで表示しますが、3次元的情報をシリアライズしたテキストは、書くの…

「デカルト・モノイド関手は色々」で、デカルト・モノイド圏のあいだの関手が「デカルトである」ことは、状況依存で規準的・一意的な定義は無理だろう、と言いました。色々な状況はあるでしょうが、ラックス対称モノイド関手に課す条件で、デカルト性条件の…

「ストリング図と相性が良いテンソル計算 2/2」において： マルコフ行列／マルコフテンソルのときは、確率に特有なワイヤーベンディング・オペレーターが登場します。それは条件化〈conditionalization〉オペレーターです。条件化オペレーターもワイヤーベン…

「ストリング図と相性が良いテンソル計算 1/2」の続きです。今回は、ベイズ確率やデータベースで実際に使う記述・計算を紹介します。$`\newcommand{\Idx}[2]{ {\scriptsize \begin{pmatrix} #1 \\ \downarrow\\ #2\end{pmatrix} } } %\newcommand{\IdxDU}[2]…

ストリング図とテンソル計算については、以下の過去記事で述べました。 ストリング図とテンソル計算： クソバカ丁寧編 上記過去記事では、律儀に愚直にテンソル計算する方法を説明しました。もっと素早く計算する方法があることは記しておきました。 ここま…

「デカルト・モノイド圏のあいだの関手、そして自然変換」にて： デカルト圏をモノイド圏として定義したもの、つまり、デカルト・モノイド圏の定義はハッキリしています。が、デカルト・モノイド圏のあいだのデカルト構造を保つ関手、そのような関手のあいだ…