このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

データベース・テーブルの変更を圏論的に見るならば

【注意】2022年3月より、MathJaxまたは「はてなブログ」の仕様変更またはバグにより、MathJax/XyJaxを使った数式・図が表示できなくなりました。そのため、一部の数式・図は表示できなくなっています(ソースコードが見えます)。新しいタブまたはウィンドウ…

実用圏論: 2-圏、居住関係、プロファイリング

ここ何年かで、150分×10回で1クールのセミナーをシリーズとして行いました。話題は毎クール違うのですが、共通するテーマを一言でいえば「実用圏論」でしょう。ラムダ計算、プログラム意味論、論理、ベイズ確率論、データベース理論、システム設計などに“使…

圏論的コンストラクタと圏論的オペレータ〈コンビネータ〉 再論

「圏論的コンストラクタと圏論的オペレータ: 関手性・自然性の呪縛からの脱却」において、必ずしも関手性〈functoriality〉を持たない対応や、必ずしも自然性〈naturality〉を持たない変換を紹介しました。ときに、非関手的対応/非自然変換が多用されるこ…

ギリシャ文字が足りない(2-関手のために)

自然変換や2-射はギリシャ文字小文字で書くのが習慣です。例えば次のように:一部のギリシャ文字は、その用途が習慣的に決まっています。習慣なので破っても問題ありませんが、あえて習慣から外れたことをしたいとは思いません。内容: モノイド圏 α, λ, ρ, …

保証と要求: カリー/ハワード対応も添えて

文の種類に、平叙文〈declarative sentence〉や疑問文〈interrogative sentence〉などがあります。論理式で書かれるような命題は平叙文だと考えられるでしょう。では、論理式で書かれる“疑問文”はないのでしょうか? 不要なのでしょうか?命題をめぐる対話の…

可換モナドとラックス・モノイド・モナド(動機も少し)

「対称モノイド圏上の可換モナドはラックス・モノイド・モナドとみなせる」という事実があります。それを聞いても「あーそうですか、それで?」なんだけど、動機があって辿り着くと「ほー、そうかそうか、ウンウン」みたいな気分になります。動機・経緯につ…

過剰高次射を認めるn-圏の便利さ

本日(2022-01-17)2投目の小ネタ。 n-圏の過剰高次射と反転原理 負次元の圏と(N, m, n)-圏 上記2つの記事で、n-圏(n次元の圏)のk-射(k次元の射)の話をしました。通常の圏(つまり1-圏)の議論に高次圏は出てこないと思うかも知れませんが、そうではあり…

スタックの話: 仕様と実装とテスト

【注意】2022年3月より、MathJaxまたは「はてなブログ」の仕様変更またはバグにより、MathJax/XyJaxを使った数式・図が表示できなくなりました。そのため、一部の数式・図は表示できなくなっています(ソースコードが見えます)。新しいタブまたはウィンドウ…

負次元の圏と(N, m, n)-圏

「n-圏の過剰高次射と反転原理」は僕の雑感でした。雑感の続きを書きます。関連する記事: ファンタジー: (-1)次元の圏と論理 負次元の圏一般に、すべてのn-圏を対象とする(n + 1)-圏を と書きます*1。“負次元の圏”と言い出したのはバエズ〈John C. Baez〉…

n-圏の過剰高次射と反転原理

n-圏のなかで、nを超える次元の射の有無や性質が問題になることがあります。そのような射、つまり n < k であるk-射を過剰高次射〈excessively higher morphism〉と呼ぶことにします。過剰高次射に対する態度には次の3つがあるでしょう。 過剰高次射なんて…

モナド: 随伴系の圏の上のインデックス付き圏として

2022年あけましておめでとうございます。2022年最初のブログ記事は、10年前の話を蒸し返すかも知れない。今年中は無理だけど。 https://t.co/9GvXWUJv5a— 檜山, キマイラの爺さん (@m_hiyama) 2021年12月31日 というわけで、圏に対してその上のモナドの圏を…

等式的推論と高次圏論

圏論内で使う等式的推論を、圏論のなかで定式化してみます。等式的推論は高次射になるので、少しだけ高次圏論を使います。内容: 等式的推論 高次圏 高次圏における結合 結合の演算子記号 恒等射 2-圏の3-射、4-射 恒等射だけの圏 恒等射の計算と等式的推論 …

米田テンソル計算 4: 米田埋め込み

「米田テンソル計算 3: 米田の「よ」、米田の星、ディラックのブラケット 再論」にて: 圏の対象・射の{余}?米田埋め込みと関手・自然変換の{余}?米田埋め込みの両方に米田の星を使ってますが、これはオーバーロードです。両者はすこし別な対応です。僕は、…

ニンジャ米田の補題と本家・米田の補題

「自然変換の集合のエンド表示」で、自然変換の集合がエンドで表現できることを示しました。投稿の時間順序は前後してますが、必要な基本事項を「ホム関手とサンドイッチ結合」で解説しています。また、「米田テンソル計算 3: 米田の「よ」、米田の星、ディ…

