このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

述語, 論理 の検索結果:

チャンネル理論の演算子記号が使いにくい理由

…、余域が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)(「拡張スタイルのジリィモナド // 確率…

多タプル・多行列とその計算 1/2

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

プログラミング言語としての AutoHotKey

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

マルコフ核: 確率計算のモダンな体系

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

等式的関手インスティチューション(概要)

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

任意の圏を等式により2-圏とみなす

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

ガロア接続(順序随伴系)の簡単な例

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

ガーッ! また左と右が。カン拡張

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

どうやら人間のようだ

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

奇妙なコメント、人が書いてる?自動生成?

…然数』氏による)。「述語論理とインデックス付き圏と限量随伴性」へのコメント: ≪…トポスがあれば(高階の)述語論理の入念な議論…≫との事を、 ライプニッツの「理性に基づく自然と恩寵の原理」の『《モナド》』に『自然比矩形』を[同定]すると≪…トポス…≫に観えて、『《モナド》写像(関数)』が『次元の数』と生り[位相]の[数学概念]を[内在秩序]化し、[数学共同体の自然数]が『縮約(縮退)自然数』として『天賦』し・させていると観る。まったく意味不明ですが、スパムでもないので放置しま…

ディープラーニングの論理:: シャープネスと外延化

…準備 シャープネス 述語の外延化 準備基本的な参考文献は、Jacobs-Zanasi-2018です。 Title: The Logical Essentials of Bayesian Reasoning (3 Apr 2018 (v1), 27 Apr 2018 (v2)) Author: Bart Jacobs, Fabio Zanasi Pages: 29p URL: https://arxiv.org/abs/1804.01193 この論文の解説は「ベイズ確率論、ジェ…

ゲーデルの不完全性定理と圏論のセミナーをやります

…年9月から)では古典述語論理(普通の論理)を前回より詳しく説明・練習するつもりです。「圏論」は新しいコースです。事前には何も知らない人でもモナドまでたどり着けるのが目標です。このブログで何度か強調しているように、集合の圏のような巨大な圏ではなくて、手で触れる“可愛い圏”からスタートして、圏を身近に感じてもらえれば、と思っています。圏論の応用は多岐に渡るので、特定の話題に偏りすぎないように注意します。そういう方針なので、コンピュータやプログラムの話ばっかりってことではないです*…

データベース:: 論理の使い所は

…ないのなら、第2章「述語論理とリレーショナルモデル」は不要です。奥野さんは、 論理学に触れない正規化の解説は、でたらめだと言っても過言ではありません。 と思いっきり強調太字で書いてますが、過言です。実際に、第3章以降で、述語論理を実質的・本質的に使っている所はないです。 奥野本に限らず、「RDBは集合論をベースにしている」「RDBは論理を使っている」と言うだけで、実際には集合論も論理もロクに使っていない説明をみうけます。論理を使うのは、形式化のためです。何らかの形式体系〈fo…

圏論図式の描き方と解釈のコツ

…tion-ofが二項述語です。fとgは共端な射であることも表すには、図式を混ぜ込んだほうがいいでしょう。X is-solution-of (f, g) の意味は、Xから出る射eがあって、eが(f, g)の等値核であることですから:2行目の論理式に含まれる左上の'eq.'は、当該の図式が等値核図式であることを示します。等値核図式であること(is-equalizer-diagram)をちゃんと書けば次のようになります。(Xとバツ印が紛らわしいですからご注意。)論理記号の意味は: …

ベイズ確率論、ジェイコブス達の新しい風

…成する 状態変換子と述語変換子 確率的状態 確率的状態変換子とチャンネル チャンネルについてもう少し 状態とチャンネルの実例 ファジー述語 ベイズ論理/ベイズ計算に向けて ベイズ確率論を整理して再構成するベイズ確率論〈Bayesian probability theory〉は幾つかの起源を持ち、たくさんの応用分野を持ちます。関連する諸分野が多い理論にありがちな事として; 各分野の概念・用語・記法がもとの理論にシッチャカメッチャカになだれ込んで、もとの理論がグチャグチャに見えて…

論理式の集合とは何か?

…算記号〈関数記号〉 述語記号〈関係記号〉 論理記号〈論理結合子記号と限量子記号〉 補助記号 説明は後にして、各種の記号を並べてしまいます。 定数記号: '0', '1' 変数記号: すぐ下で定義する 演算記号: '+', '*' 述語記号: '=', '≦' 論理記号: '∧', '¬', '∀' 補助記号: '(', ')', ',', '.' 変数記号は無限個あるので、書き並べるわけにいきません。変数記号は次のように決めます。 英字〈ラテン文字〉小文字1文字、またはその後…

