…scourse〉： 述語論理の用語で、述語の域のことです。 個体〈individual〉： 論域の要素のことです。 具体化〈instantiation〉 ： パラメータ／インデックス／個体を特定値にして評価したモノです。 証拠〈witness | evidence〉 ： 原則的に証明と同義ですが、公理命題にも証拠は付いていると考えます。命題のラベルは、実際は命題の証拠の名前です。 背景〈background〉： 当面の興味の対象ではないが、暗黙に仮定されているものという意味で…

…ます。ここに出てくる述語記号 $`\mrm{isEven}, \mrm{isPrime}`$ の意味は想像できるでしょうが、述語記号の定義も前提にちゃんと入れるなら次のようになります。$`\quad \mrm{isEven} := \lambda\, m\in {\bf N}.(\exists k\in {\bf N}. m = 2k), \\ \quad \mrm{isPrime} := \lambda\, m\in {\bf N}.(\\ \qquad m \ne 1 \…

…／複圏／多圏の可達性述語 指標の理論や依存型理論の場合 圏論、型理論、論理圏論、型理論、論理は「似てるな」という印象を持ちますが、それは印象だけではなくて、キチンと対応付けることが出来ます。多少乱暴ではありますが、「表層が違うだけで内容的には同じ」と言っていいでしょう。「内容的には同じ」であっても、異なる分野なので、異なる用語法・記法を持ちます。それは、地方ごとに方言があるのと似た状況です。「郷に入っては郷に従え」なので、特定の分野について語るときはその分野の用語法・記法を使…

…ぶ）を、型を制約する述語のように使っている場面があって、指標は述語じゃないのに、これは何でだろう？ と。人が概念を誤認したり誤用するときは、誤認・誤用をさせるようなメカニズムが背後にあるのでしょう。それを探ってみます。存在型と呼ばれていた型の一部をヒルベルトのイプシロン記号で説明することを目標にします。その準備として、型クラス述語という概念を導入します。$`\newcommand{\cat}[1]{ \mathcal{#1}} \newcommand{\mrm}[1]{ \m…

…、論理式（が表現する述語）を、単一の真偽値へと変換するオペレータだと考えることができます。もうひとつのオペレータ $`\Delta`$ とトリプル〈トリオ〉を作ると、三者は密接な関係を持ちます。その関係性を次のような記法で表し、随伴トリプル〈adjoint triple〉と呼びます。$`\quad \exists \dashv \Delta \dashv \forall`$依存型理論においても随伴トリプルが現れます。$`\mathscr{E}`$ を型変数 $`\alpha`…

…Bool}]`$ （述語の型） $`[\mrm{List}(\alpha), \mrm{Int}]`$ （リストの長さ $`\mrm{length}`$ が所属する型） 「$`\alpha`$ を含む」と書きましたが、$`\mathscr{E}`$ に $`\alpha`$ が現れなくてもかまいません。例えば： $`\mrm{Bool}`$ $`\mrm{Bool}\times \mrm{Bool}`$ $`[\mrm{Int}, \mrm{Bool}]`$ $`\mrm{L…

…命題とみなせるので）述語論理の論理式だと思えます。$`\forall X\in {\bf T}.\\ \quad \mrm{dom}(\mrm{length}_X) = \mrm{List}(X) \,\land\, \mrm{cod}(\mrm{length}_X) = \mrm{Int}\\ \forall X\in {\bf T}.\\ \quad \mrm{dom}(\mrm{first}_X) = \mrm{List}(X) \,\land\, \mrm{cod}(…

… ハブ記事： 圏論的述語論理とお絵描き 複圏、余複圏、多圏まず、複圏〈multicategory〉、余複圏〈comaulticategory〉、多圏〈polycategory〉についてすごく大雑把に説明します。n, m は任意の自然数（0 も許す）とします。 圏 ： 圏の射は単一の入力（域の対象）と単一の出力（余域の対象）を持つ。 複圏 ： 複圏の射はn個の入力と単一の出力を持つ。 余複圏 ： 余複圏の射は単一の入力とn個の出力を持つ。 多圏 ： 多圏の射はn個の入力とm個の…

… ハブ記事： 圏論的述語論理とお絵描き 記法に関する注意ターンスタイル記号 '$`\vdash`$' は、証明可能性〈導出可能性〉を表すメタ述語記号としても、シーケントの区切り記号としても使われます。このオーバーロードは混乱・誤解をまねくリスクがありますが、広く採用されているので、ここでもシーケントの区切り記号に '$`\vdash`$' を使います。区切り記号としてのターンスタイルは、特に何かを主張するものではなくて、単に“区切りに使う変な矢印”です。バーケダル／ビージャッ…

…は、$`X`$ 上の述語〈predicate〉と呼びます。また、集合 $`X`$ のすべての部分集合の集合（ベキ集合〈powerset〉）は $`\mrm{Pow}(X)`$ と書きます。$`X`$ 上の述語と、$`X`$ の部分集合は次のように1：1対応します。$`\quad (p:X \to \{\mrm{true},\mrm{false}\}) \longleftrightarrow \{x\in X\mid p(x)\}`$この対応を前提としたときに、以下の対応表は間…

記事タイトルの「述語論理」は、昨日の記事「圏論的述語論理とお絵描き」で紹介した、ハイパードクトリンによる圏論的述語論理のことです。このスタイルの述語論理に関係する話題には、記事タイトル冒頭に「述語論理：」を付けるつもり。ハイパードクトリンは、2つの圏 $`\mathcal{C}, \mathcal{L}`$ とそのあいだの反変関手 $`\mathrm{Pred}:\mathcal{C}^\mathrm{op} \to \mathcal{L}`$ で構成されます。今日は、ハイパ…

圏論的述語論理の話は過去に何度かしたことがありますが、現時点での観点から大雑把に復習してみます。そして、「全称記号の導入」と「存在記号の消去」と呼ばれる“推論規則”の絵の描き方を紹介します。$` \newcommand{\Imp}{\Rightarrow } \newcommand{PPB}{\diamondsuit} % Predicate Pull Back \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\op}{\mat…

…変数 論理式から作る述語関数 行列記法と行列計算 単位対象、単元集合、自明圏 0, 1, 2個のモノからなる集合／圏 演算記号と恒等 ホムセットの交わり 同型・同値 CD構造と余CD構造 複、余複、多 最初の記事＋シリーズ目次 方向付き区切り記号リスト／タプルの区切り記号にはカンマが使われますが、我々の目的ではカンマだけでは足りません。まず、記号 '' をカンマと同じ意味・使用法で導入します。例えば：'' はカンマより優先度が低いので、次のように入れ子が書けます。'' で区切…

…ダメです。今定義した述語 を使って写像集合を定義します。ここで、 はベキ集合です。定義から、 です。特に、 なので、次のどちらかが成立します。 どちらになるかは の真偽によりますが、 は真です（成立してます）。なぜかというと、写像の条件である を と書き換えてみると、含意の前件が偽となり命題は常に真となるからです。このことから、集合 が何であっても、 であっても、です。集合圏のホムセットの場合とは事情が異なります。 の場合でもあっても、次が成立します。異なる集合ペア に対して…

…、余域が2である射を述語〈predicate〉と呼びます。チャンネルの結合〈composition | 合成〉の記号は で、反図式順の中置二項演算子記号として使います。その他に、中置演算子記号 も使います -- これらはすべてチャンネルの結合の記号で、 と意味は変わりません。色々な結合記号を用意しているのは、結合される2つの射の種類ごとに使い分けるのです。 2つの射の種類 結合の表し方 結合記号の語順 一般の射と一般の射 反図式順 状態と一般の射 反図式順 一般の射と述語 図…

…意味論の状態変換子／述語変換子の概念を移入しました（「ベイズ確率論、ジェイコブス達の新しい風」参照）。ドールクゥイスト〈Fredrik Dahlqvist〉達は、ベイズ反転の定式化のためにプログラム意味論のω完備性の概念を移入しました（「統計的反転の圏論的セットアップ 1/2」参照）。実は、スピヴァック／パターソンが利用したローヴェア流セオリー論も、プログラム意味論におけるインスティチューション理論〈institution theory〉としてかなり整備されています（「インス…

…マルコフ核とファジー述語 エフェクト代数と論理 PS論理 マルコフ核とファジー述語可測空間とマルコフ核の圏（「マルコフ核： 確率計算のモダンな体系」参照）をStocとします。B = {0, 1} をブール値〈二値真偽値〉の集合として、これを離散可測空間と考えます。つまり、B∈|Stoc| 。マルコフ核 p:X → B in Stoc の、可測空間の圏Measでの表現は p∩:X → Giry(B) in Meas となります（通常、p と p∩ は同一視されます）。ここで、G…

…条件の具体例として、述語論理における限量子と代入〈substitution | 置換〉の交換可能性があります。 代入を施した論理式に限量子を付けたものは、限量子を付けた論理式に代入を施したものと同値。 この交換可能性をベック／シュバレー条件の形で記述してみます。「Σ-Δ-Π随伴、もう一言」で述べたΣ-Δ-Π随伴〈随伴トリオ〉とも関係します。この記事で使っている、カクカクで見栄えが良くないストリング図は、「カリー／ハワード対応のための記法・図法」で述べた方法で描いています。カク…

…rd。これで、論理の述語のときと同じセットアップになりました。連続写像 f:A → B in CompHouse に対して、順序集合のあいだの単調写像 Δf:C(B, [0, ∞]) → C(A, [0, ∞]) in Ord が誘導されます。ここから先は論理の場合と同じように定義して、連続関数の最大値／最小値の議論ができます。コンパクト・ハウスドルフの仮定がなくても、∞を入れているので連続関数の上限／下限は定義可能です。データベースの場合最後にほんとに一言だけ、データベース…

…が無難です。依存型と述語論理の関係は、いずれ書く機会があるでしょう、たぶん。上記のプロファイルでは「ギリシャ文字小文字は型を表す」約束ですが、一般的な“パラメータを持った型”を扱いたいので、多相関数のプロファイル記述は次の形にします。 ここで： fは多相関数（ちゃんとした定義は後述） Xはパラメータの集合（集合なら何でもいい） xは何らかのパラメータ（xは束縛変数になる） F(x) と G(x) はパラメータを持った型 パラメータ a∈X を固定すると、通常の型〈集合〉のあい…

…確率分布でも同義）と述語〈ファジー述語〉を双対的に扱います。述語はもちろん状態ではありません。ジェイコブス〈Bart Jacobs〉は、「状態と述語を混同するな」と注意しているのですが、それを見て僕はハッとしました。自分が混同していた人だからです。今でも、「混同してんじゃないか？ 誤解してんじゃないか？」と不安になります。この混同を引き起こす大きな原因は確率密度関数でしょう。確率密度関数は確率測度の表現ですが、それ自体は実数値関数なのでファジー述語と区別が付きにくいのです。 …

…る可測関数をファジー述語〈fuzzy predicate〉と呼びます。ジェイコブス達の定式化（「ベイズ確率論、ジェイコブス達の新しい風」参照）では、確率測度を“状態”、ファジー述語を単に“述語”と呼んで、状態と述語を双対的に扱います。ここでも同様な考え方をするので、混乱の心配がなければファジー述語を単に述語〈predicate〉と呼びます。可測空間X上の確率測度の集合をP(X)とします。必要があれば、P(X)とシグマ集合代数ΣP(X)（「拡張スタイルのジリィモナド // 確率…

…決める。（leは全域述語になる。） le(μ, ν) は未定義とする。ソフトウェア的に言えば例外を投げる。（leは部分述語になる。） 今の文脈では、どちらにしてもかまいません。 [/補足]極性付き自然数のリストのあいだの順序を使うと、多インデックスセットは次のように定義できます。 For μ∈(NP0)r, 〚μ〛 := {a∈(NP0)r | 0＜ a ≦μ} 集合の定義のなかの下線付きラテン文字'a'は極性付き自然数のリストを表す変数です。0は、0が並ぶリストを表していま…

…ブール値を返す関数〈述語〉です。論理アンド（&&）や論理オア（||）も使えます。WinActiveに渡す引数は旧ディレクティブ構文を文字列にしたものです（2引数にすればいいのに、と思いますけど）。コマンドラインここからは、ホットキー設定のことは忘れて、スクリプトを書いてみます。 ; AHK-01.ahk #SingleInstance, Force InputBox, UserInput, Input Box, Please input your name. MsgBox, …

…数環／半環 ファジー述語代数 指示関数＝指示述語 ラムダ記法 カリー化、反カリー化 書字順記法と反書字順記法 ジリィ関手 記号のだいたいの約束 マルコフ核の定義 マルコフ核のラムダ記法表示 積分表示と被積分形式 ランダム要素 ランダム要素の事象への所属度 ディラック測度 チャップマン／コルモゴロフ結合 デルタ関手 暗黙のデルタ ペアリング記法 測度の前送り -- 写像の場合 関数の引き戻し -- 写像の場合 随伴公式 -- 写像の場合 測度の前送り -- マルコフ核の場合 関…

…を、等式的論理と一階述語論理に固定する。 指標Σに対するモデルの圏を、Model[Σ] := [FreeCat(Σ), Set]CAT と具体的に与える。 指標圏を固定する気はないのですが、当座の指標圏としては、有向グラフの圏を採用します。ただし、単に「有向グラフ」と言ってしまうと誤解をまねきそうです。通常の有向グラフGと、両端を共有するパスの対（スピヴァックの言葉だとパス同値関係〈path equivalence relation〉、「衝撃的なデータベース理論・関手的データ…

…理を等式的論理と一階述語論理に固定します。等式的論理／一階述語論理以外の論理を使いたいケースは少ないからです。 モデルの圏の作り方を固定する： 抽象的インスティチューションのモデルの圏は、公理的に存在が要請されているだけで、どう作るかは指定されてません。が、特殊化されたインスティチューションでは、指標Σのモデルの圏 Model[Σ] は、Model[Σ] := [FreeCat(Σ), Set]CAT と具体的に与えます。指標Σは有向グラフとみなし、FreeCat(Σ) はΣ…

…理における ∃ -| π* -| ∀ 述語論理とインデックス付き圏と限量随伴性 全称・存在限量子の色々をまとめた絵 集合達の直積と直和における Σ -| Δ -| Π カン拡張における上下左右： 入門の前に整理すべきこと // 随伴トリオとその例 加群層における f! -| f-1 -| f＊ 層に関してちょっと // グロタンディーク演算 *1:関係データベース用語のジョインがミートに相当し、ユニオンがジョインが相当します。順序構造のジョインをユニオンと呼ぶこともあります。

…集合のカン拡張と特徴述語論理」でそう呼んでます。） 優拡張のなかで最小のもの（最小優拡張）が、カン優拡張 劣拡張のなかで最大のもの（最大劣拡張）が、カン劣拡張 とかなら、まだしも覚えやすかったのだけど、実際は何の連想も働かない左と右、どうコジツケましょうか？随伴の左右と結びつける随伴の左右と結びつけることにします。随伴に関しては、左右の定義を覚えてます（僕は）。これもコジツケで覚えてるのですが、今日はそのコジツケの話はしないで、ともかくも「随伴の左右は知ってるよ」を前提します…

…産まされ［二（多）階述語論理］（上空移行）した『包摂言語』と生り・ならされたもので、［カオス］表示の（ｅ）（π）（ｉ）は幽霊的な［内在秩序］として姿が見えなくなっている。 【数そのモノ】は、［カオス］から［コスモス］・［コスモス］から［カオス］を行き来できる『包摂言語』と生り・ならされている。 このことにより［コスモス］表示内での［四則演算］は、［群］（可換群）としての［算術（算数）演算］を生得（スービタイズ）的に獲得し・獲得させられていると観る。 結局、無限（∞）の言語（数…