ジャズ・マイヤース〈David Jaz Myers〉が、Categorical Systems Theory のなかで、「アリーナの二重圏」という概念を定義しているのですが、なんだかピンとこない。実例を考えてみました。具体的な状態遷移系をタイト射とする二重圏です。この具体的な状態…

名前の解釈をちゃんとしよう -- と、口頭では何百回も言った気がするのですが、ちゃんと書いたことはなかったので、この記事にまとめておきます。名前を正確に解釈せずにボヤッとした印象で済ませてしまう癖を矯正するのは難しいですね。それが、何百回も言…

カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉のコンテキスタッドは、最近の記事「コンテキスタッドかぁ、ウーム‥‥」で紹介しました。依存アクテゴリーと呼ばれていた頃（2023年末）から注目はしていましたが（「依存アクテゴリーが面白い」参照）…

タイトルはダブルミーニングです。ひとつは「二重圏は面白いよなー」ということ。もうひとつは「興味深い二重圏の事例を幾つか紹介するよ」ということです。過去記事への参照をたくさん含むので、二重圏関連のハブ記事になっています。最後に、まだ触れたこ…

表題の話題については過去に書いているのですが、改めて何回かの記事に分けて書こうかと思います。過去記事を参照〈リンク〉はしますが、参照をたどらなくても済むように出来るだけ自己充足的〈self-contained〉なスタイルにします。「出来るだけ」ですけど…

古典テンソル計算は何度も話題にしていますが、不満や愚痴として僕がよく言っていたことは； 「計算の手順だけ教わって、それを機械的に遂行するのは辛い」てなことです。しかしこれは、言葉を換えると、機械的な計算手順だけでも（セマンティクスをろくに知…

カン拡張とラムダ計算の関係をはじめて意識したのは2013年のことです。以下の記事に書いてあります。 右カン拡張が、自然変換のラムダ計算における指数型らしい件 次の絵が2013年記事にあります。このとき、次のようなことを言ってます。 runは自然変換です…

「バエズ／ドーラン茂みとリントン／ローヴェア・モナド」と「多項式関手とスケマティックなリントンの定理」において、「たわ言かも知れない」「与太話かも知れない」「怪しい話」を書いていて、出来ればちゃんとした話にしたいと思っているわけです。その…

「ローヴェア・セオリーのモデルの圏と、ローヴェア・セオリーに対応するモナドのアイレンベルク／ムーア圏が圏同値である」という結果は、リントン〈Fred Linton〉が示したのだと僕は思っていました。しかし、リントンのオリジナルの論文 "Some aspects of …

指標は宣言文の集まりです。各宣言文は、順番〈位置番号〉でも名前でも一意識別できます。実用上は、（順番は覚えにくいので）名前が使われます。が、理論上は名前が邪魔になることがあるので、ときに、名前を削除する必要があります。名前の削除方法の記述…

同義語・多義語の問題について過去3回の記事で述べました。 同義語・多義語にホトホト困っている 同義語・多義語の問題（続き） 同義語・多義語の問題： タグによる修飾と分類 同義語・多義語の問題は、正確なコミュニケーションにとっては深刻な障害となり…

