$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\hyp}{\text{-}} \newcommand{\u}[1]{\overline{#1} } \newcommand{\Ev}{\triangleleft} \newcommand{\In}{\text{ in } } `$$`/\cat{C}/ = (|\cat{C}|, \times, \to, \u{(\hyp)}, \Ev)`$ $`(\times) : |\c…

purely functional code ＝ pure code ＝ 純コード imperative code ＝ impure code ＝ 不純コード transpile to pure code ＝ purify ＝ 浄化 impure block ＝ Kleisli block impure function ＝ command impure program ＝ script impure program fragment…

$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\hyp}{ \text{-} } `$$`\mrm{K}^X_I`$ を $`I`$ 上の定数ファミリーとして、$`A`$ を任意のファミリーとする。ファミリーの射$`\quad \mrm{K}^X_I \to A \text{ on }I`$は、グロタンディーク同型により次…

罪も多い。次を混乱させてしまった。 指標とモデル圏 パラメータ付き指標とファイバー付きモデル圏 忘却射影に対するセクション（so-called インスタンス） ひとつのモデル モデル圏／ファイバー付きモデル圏のあいだの関手（構成手続き） 特に、ファイバー…

$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Within}{ \sqsubseteq } `$ $`\cat{Sign}`$ 指標の圏 $`\cat{Alg}`$ 代数の圏 $`\mathbb{F}:\cat{Sign} \dashv \cat{Alg} : \mathbb{U}`$ 自由忘却随伴系 $`J:\ca…

課題と参考文献： インスティチューションがうまく使えない - 檜山正幸のキマイラ飼育記 (はてなBlog) 2005年7月の疑問・課題 はじめての圏論 その第5歩：変換キューの圏 - 檜山正幸のキマイラ飼育記 (はてなBlog) はじめての圏論 第6歩：有限変換キューと半…

出現するたびに悪口を言っている。https://m-hiyama.hatenablog.com/entry/2020/09/07/165418 蒸し返し： アドホック多相 vs パラメトリック多相 '∀'は、もともとは記号論理の全称限量子〈universal quantifier〉の記号です。僕は、ここに'∀'を使うのは好き…

Haskellで「アクション」という言い方があるが、どうもクライスリ射のことらしい。IOアクションは、IOモナドのクライスリ射という具合に。となると、Leanのtacticモナドのクライスリ射はtacticアクションとなるが、「tacticアクション＝タクティク」だから、…

忘却ファイブレーション ＝ 指標の分割が定義する、忘却関手を射影関手とするファイブレーション パラメータ・インデキシング ＝ パラメータ付き指標が定義する、パラメータ指標のモデル圏をインデキシング圏とするインデキシング（インデックス付き圏） グ…

指標のあいだの構成〈construction〉は、ML言語のファンクタと同じ概念。引数がない構成がML言語のストラクチャ。問題は、パラメータ付き指標のあいだの構成＝パラメータ付き構成。意味論はむしろ簡単で、パラメータ付き指標の意味がインデックス付き圏だか…

型クラス＝指標の立場なら、指標Σの意味は〚Σ〛 := Mod[Σ]。そのインスタンスは〚Σ〛の対象のこと。実に素直。圏Pに対して、ΣのP-パラメトライズ・インスタンスを P→〚Σ〛と定義する。自明圏Iに対するI-パラメトライズ・インスタンスはインスタンスと同一視…

横と縦があるので、 縦方向の列＝ピア〈pier〉（peerではない！） 横方向＝フロア フロアの数＝ストーリー 次のように呼ぶのが良さそう。∈0 は「対象として所属する」。 指標Σ ∈0 リテラチャーL ターゲット圏C ∈0 アンビエントA 指標とターゲット圏から決ま…

次の列がある。 Set = Total ⊆ Partial ⊆ ND Totalは双デカルトな半環圏、NDはテンソル半加法圏、Partialはその中間のなにか。これは、ND上に積み上がった3段のパレスになっている。フレイド圏 J:C→D も埋め込みJで C⊆D と考えれば二段のパレスだ。どうもパ…

コンストラクタ＝集合コンストラクタ： 圏の対象に集合を対応させる コンビネータ＝射コンビネータ： いくつかの圏の射から圏の射を作り出す 一般的には： コンストラクタ：|C|→|D| コンビネータ：|C|→Mor(D) さらに一般的には： (n, m)-コンビネータ：|C|n→…

後で追加修正するかも。指標の一覧： 名前 提供記号 ひとこと Magma * 乗法記号使ったマグマ UnitalMagma *, 1 単位的マグマ MonoidAste *, 1 モノイド MonoidPlus +, 0 モノイド Group *, 1, ~ 群 AbGroupPlus +, 0, - アーベル群 Ring +, 0, -, *, 1 可換…

裏紙にテキトーに書いたから汚いのだが：(http://www.chimaira.org/img4/algebraic-ladder.png)いくつか間違っている： Σ3, Σ2, Σ1 は、3Σ, 2Σ, 1Σ 。 2C, 1C, 0C は、3A, 2A, 1A のほうが良かった。 下から、レイヤー1、レイヤー2、レイヤー3の代数的レイヤ…

構文論はコンピュータッド理論といえる。各次元の基本記号（セル | アトム）を決めて、基本記号のプロファイルは、下の次元の基本記号から構成される項（複合セル | ダイアグラム）で記述する。各次元の基本記号（セル）の意味（割り当て）が決まれば、アン…

プログラムfを状態変換子とみたものを f*、プログラムfを述語換子とみたものを f* とすると： < x | f*(q)> = < f*(x) | q> が成立するのではないか、これはインスティチューションの充足関係 x |= f*(q) ⇔ f*(x) |= q と同じではないか。つまり、 状態変換…

型／ソート変数（型／ソート名）は、0-項。0-生成元＝0-セル 型項は、0-項。生成された0-射 定数／変数は、1-項。1-生成元＝1セル。点射または域不定射 値項は、1-項。1-射だが、点射 関数項は、1-射。一般の射、または、フルカリー化された点射 項の構成法 …

車輪の同時発明／再発明 目眩がする - (新) 檜山正幸のキマイラ飼育記 メモ編の続きほぼ同義語： 指標 型クラス インターフェイス スキーマ 型コンテキスト 仕様 公理系 セオリー・インターフェイス 構造体型 （OBJ系）モジュール 型コンテキスト コンセプト…

なんというバカバカしさ、なんという無駄、なんという浪費！ ラムダ計算 インスティチューション 型理論 型コンテキスト 指標 型前提（域側） 大きなラムダ式 クライスリ指標射 型判断（シーケント） 大きなラムダ計算 指標圏の計算 型証明計算 レコード（値…

もっと整理が必要だが縦に見ると同義語 1-真偽値 2-真偽値 3-真偽値 4-真偽値 5-真偽値 0-要素 1-要素 2-要素 3-要素 4-要素 (-1)-集合 0-集合 1-集合 2-集合 3-集合 (-2)-圏 (-1)-圏 0-圏 1-圏 2-圏 縦に見ると同義語 1-インスタンス 2-インスタンス 3-イン…

モノイドの有限族〈finite family of monoids〉とは、圏論を使って定義すれば： Mは圏である。 |M|は有限集合である。 a, b∈|M|, a ≠ b ならば M(a, b) = ∅ このMがモノイドの有限族。モノイドの有限族は圏なので、準同型射＝関手で、終対象／始対象／直和／…