…で無料な木 型クラス述語とイプシロン型 結局、指標と仕様の明示的な区別は設けずに、指標の拡大〈拡張〉を使うのが融通が効いて便利だと思います。そのためには、指標の圏には拡大〈extension〉をサポートする構造が必要になります。包含構造を持つ指標の圏等式的関手インスティチューションでは、指標は有向グラフ、またはパス同値関係の集合を追加した有向グラフだと具体的に定義しています。これは具体化し過ぎでした。カバーできる範囲が狭すぎるし一般化もできないし ‥‥ ここはある程度抽象的に…

…方法で作った多圏（「述語論理： 様々な多圏達の分類整理」参照）だとします。以下のような“基本素子”、あるいはスパイダー（「述語論理： 様々な多圏達の分類整理 // 補足：スパイダー」参照）を含んだストリング図をデカルト・ストリング図〈Cartesian string diagram〉と呼ぶとして、デカルト・ストリング図は多圏 $`\mrm{Poly}(\cat{C})`$ の多射〈poly {morphism | map | arrow}〉を表します。 名称 象形文字 対象ま…

…く引用するのですが、述語論理の話ではマズイことになります。どえらく誤解されるリスクがあります。述語論理とは、“不定の主語”を扱う論理です。“不定の主語”を扱わない論理は命題論理です。僕は、命題論理と述語論理という分類に意味があるとは思えないのですが、広く採用されている分類ではあります。 述語論理では、主語が不定な（具体的に確定はしてない）文も命題と考える。 命題論理では、主語が確定している文しか命題とは考えない。あるいは、そもそも主語・述語なんて分解はしないで“ひとかたまりの…

