…の記事にあります。 述語論理： 様々な多圏達の分類整理 翻訳意味論では、例えば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,…

…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`…

…： 代替案 型クラス述語とイプシロン型 全称型と存在型（表面的な定義）とりあえず、全称型／存在型の表面的な意味（ほとんど無意味だが）を説明します。$`\alpha`$ を型変数として、$`\alpha`$ を含む型項〈type term〉（型を表す記号的表現）を $`\mathscr{E}`$ とします。$`\mathscr{E}`$ の例は： $`\alpha`$ $`[\alpha, \alpha]`$ （ブラケットは指数型〈関数型〉） $`\alpha \times \…

…命題とみなせるので）述語論理の論理式だと思えます。$`\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が並ぶリストを表していま…