順序集合のカン拡張と特徴述語論理

…張と左カン拡張)を、述語論理の限量子と捉えてみます。内容: 圏と順序集合 基本的な言葉と記法 劣拡張と最大劣拡張 ミート完備な順序集合 最大劣拡張の構成 最小優拡張と書き方の約束 特徴述語論理 おわりに 圏と順序集合圏論に関する話を、順序集合に関する話にダウングレードすると、議論が容易になります。例えば、2つの関手が随伴対であることは、2つの単調写像がガロア接続を形成することと同じです。それについては: 順序随伴性: ガロア接続の圏論 モナドの順序的対応物に関しては: 順序集…

論理/メタ論理の記法をどうするか 2: 悟りへの道

…// 論理記号など 述語論理とインデックス付き圏と限量随伴性 // 命題論理 述語論理とインデックス付き圏と限量随伴性 // 述語論理 僕の本音としては、含意に'⇒'を使いたくない。二本棒矢印は、別な目的で使いたいのです。一本棒矢印も含意以外で使いたいこと多いし。論理ではいろいろな矢印が出てくるので、矢印記号が不足して困るんですよ。次の記事参照。 論理におけるさまざまな「矢印」達 ところで、いま僕は「含意記号」といいましたが、「ならば」を意味する記号は条件記号〈conditi…

『圏論による量子計算と論理』はエキサイティングだ (1/2)

…論理的対象と考えての述語論理、第5章は状態空間と観測量を扱う論理です。こう書くと、オーソドックスなコースのように思えるかも知れませんが、いやいやっ、並の教科書とは違いまっせ、徹底的に圏論的〈カテゴリカル〉で公理的です。圏論的線形代数と圏論的論理のテキストなのです。次節以降でもう少し詳しく内容を紹介しますけどね。時間がない人は、最後の節に飛べ → 。以下この記事では、『圏論による量子計算と論理』を「ヒューネン本」とも呼びます。翻訳日本語本であることを強調したいときは「ヒューネン…

TypeScriptで(無理して)論理式: 言霊排除

…な)人工言語は、古典述語論理とラムダ計算でしょう。しかし、これらの言語にどうも馴染めない、という人もいるし、ソフトウェアで構文をチェックしたり実行したりするすることが(お手軽には)できません。Coq、Isabelle、Mizarなんてプログラミング言語もありますが、これらも敷居が高いので、普通のプログラミング言語(汎用プログラミング言語)を使うことにします。そう、TypeScriptです。TypeScriptがサンプル記述に向いていることは次の記事で書いています(興味があれば…

空虚な束縛とEPペア

…Pが、集合X×Y上の述語だとします。構文的には、Pは変数x, yを含む(可能性がある)とします。正確には、意味領域の述語(真偽値をとる関数) P:X×Y→{True, False} と、それを表現する構文領域の存在物である論理式は別物なんですが、ここではあまり区別しないで、同じ記号で表します。「命題」という言葉も、意味領域の述語だったり、構文領域の論理式だったり、文脈で指すものが変わります。さて、全称命題 ∀x∈X.P(x, y) や存在命題 ∃x∈X.P(x, y) を作る…

全称・存在限量子の色々をまとめた絵

…] -- 集合X上の述語の集合。述語は、X→{True, False} という関数だと思っても、Xの部分集合だと思っても、どっちでもいいです。述語のあいだの順序関係をもとに、圏とみなします。 π2:X×Y→Y という第二射影 π2*:Pred[X]→Pred[X×Y] -- 第二射影π2から誘導される述語のあいだの写像。述語を関数だと思うなら、π2*(P) := Pπ2 。構文的には、変数水増し〈variable thinning〉オペレータです。 '-|' は随伴対を表す記…

上付き・下付き添字をマジに考えたら頭痛がした

…定した集合ではないような印象はあります。集合とは限らない類〈class〉に値をとる場合が族の雰囲気。このテの話を、印象・雰囲気で議論してもラチがあかないので、やめときます。 *4:厳密には、Map(A, X)のXは、忘却関手をUとして U(X) です。集合圏とベクトル空間の圏のあいだの随伴関手対があるのです。 *5:自然変換や圏論的オペレータです。 *6:directCoeffの定義を形式言語でしようとすると、述語論理の論理式以外にヒルベルトのイプシロン記号が必要になります。