…イド多圏（簡約版） 述語論理： 様々な多圏達の分類整理 モノイド圏から多圏を構成する場合は、対称性がないとキビシイので対称性を仮定します。ストリング図で見ると、対称性があるとは、ワイヤーの交差ができることです。$`A, B`$ の交差を与える射を $`\sigma_{A, B}`$ と書きます。$`(\cat{C},\otimes, I, \sigma )`$ を対称モノイド圏とします。対称モノイド圏から作られた多圏 $`\cat{P} := \mrm{Poly}(\cat{…

…加群はプロ関手 Diag構成の変種とその書き方 圏スタンピング・モナドの代数は前層／余前層 ローヴェア・セオリーとその周辺 亜群上の豊穣複グラフ： 豊穣化・基礎強化の例 亜群をベースとする圏類似構造： コステロの事例 昔の記事 単純平面タングルとカウフマン図のキャンバス・基準点について 平面タングル、空間タングル、ブレイドなんかが“もつれた”話 モノイド圏上のテンプレート・オペラッド：具体例とソフトウェア的解釈 オペラッドと型付きラムダ計算 述語論理： 様々な多圏達の分類整理

…呼びます。過去記事「述語論理： 様々な多圏達の分類整理 // ワイヤリング規律による分類」では（少し状況が違いますが）、ナロー多結合〈narrow polycomposition〉、ワイド多結合〈wide polycomposition〉という言葉を使っていました。過去記事での「ワイド」の意味は、任意の部分結合〈partial composition〉に意味ですが。ある条件のもとでは、単純結合によるオペラッドの定義とフル結合によるオペラッドの定義が同値になることを示せます。し…

…： ファミリーの圏 述語 ファミリーの圏の変種： 逆向き ファミリーの圏の変種： 写像に条件を付ける シグマ共変関手 パイ反変関手 まとめ ファミリーの圏ここでのファミリー〈family〉は、集合のインデックス付きファミリー〈indexed family of sets〉です。ファミリー $`F`$ は次のような写像です。$`\quad F: I \to |{\bf Set}| \In {\bf SET}\\ \Where I \in |{\bf Set}| `$$`{\bf…

…で扱われています。 述語論理： 様々な多圏達の分類整理 ガーナー／フーショウィッツの論文： [GH15] Title: Shapely monads and analytic functors Authors: Richard Garner, Tom Hirschowitz Submitted: 18 Dec 2015 (v1), 10 Oct 2017 (v3) Pages: 52p URL: https://arxiv.org/abs/1512.05980 細かいこと 向…

…テムスキーマ」という言葉はソフトウェアに寄り過ぎなので、呼び名を変える可能性はありますが、SSモナドが重要であることに変わりはありません。そしてそれから図式的手法に関する今までの記事で、不明瞭だったと思える幾つかの点について補足しました。枠組みだけの議論では面白くないので、具体的なインターフェイス付き圏を定義して、SS構成により新しいインターフェイス付き圏を構成する例が欲しいですね。インターフェイス付き圏として述語〈predicate〉の圏が、論理との関連もあり面白そうです。

…晰な記述のためには、述語論理をけっこうヘビーに使います／使うべきでしょう。なので、論理を勉強した人にとっては、データベースは、論理を実践的に応用する練習素材としてうってつけだと思います。この記事では、「データベース:: テーブルのキーって何なのよ？」で定義したテーブル構造をもとに、データベースの数理モデルであるデータベース構造を定義します。また、正確な議論のために、幾つか用語・記法も導入します。ところどころに補足を入れています。飛ばしてもかまいません。圏論／型理論の予備知識が…

…である」という意味の述語〈predicate〉を $`\text{isSuperkey}_{(C, S, \Gamma)}(X)`$ と書くことにします。この述語は次のように定義されます。$`\For X \in \mrm{Pow}(C)\\ \Define \text{isSuperkey}_{(C, S, \Gamma)}(X) :\Iff \\ \quad \forall T \in \Gamma.\, \lnot \exists t, t'\in T.\\ \qqua…

…す（多圏については「述語論理： 様々な多圏達の分類整理」を参照）。演繹系の利用場面は、「推論」「導出」と呼ばれるような操作を持つシステムの共通構造を粗視化して眺めたいときです。具体的な詳細や一部の構造を捨ててしまえば、演繹系の枠組みで捉えられることは多いでしょう。 *1:生成系がやせていても、それから生成された複圏〈オペラッド〉がやせている（複ホムセットが単元集合か空集合）とは限りません。 *2:この条件は、スパンに対する jointly monic 条件です。 *3:証明ツ…

…積をもつ多圏です。「述語論理： 様々な多圏達の分類整理」に書いたように、「プロップ〈PROP〉 ＝ 対称・モノイド・ワイド多圏」です。"PROP" は "product and permutation category" に由来します。対称・モノイド・ワイド多圏は対称厳密モノイド圏ともみなせるので、対称厳密モノイド圏をプロップと呼ぶこともあります（用語運用は曖昧です）。ロブスキ／ザンサイ論文における層化プロップ〈layered prop〉は、余インデックス付き対称厳密モノイド…

…真）である行列 二項述語 ： 二変数のブール値関数 これらは事実上同じモノですが、由来・出自が違います。モノに対して演算を施す場合でも、使われる演算記号は由来により違います。足し算と掛け算に相当する演算記号でも、集合由来、論理由来、算術由来では次の違いがあります。 集合由来 論理由来 算術由来 $`\cup`$ $`\lor`$ $`+`$ $`\cap`$ $`\land`$ $`\cdot`$ この対応表をもう少し伸ばしてみましょう。ベキ集合 $`\mrm{Pow}(X)…

…Y`$ に関する二項述語」と言います。ブール値の論理ORを足し算とみなすと、無限の足し算でも自由にできます。“ブール値係数の行列とみなした成分総和”と“二項述語とみなした存在限量〈existential quantification〉”は同じコト（相互に移りあえるコト）です。$`\quad \sum_{x\in X}A_x^y \longleftrightarrow \exists x\in X. p(x, y)`$関係に関する用語同じモノ／同じコトに異なるたくさんの言葉を割…

…理論： 依存型理論で述語論理が出来てしまう理由 最近の型理論： 外部化手法のもとでのパイ型と指数型 型圏化関手 $`\J`$ と、それのもとになる外延化関手 $`\mrm{Inst} = \ol{(\hyp)}\;`$ を使う手法が外部化〈externalization〉手法で、外部化手法の妥当性や有効性に関する疑問点・問題点が冒頭の引用です。インデックス付き圏 $`\cat{P}`$ は、$`\cat{C}`$ の適当なシード射／シード四角形のクラスに対してハイパードクトリ…

…理論： 依存型理論で述語論理が出来てしまう理由」で導入した概念で、$`\J`$ で表します。$`\xymatrix{ \cat{C} \ar[r]^{\mrm{Inst}} \ar[dr]_{\J} & {\bf Set} \ar[d]^{\mrm{Disc}} \\ {} & \dim{\bf CAT}{1} }\\ \In \mathbb{CAT} `$外部化手法では、型外延化 $`\mrm{Inst}`$ や型圏化 $`\J`$ を用いて、圏 $`\cat{C}`$ の…

「依存型理論で述語論理が出来てしまう理由」において、2つの圏をもとにしてハイパードクトリンを構成する方法の概略を示しました。このハイパードクトリンは、依存型理論と述語論理のどちらも記述できる汎用的な機構になっています。銀河（型をホストする圏）からハイパードクトリンを構成したい動機のひとつは、構文的に定義される“型理論の型判断”や、“論理のシーケント”にハッキリした意味を与えたいからです。「ハッキリした意味」の“意味”をこの記事で説明します。$`\newcommand{\cat…

…理論の論理的対応物が述語論理〈predicate logic〉です。述語論理の圏論的定式化にはローヴェア〈William Lawvere〉のハイパードクトリン〈hyperdoctrine〉があります。ハイパードクトリンは、依存型理論の枠組みでもあります。カリー／ハワード／ランベック対応により、“単純型理論←→命題論理”、“依存型理論←→述語論理”と対応するので、依存型理論と述語論理が共通のフレームワークに包摂されるのは当然とも言えます。適当なセッティングのもとで、依存型理論を…

…理論： 依存型理論で述語論理が出来てしまう理由 最近の型理論： 型判断／シーケントの意味論に向けて 最近の型理論： 外部化手法のもとでのパイ型と指数型 最近の型理論： デカルト閉圏の外部化・内部化とスノーグローブ現象 最近の型理論： 宇宙より銀河 最近の型理論： 具体的・構文的なコンテキスト 最近の型理論： 拡張包括構造を持ったインデックス付き圏 関連記事： 射ファミリーと圏論的コンビネータ 圏の束構造と包含的圏 一般化されたファミリーの圏 自然言語混じり形式証明の意味論と最…

昨日の記事「述語論理： 二重圏的ハイパードクトリン」で、二重圏的ハイパードクトリンという概念を出しました。二重圏的ハイパードクトリンを定義するために、シード付き二重圏を定義したのですが、どうも安直過ぎました。シード付き二重圏を再定義します。$`\newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in } } `$内容： 二重圏的ハイパードク…

…いやすい気がします。述語論理系やベック／シュバレー条件が比較的素直に定義できます。[追記]シード付き二重圏の定義が甘すぎたので、「述語論理： シード付き二重圏 -- 訂正と再論」に訂正を書いています。本文中でも、注意を追記しています。[/追記]$`\newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in } } \newcommand{\i…

…圏とシーケント計算 述語論理： 様々な多圏達の分類整理 証明と計算は同じこと： 形式証明におけるノードとコネクター 多圏をモノイド圏とみなす多圏における多射の結合は、ストリング図ならワイヤーを引き回して繋ぐことに対応します。様々なワイヤリングがありますが、次のルールによる結合なら単純です。 複射 $`f: \Gamma \to \Phi`$ と複射 $`g: \Theta \to \Psi`$ は、$`\Phi = \Theta`$ のときだけ結合可能とする。 $`\cat{…

…の記事にあります。 述語論理： 様々な多圏達の分類整理 翻訳意味論では、例えばLean 4のような既存の証明記述言語にコンパイル〈トランスパイル〉します。自然言語混じり形式証明を既存の証明検証系でチェックしたいときは、このようなコンパイルが必要です。もっとも、近い将来に証明ソフトウェアが自然言語混じり形式証明を直接解釈できるようになれば、このようなコンパイルは不要となりますが。自然言語混じり形式証明の記述言語を $`\mathscr{N}`$ 、表示的意味論の意味領域である多…

…いては、次の記事に（述語論理との関係から）まとめてあります。 述語論理： 様々な多圏達の分類整理 次節で具体例を出して説明を続けます。形式証明のストリング図次の図は、「証明支援系がダメだった理由と、AIでブーストする理由 // 人間可読証明」で出した、形式証明を表すストリング図です。この図をテキストにエンコードするときや、地の文で説明するときは矢印記号を使います。そのとき、「何をどの矢印記号で表すか」が分野ごと・コミュニティごとに違っていてシンドイ。以下の記事に嘆きや対処法が…

…ベースを捨てて、一階述語論理／高階述語論理などをベースにした証明ソフトウェアに乗り換える。 ラムダ計算／型理論ベースは維持して、シンタックスシュガーやコンパイル〈トランスパイル〉技術で難読性を緩和する。 一番は身も蓋もない解決策だし、「根性と時間」を持ち出す時点で解決策とも呼べません。二番は考慮に値する案ですが、現在主流で広く利用可能な証明ソフトウェアがラムダ計算／型理論ベースであるという現実的な事情から採用が難しいでしょう。となると、三番しか残っていません。今でも、より読み…

…ます。$`P`$ は述語（を表す論理式）だとします。$`\context \Gamma\\ \calc \forall x\in X. P(x) \leftarrow\\ \uparrow \text{ 全称記号を外す}\curs `$[Enter]キーで次の状態になります。$`\context \Gamma\\ \calc \forall x\in X. P(x) \leftarrow\\ \uparrow \text{ 全称記号を外す}\\ \quad \context …

…m{Int}]`$ 述語論理の記法： $`\forall X\in{\bf Type}. \mathrm{List}(X) \Rightarrow \mathrm{Int}`$ 束論的な記法： $`\bigwedge_{X\in{\bf Type}} [\mathrm{List}(X), \mathrm{Int}]`$ 圏論的な記法： $`\mathrm{lim}_{X\in{\bf Type}} [\mathrm{List}(X), \mathrm{Int}]`$ 一般的な…

…論 論理 命題論理 述語論理 用語法・記号法用語は、通常使われているものは無視します。慣習・伝統より合理性・一貫性・効率性を重視します。それにより、カリー／ハワード／ランベック対応が明瞭になります。通常使われているメジャーな用語法は別途調べてください。 双対概念には一律に "co"〈余〉を付ける。 逆写像には一律に（今回はカリー化しか登場しないが） "un"〈反〉を付ける。 依存性がある場合は一律に "dependent"〈依存〉を付ける。 限量子に関係する場合は一律に "q…

…変数記号／関数記号／述語記号などを組み合わせた記号的表現を項〈term〉と呼びます。項 $`\psi`$ に対する型判断〈{type | typing} judgement〉とは、次の形のものです。$`\quad t: T, x: X \vdash \psi : C`$これは次のような意味を持ちます。 変数 $`t`$ の型は $`T`$ である。$`t`$ は今は注目してない変数である。 変数 $`x`$ の型は $`X`$ である。 項 $`\psi`$ は変数 $`t,…