[追記]「論理計算のための宇宙と型 補遺」に続きがあります。[/追記]型理論と圏論の言葉は次のように対応します。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mfk}[1]{ \mathfrak{#1} } \newcommand{\In}{ \text{ in } }`$ 型理論 圏論 型 対象 型…

「指標の話： 形状の記述と形状付き集合」において、形状付き集合について述べました。よく使われる形状付き集合に球体集合〈球体的集合〉があります。球体集合達の圏の部分圏（有限な球体集合達）に対して、その構文表示を考えましょう。圏の構文表示とは、…

以下の論文、タイトルを見て興味をそそられました。が、「んっ？ 思ってたのと違う」となりました。コンピュータッドも指標も僕が知っているコンピュータッド／指標とは定義が異なるのです。が、冷静になって考えると「あっ、やっぱり同じか」となりました。…

圏のスパンの全体は、プルバックを使って圏にすることができます。スパンの左脚と右脚に制約を付けても圏を構成できるときがあります。こうして作った制約付きスパンの圏が役に立つことがあります。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}…

最近の応用圏論〈ACT | Applied Category Theory〉では、モノイド圏、アクテゴリー、二重圏、三重圏などの複雑な構造を平気で使います。このような複雑な構造を扱うときは、名前に十分な注意をはらう必要があります。複雑な構造でなくても、名前に十分な注意…

随伴系、モナド、モナドのアイレンベルク／ムーア代数、自己関手のランベック代数、ベックの分配法則などを扱っていると、こういうモノ達を系統的に組織化したい、という気持ちになります。代数的構造の組織化のためには、ゴグエン／バーストル〈Joseph Gogu…

カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉の依存アクテゴリーは、アクテゴリーと二重圏の中間にある、ほど良い感じの概念的フレームワークです（「依存アクテゴリーが面白い」参照）。まだ定義さえハッキリしない状態ですが、僕は期待してます…

“ファイバーの計算”（「ファイバーの計算 基本概念」参照）に関する一連の記事のひとつとして、木と林の話を書き始めたのですが、独立した話題として扱えるので、シリーズ記事からは外れた記事にします。木と林は有向グラフの種類のことで、現実世界の植物の…

バタニン／マークル〈Michael Batanin, Martin Markl〉のオペラディック圏は、オペラッドを定義するための道具ですが、“ファイバーの計算”を抽象化したものだともみなせます。この記事では、抽象化する前の具象的な“ファイバーの計算”、つまり集合圏の部分圏…

レナート・ベッチ／ロバート・ウォルターズ〈Renato Betti, Robert F.C. Walters〉のとある論文を眺めていて、カン拡張／カン持ち上げの記述で戸惑ってしまいました。右カン持ち上げだと記されていたペースティング図が間違っていて左カン持ち上げになってい…

ここ2,3年「二重圏がきてる」印象があります。応用圏論を牽引している一人であるイバン・パターソン〈Evan Patterson〉は今年の1月、トポス・インスティチュートのブログ記事に次のように書いています。 Lately I’ve been fixated on double categories, pur…

集合圏内のスパンに対して、標準的なファイバー積を使ってスパンの結合〈composition | 合成〉を定義できます。その結合は、行列の掛け算で表示・計算できます。$`\newcommand{\NFProd}[3]{ \mathop{_{#1} \!\underset{#2}{\times}\,\!_{#3} } } \newcommand…

この記事には内容的な記述はありません。スケマティック系関連の記事へのリンク集となります。スケマティック系の概略と目的は、「スケマティック系のために： 雑多な予備知識 // 絵図的手法とスケマティック系」に書いています。 スケマティック系 半グラフ…

ローヴェア〈William Lawvere〉は、彼の学位論文で「セオリー」という概念を導入しました。現在、ローヴェアのセオリーに対する色々な呼び名がありますが（「用語のバリエーション記述のための正規表現 // ウンザリする例」参照）、ここではローヴェア・セオ…

「スケマティック系のために： 雑多な予備知識 // Diag構成」でDiag構成について述べました。Diag構成を特殊化すると既存の色々な構成法になるので、Diag構成は、様々な構成法を包括的に扱うフレームワークとなります。また、「一般化されたファミリーの圏」…

2019年に「データベース:: 論理の使い所は」という記事を書きました。タイトルに「データベース::」という接頭辞を付けたのは、一連の記事を検索しやすくするためです。一連の記事とは、次の意図で書かれる“はずだった”記事です。 ちゃんと書こうと思うと億…

Lean（最新版はLean 4）は強力な型システムを備えた汎用プログラミング言語です。そればかりではなくて、証明支援系としての機能も同一の型システムをベースにして実現しています。AgdaやCoqもまた、型システムに基づく証明支援系／プログラミング言語です。…

ChatGPT-xのような、チャット方式の対話型AIが世間を騒がしています。確かに、現代社会に大きなインパクトを与えそうです。僕も期待に胸を躍らせているのですが、だいぶニッチな方面への期待です。今までとても困難だった“機械可読形式証明〈machine-readabl…

カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、「型理論（ラムダ計算を含む）」「論理」「圏論」の三分野の概念のあいだの精密・詳細な対応を与えてくれます。しかし、言葉はうまく対応してくれません。異なる分野の言語・文…