昨日の記事で話題にした長／ジェイコブス論文の Proposition 3.10 （p.11）のそば（p.10）に次の絵（描画方向は ↑→）があります。 これを見ると、次のように思えます。 integration は同時化： disintegration はベイズ反転： 実際、integration ＝ 同時化、…
表題の事実は、長／ジェイコブスの以下の論文の p.11 Proposition 3.10 として記述されています。 Title: Disintegration and Bayesian Inversion via String Diagrams Authors: Kenta Cho, Bart Jacobs Submitted: 29 Aug 2017 (v1), 8 Feb 2019 (v3) Pages…
デカルト閉圏では、単純型理論とラムダ計算が気持ちよく出来ます。が、実用上、もう少し広い範囲の型 -- 依存型と再帰的型も扱えたほうがいいですね。依存型と再帰的型も扱えて、手で触れる感じ（あくまで“感じ”）の圏を考えましょう。内容： 実用上必要そう…
記法をどう取り決めるか？ どうでもよさそうでも深刻に悩んでしまうのですよね。悩んだ経緯も含めて、現時点での約束ごとを記しておきます。表題に挙げた 米田の「よ」、米田の星、ディラックのブラケット の概念と記法について述べます。$` \newcommand{\Co…
Haskell風構文の擬似コードで記述された概念をデカルト閉圏で解釈してみます。翻訳の過程でけっこうな“忖度”が要求されます。内容： 理想化Haskell デカルト閉圏に対する直訳 忖度翻訳 関連する記事： Haskellの二重コロン「::」とバインド記号「>>=」の説明…
オプティックは双方向データ変換の技法ですが、抽象的定式化の枠組みとしては丹原／ペイストロ*1／ストリート理論〈Tambara-Pastro-Street theory〉が使われているようです。なので、オプティックのための丹原／ペイストロ／ストリート理論の枠組みについて…
レンズ／オプティックなどの議論では、エンド／コエンドをヘビーに使います。この記事では、自然変換の集合をエンドで表示することを目的にして、エンドの説明をします。当該の目的に不要なことはカットして、できるだけ短い説明にします。この記事内では、…
【注意】2022年3月より、はてなブログの仕様変更またはバグにより、MathJax/XyJaxを使った数式・図が表示できなくなりました。そのため、一部の数式・図は表示できなくなっています（ソースコードが見えます）。もし、表示できていれば、この注意書きは無視…
オプティックに関する文書を読んでいると、ラテン文字を丸で囲んだ記号が登場するんですよね。まず、MathJaxでどうやって書いたらいいのだろう？ enclose というMathJax拡張があるので、それを使ってみます。次のようにマクロ〈ユーザー作成コマンド〉を定義…
「依存型とΣ-Δ-Π随伴、そしてカン拡張」の冒頭にて： 「依存積型」と「依存和型」に関しては、もうサンザンだよー、あったく...[snip]...ふんとに「依存ナントカ型」って紛らわしいよねぇ。それで、「依存ナントカ型」と言うのはやめます。...[snip]...今後…
型クラスの多重継承やオーバーロード解決機能を考えるにあたって、「忘却グラフに追憶スパンをアタッチする」という定式化がいいような気がします。それを説明します。この記事は“とりあえず・取り急ぎ”書いたもので、自己完結的な解説にはなっていません。…
最近、プライベートに という記法を使っていて具合がいいので、これについて説明します。内容： 圏＝n-圏 n-離散圏と圏の離散化 圏の切り捨て 圏の次元調整 次元調整記法の使い方事例 次元を上げる例 次元を下げる例 高次元部分が不明な例 圏＝n-圏単に「圏…
米田テンソル計算の内容について書こうと思ったら、けっこう色々準備が必要みたい。「圏論からの準備」というより、もっとツマラナイこと、しかし無視できないことに関する細々とした準備です。記述や計算のためのツマラナイ道具（いや、ツマラナクないが）…
ストリング図とテンソル計算に関して僕が言えること、言いたいことは「やってみてください」です。ある意味“機械的な作業”なので、やれば出来ます。ボブ・クック教授に言わせれば「幼稚園児でも出来る」（「幼稚園児のための量子力学とその周辺」参照）。も…
今回は、僕の雑感のようなものです。若干茫漠とした短い話ですが、抽象的オプティックの世界を俯瞰してみます。内容： オプティックとは何か？ オプティックの世界 最初の記事＋シリーズ目次 オプティックとは何か？オプティックは、ソフトウェアの理論・技…
