雑記／備忘
「双線形写像集合関手の表現可能性とテンソル積の普遍性」で、ベクトル空間のテンソル積を事例として、表現可能関手と普遍元の話をしました。テンソル積より簡単でお馴染みな例がありますね。デカルト圏における指数対象〈exponential object〉です。これは…
表現可能関手〈representable functor〉に関連して、「普遍性〈universality〉」と「普遍元〈universal object element〉*1」という言葉のハッキリした用法があることを最近知りました。「普遍性」は、up-to-isoで何かが一意的に決まる状況で漠然と使うこと…
2019年に「データベース:: 論理の使い所は」という記事を書きました。タイトルに「データベース::」という接頭辞を付けたのは、一連の記事を検索しやすくするためです。一連の記事とは、次の意図で書かれる“はずだった”記事です。 ちゃんと書こうと思うと億…
圏論的確率論の舞台となる圏にマルコフ圏〈Markov category〉があります。マルコフ圏に関しては、このブログでけっこう書いています。 「マルコフ圏」の検索結果 最初の紹介記事を挙げれば： マルコフ圏 A First Look -- 圏論的確率論の最良の定式化 マルコ…
「演繹系とオペラッド」で演繹系について述べました。演繹系を、別な側面からさらに抽象化した構造として閉包系〈closure system〉があります。$`\newcommand{\Imp}{ \Rightarrow } \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\cat}[1]{\mathcal{#1}} %…
「カーディナリティ〈多重度〉の“カラスの足”記法が分からない」において、関係のカーディナリティ〈多重度〉の説明が（僕が見た少数の事例では）曖昧・意味不明で困ったもんだ、という話をしました。その後、ER diagrams vs. EER diagrams: What’s the diff…
データベースに関する説明では、一見して理論的に見えても、その実、内容が曖昧だったり残念だったりすることがあります。例えば、数年前に次の記事を書きました。 奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか 最近、ER図に出てくる“カ…
「米田埋め込みの書き方（色々ありすぎ）」において、米田埋め込みの記法がたくさんあることを紹介しました。別名／別記法の氾濫は、鬱陶しくて面倒な事ですが、メリットもあります。それは、用途・場面に応じて適切な呼び名と記法が選べることです。今言っ…
「米田テンソル計算 3： 米田の「よ」、米田の星、ディラックのブラケット 再論」でも触れたことですが、米田埋め込み／余米田埋め込み／ホムセットの記法が色々ありすぎます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\hyp}{\text{－}}`$ $`\text…
「層化ストリング図」では、"layer"を「層」としたのですが、「層」は"sheaf"の翻訳語であり、トラブルの原因になりそうなので「層」から「レイヤー」に変更します。ただし、過去の記事は変更しません*1。で、レイヤー化ストリング図〈layered string diagra…
次の論文の内容で、僕が「面白いな」と思った点を幾つかピックアップして紹介します。 Title: String Diagrams for Layered Explanations Author: Leo Lobski, Fabio Zanasi Submitted: 8 Jul 2022 Pages: 21p URL: https://arxiv.org/abs/2207.03929 科学的…
互いに逆向きな関手のペア $`F:\mathcal{C} \to \mathcal{D}`$ と $`G:\mathcal{D} \to \mathcal{C}`$ を含むような随伴系〈adjunction | adjoint system〉の定義として、次の2つがよく使われます。 自然なホムセット同型 単位と余単位を含む代数系 “単位と…
過去2回の記事「関係（非決定性写像）に関する用語」「(続き) 関係（非決定性写像）に関する記法」で、関係の話をしました。関係の計算にはテンソル計算を使うと便利です。テンソル計算は、物理や微分幾何だけでなく、様々な場面で使える汎用的でとても便利…
前の記事「関係（非決定性写像）に関する用語」で、関係に関する用語をまとめました。既存用語の流用で、整合性のある用語法を構成できました。この記事は続きです。関係に関する記法（記号的な書き方）はどうでしょうか？ 既存記法の流用で、整合性のある記…
関係（非決定性写像）に関する用語を一式準備します。できるだけ新しい言葉を作らないで、既存の言葉を流用します。その流用が整合的であることにも注意をはらいます。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\hyp}{\text{－}} \newcommand{\Imp}{…
前回の記事「最近の型理論： 具体的・構文的なコンテキスト」にて： コンテキストの水増し規則をキチンと定式化しようとすると意外と難しかったりします。このあたりを説明するには、構文論だけではなくて意味論も紹介したほうがよさそうなので、次の機会と…
型理論では、コンテキストが必ず出てきます。コンテキストをヘビーに使う割には、あらためて「コンテキストとは何か？」と聞かれると、うまく答えるのは難しいですね。返答に窮するのは、たぶん僕だけではないでしょう。型理論の圏論的定式化のひとつである…
アンドレ・ジョイアル〈André Joyal〉の講義動画 New variations on the notion of topos をボンヤリと見てました。ほとんど分かんないのだけど、たまに簡単な話も混じります。動画51分くらいから、付点集合〈pointed set〉とファミリーの話があるのですが、…
nLabの2-前層〈2-presheaf〉の項目 https://ncatlab.org/nlab/show/2-presheaf を見ると、2-前層はインデックス付き圏〈indexed category〉の別名のようです。インデックス付き圏の定義 https://ncatlab.org/nlab/show/indexed+category を参照すると、2-圏…
圏の次元調整〈dimension adjustment〉という概念を出したのは次の記事でした。 圏の離散化、切り捨て、次元調整（MathJax数式がうまくレンダリングされないときは、ページリロードで表示されると思います。） まず前提として、すべての圏は無限次元圏だと考…
項・式など（と呼ばれる記号的存在物）の生成や操作に関連してモナドが現れることがあります。この種のモナドについて述べておきます。「構文論 vs. 意味論」という文脈で、構文機構の扱いやすい定式化が必要になりますからね。$`\newcommand{\cat}[1]{\math…
モナドに関して： モナドの単位自然変換は、成分ごとにモノ射だろう。 とか予想しがちですが、これは違います。よく見かけるモノドの単位がモノ射成分なだけです。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\id}{\mathrm{id} } \newcommand{\In}{\te…
一連のシリーズ記事（最初の記事は「最近の型理論： 宇宙と世界、そして銀河」）を始めた目的は、最近のプログラミング言語・証明支援系 Lean、Agda、Coq などが備えている型システムの背景となっている「階層化された宇宙達を備えた型理論」を調べて紹介す…
ひと月以上前（4月6日）「自然言語混じり形式証明の意味論」という記事を書きました。そこに、5つの過去記事へのリンクがあります。それら一群の記事で、「自然言語文がコメントや補足説明ではなくて、形式証明の正式な一部となるような証明記述言語が使える…
前回の記事「最近の型理論： 外部化手法のもとでのパイ型と指数型」で、次のようなことを書きました。 対象を圏の外部に取り出す方法を外部化手法〈externalization〉と呼ぶとして、...[snip]... 「集合圏と似てないデカルト閉圏に対しては、外部化手法は有…
一連のシリーズ記事として、「階層化された宇宙達を備えた型理論」について述べてきました。最初の記事がハブ記事（他の記事へのリンク集）にもなっています。 最近の型理論： 宇宙と世界、そして銀河 「階層化された宇宙達を備えた型理論」は依存型理論でも…
「依存型理論で述語論理が出来てしまう理由」において、2つの圏をもとにしてハイパードクトリンを構成する方法の概略を示しました。このハイパードクトリンは、依存型理論と述語論理のどちらも記述できる汎用的な機構になっています。銀河（型をホストする圏…
タイトルの件に関して、とりあえず概要だけ述べます。おおよそのストーリーを語るので、細部の抜けやギャップはあります。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\J}{\mathrm{J}} \newcommand{\In}{\text{ in…
記事タイトルの「最近の」は、「理論的には古くから知られていても、実用的利用は最近になって出てきた」といった意味です。さらに具体的な特徴として、「階層化された宇宙達を備えた型理論」のことです。そのような型理論は、Lean, Agda, Coq などの型シス…
インデックス付けられた集合の族〈indexed family of sets〉を単にファミリーと呼びます。ファミリーにはたくさんの同義語があります； コンテナ、多項式、（集合論的な）バンドル、ファイバー付き集合、アリーナ、メニューなど。同義語がたくさんあるのは、…