ホム関手とサンドイッチ結合

【注意】2022年3月より、MathJaxまたは「はてなブログ」の仕様変更またはバグにより、MathJax/XyJaxを使った数式・図が表示できなくなりました。そのため、一部の数式・図は表示できなくなっています(ソースコードが見えます)。新しいタブまたはウィンドウ…

単調作用素と閉包作用素のプレ不動点

昨日の「有法則代数と無法則代数」から連想した小ネタ。 昨日の話 (記号の乱用)を圏 上のモナドとします。このモナドのクライスリ圏とアイレンベルク/ムーア圏は次のように書くことが多いです(僕だけでなく世間的に)。 クライスリ圏: アイレンベルク/…

有法則代数と無法則代数

「圏論的レンズ 最初の一歩: ストリング図を中心に」において、レンズには有法則レンズ〈lawful lens〉と無法則レンズ〈lawless lens〉があると書きました。「有法則/無法則」という形容詞を使うのは初めて見ました(レンズ以外で見たことがなかった)。こ…

disintegration は使わないほうが吉

昨日の記事で話題にした長/ジェイコブス論文の 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…

型理論が気持ちよく出来る圏とは

デカルト閉圏では、単純型理論とラムダ計算が気持ちよく出来ます。が、実用上、もう少し広い範囲の型 -- 依存型と再帰的型も扱えたほうがいいですね。依存型と再帰的型も扱えて、手で触れる感じ(あくまで“感じ”)の圏を考えましょう。内容: 実用上必要そう…

米田テンソル計算 3: 米田の「よ」、米田の星、ディラックのブラケット 再論

記法をどう取り決めるか? どうでもよさそうでも深刻に悩んでしまうのですよね。悩んだ経緯も含めて、現時点での約束ごとを記しておきます。表題に挙げた 米田の「よ」、米田の星、ディラックのブラケット の概念と記法について述べます。$` \newcommand{\Co…

理想化Haskellと忖度翻訳

Haskell風構文の擬似コードで記述された概念をデカルト閉圏で解釈してみます。翻訳の過程でけっこうな“忖度”が要求されます。内容: 理想化Haskell デカルト閉圏に対する直訳 忖度翻訳 関連する記事: Haskellの二重コロン「::」とバインド記号「>>=」の説明…

圏論的レンズ 6: 丹原/ペイストロ/ストリート随伴系

オプティックは双方向データ変換の技法ですが、抽象的定式化の枠組みとしては丹原/ペイストロ*1/ストリート理論〈Tambara-Pastro-Street theory〉が使われているようです。なので、オプティックのための丹原/ペイストロ/ストリート理論の枠組みについて…

自然変換の集合のエンド表示

レンズ/オプティックなどの議論では、エンド/コエンドをヘビーに使います。この記事では、自然変換の集合をエンドで表示することを目的にして、エンドの説明をします。当該の目的に不要なことはカットして、できるだけ短い説明にします。この記事内では、…

両側アクテゴリーとその準同型射

【注意】2022年3月より、はてなブログの仕様変更またはバグにより、MathJax/XyJaxを使った数式・図が表示できなくなりました。そのため、一部の数式・図は表示できなくなっています(ソースコードが見えます)。もし、表示できていれば、この注意書きは無視…

オプティック界隈の丸付き文字と記号の乱用

オプティックに関する文書を読んでいると、ラテン文字を丸で囲んだ記号が登場するんですよね。まず、MathJaxでどうやって書いたらいいのだろう? enclose というMathJax拡張があるので、それを使ってみます。次のようにマクロ〈ユーザー作成コマンド〉を定義…

リスト、タプル、タグ付きデータ、関数、依存関数

「依存型とΣ-Δ-Π随伴、そしてカン拡張」の冒頭にて: 「依存積型」と「依存和型」に関しては、もうサンザンだよー、あったく...[snip]...ふんとに「依存ナントカ型」って紛らわしいよねぇ。それで、「依存ナントカ型」と言うのはやめます。...[snip]...今後…

型クラスと忘却・追憶構造

型クラスの多重継承やオーバーロード解決機能を考えるにあたって、「忘却グラフに追憶スパンをアタッチする」という定式化がいいような気がします。それを説明します。この記事は“とりあえず・取り急ぎ”書いたもので、自己完結的な解説にはなっていません。…

圏の離散化、切り捨て、次元調整

最近、プライベートに という記法を使っていて具合がいいので、これについて説明します。内容: 圏=n-圏 n-離散圏と圏の離散化 圏の切り捨て 圏の次元調整 次元調整記法の使い方事例 次元を上げる例 次元を下げる例 高次元部分が不明な例 圏=n-圏単に「圏…

米田テンソル計算 2: 準備

米田テンソル計算の内容について書こうと思ったら、けっこう色々準備が必要みたい。「圏論からの準備」というより、もっとツマラナイこと、しかし無視できないことに関する細々とした準備です。記述や計算のためのツマラナイ道具(いや、ツマラナクないが)…