…ータは割と簡単です。古典的微分計算と対応付けたり、絵による微分計算（微分絵算）も出来るでしょう。絵図主義者（picturalist）には朗報なんですが、微分圏は絵算と意外に相性がいいです。絵算の創始者の一人であるペンローズは、テンソルの代数計算だけでなく、テンソル場の微分計算も（ペンローズ・ヒエログリフとも呼ばれる）彼の図式法で遂行していたので、微分も絵で描けることもむべなるかなです。*5ヤコビ微分圏の典型的な事例は、ユークリッド空間の開集合と、その上で定義された無限回微分可…

…は日常生活の論理を（古典論理より）うまく説明できるかも知れません。「アブダクションと確率的推論」で断片的に述べたことを、もう少し体系化できる可能性があります。現時点での感触としては、「計算と論理と圏の三者が密接に関連している」というカリー／ハワード／ランベック対応（Curry-Howard-Lambek correspondence）の確率版があるような気がします。オマケ：マルコフ・テンソルと関数の一覧矢印が'→!'と書いてあるのは関数です。 test: 感染? → 陽性? …

…とも言えないのです。古典論理では認められていなくても一理ある推論（のいくつかの形式）をアブダクションと言います。「AならばB」から「BならばA」を導くのもアブダクションの一種です。このアブダクションを確率的推論の立場から分析してみます。内容： 一理ありそうな推論 黒いはカラス 「『カラスは黒い』が本当だ」とはどういうこと？ 鳥に関する観測結果をテーブルで表す 同時確率テーブルと条件付き確率テーブルの転置 真である度合 一理ありそうな推論古典論理や直観論理から見て認められない推…

…いう発想で展開される古典モデル理論の再構築版が、インスティチューション独立モデル理論（Institution-independent Model Theory）です。「インスティチューション独立」は、個々のインスティチューション（論理系）に依存しないということであり、インスティチューション理論をベースにした一般（汎用、普遍的）モデル理論です。特定の基底論理に依存したいという気持ち（邪念？煩悩？）はけっこう強烈なものなので、その誘惑を排除してニュートラルであり続けるのは大変です…

…toward 量子と古典の物理と幾何＠名古屋」と付けた一連の記事を書いた動機は、自分の考えを整理するため、それと、事後資料を準備するためです。「事後資料」というのは、「僕が省略してしまった事、詳細が不明な事、周辺や背後の情報」などを後から知りたくなったときに参考になるような資料という意味です。事後資料は、こんなもんでまーいいかな、と思います。 PROと代数系 高次圏の次元について 従順な複体から作られる3次元の圏 関係圏 ストリンググラフのレベル関数と全順序 3-圏と、3-圏…

…ておきます。 *2:古典微分幾何（classical differential geometry）という言葉もよく使われます。 *3:過去の記事「微分のチェーンルール」や「接関手の上のモナド」では単にManと書いた圏です。 *4:マウント・アリソン大学（http://www.mta.ca/）のクラットウェルのページが消失しているようです。 *5:[追記]スライドはありますね。http://www.mathstat.dal.ca/~selinger/fmcs2012/slide…

…は、二値ブール代数（古典命題論理の真偽値）から否定を忘れ、論理ORを足し算、論理ANDを掛け算と思った可換半環です。Bでは足し算がベキ等でs-完備になるのは明らかです。決定性オートマトンは、集合圏のなかでのモノイド作用であり、非決定性オートマトンは、B-半ベクトル空間の圏のなかでのモノイド作用です。決定性オートマトンは特殊な非決定性オートマトンであり、非決定性オートマトンは状態空間のベキ集合を使って決定性オートマトンに変換できます。この相互関係は、随伴関手ペアによる結び付きだ…

…き実行の「条件」が、古典二値の命題でいいのかは疑問です。ハング（無限ループ）するプログラムとか判断困難な状況を考えると、4値論理がいいような気がします。 3値または4値の論理の使いどころ 4値の論理のベキ集合モデル 時分割実行と待ち合わせ複数のCPUを使う「ほんとの並列実行」は、時分割方式で単一CPUでもシミュレートできます。これはよく知られた事実で、現実にも使われています。でも僕は時分割シミュレーションが不思議でしょうがありません。シミュレートのメカニズムが目に見えるように…

…数として行列を作り、古典的な行列計算／テンソル計算を定義します。すると、これはテンソル半加法圏となります。以上のように、古典的な行列計算／テンソル計算がスカラー系（係数半環）からテンソル半加法圏の構成を与えているわけですが、こうして構成したテンソル半加法圏がもとの圏Cと一致する（圏同値である）保証は全然ありません。もとの圏に次の条件を付ければ、再現できるのではないかと思えます。 Cの単純対象はすべて、I（単位対象）と同型。つまり、単位対象は本質的に1個しかない。 Cの対象はす…

…ほうが自然です。（「古典論理は可換環論なんだよ」参照）集合＝離散空間X上のB値連続関数＝単なる関数の全体を C(X, B) とします。C(X, B) はB係数の可換環で掛け算の単位元を持っています。可換環 C(X, B) の極大イデアルの全体がストーン／チェック／ウォールマン・コンパクト化を与える、ということが「超フィルター（ultrafilter）って何なんだ： 点？ 確率測度？」の前半で述べた内容です。連続関数（とは言っても単なる関数）f:X→B に対して、Xの部分集合 …

…使うと、ブール代数（古典論理）に関する議論はベキ等可換環の上の代数幾何に翻訳できます。この話は次のエントリーで書きました。 古典論理は可換環論なんだよ 上記の翻訳で、次のように対応します。 フィルター ←→ イデアル 超フィルター（極大フィルター） ←→ 極大イデアル ストーン空間 ←→ スペクトル 超フィルターと極大フィルターは同義語です。ベキ等可換環では、極大イデアルと素イデアルは同じものです。よって、「超フィルターの空間＝スペクトル（素イデアルの空間）」となります。適当…

…示唆に富む論説です。古典論理のストーン双対性を圏論的な双対性の有限的／コンパクトな典型的事例として位置付け、無限的／非コンパクトなケースとしては幾何的論理を対比させています。幾何的論理（geometric logic）は、「SGL読書会」のテキストである"Sheaves in Geometry and Logic"の主要なテーマでしょう（たぶん、僕は最終回だけしか出てないので半分憶測）。古典論理のストーン双対性が、代数幾何の枠組であるスペクトルやスキームと類似であることも詳し…

…い、そのせいで否定も古典論理の否定とは違った振る舞いをします。含意は選言（＝連言）と否定を使って、(A⊃B) := (¬A∨B) と定義します。連言と選言が一致してしまった論理演算（論理結合子）を×と書いて、×、¬ を持つ（そしてコンパクト閉圏がモデルになる）論理をコンパクト論理と呼ぶことがあります。さらに、自己双対コンパクト閉圏をモデルにするような論理を考えると、否定もなくなってしまいます。正確に言うと、¬A = A なので、否定は無意味・不要なのです。(A⊃B) := (…

…含意です。我々が使う古典論理では、P⊃Q は ¬P∨Q と同値です。ここで、「∨」は論理OR（選言）、「¬」は否定です。含意の逆向きの「⊂」は論理記号ではなくて、「A⊂B ⇔ (A⊆B ∧ A≠B)」の意味ですから注意してください。「∀X.…」は「任意の集合Xについて …」と読みます。任意とはいっても、X∈T なので、「∀X∈T.」と書くほうが正確です。ここではまだ出てきてませんが、「∃X.…」は「…である集合Xが存在する」です。定義に基づいて次を示せます。 Aに対して A⊂…

…, false} を古典論理の真偽値の集合とすると、たいていの場合はΩをデータ領域Dに埋め込めます。Ω⊆D と考えると、[D->Ω]⊆[D->D] となります。もちろん、必要があれば「⊆」は圏論的に解釈してください。[D->Ω] はデータ領域D上で定義された真偽値を取る関数（または部分関数）です。部分集合とその特性関数（characteristic function）との対応から、[D->Ω] ＝ Pow(D) ＝ (Dのベキ集合）とみなしてかまいません。つまり、[D->D]…

…。 特に制限なし： 古典論理のシーケント 右側の論理式は高々1個： 直観主義論理のシーケント 左側の論理式は0個： 右片側シーケント 右側の論理式は0個： 左片側シーケント 片側シーケントなんて意味がなさそうですが、そうでもありません。「演繹系とお絵描き圏論」とか「コンパクト閉圏と絵算で理解する線形代数とシーケント計算（入り口だけ）」を参照してみてください。シーケントの形による分類に「古典論理」とか「直観主義論理」とか出てきますが、気にする必要はありません。ある形状のシーケン…

…味により色々ですが、古典論理の標準的な論理結合記号である ∧（連言、かつ）、∨（選言、または）、¬（否定、ではない）、⊃（含意、ならば）としておきます。「論理記号のいろいろ」と「さまざまな「ならば」達」も参考にしてください。2 + 3×4 = 14 と x + 1 ≦ 5 は原子論理式なので、(2 + 3×4 = 14) ∧ ¬(x + 1 ≦ 5) は原子論理式から組み立てられた論理式の例となります。型の論理式型に関する議論でも、項と論理式（命題）が出てきます。しかし、型の…

…では解釈できません。古典論理のように、左右のカンマの意味が異なるなら、2つのモノイド積を持つ圏が必要になります。コンパクト論理ならモノイド圏でも大丈夫です。話を簡単にするために、コンパクト論理のシーケントを考えることにします。この場合、左右のカンマをどちらもモノイド積に対応させて解釈できます。しかしそうすると、A, B ⇒ X, Y と A×B ⇒ X×Y の違いは（意味論的に）説明できなくなります。そこで多圏を使いましょう。圏Cの対象のリストの集合（クリーネスター）|C|*…

…定義は、先日の記事「古典論理のシーケントとコマンド： カリー／ハワード対応」に書いたので参照して下さい。シーケントは次の形をしています。 A1, ..., An ⇒ X1, ..., Xm 最初から圏C上の意味論を考えることにします。Ai（i = 1, ..., n）、Xj（j = 1, ..., m）は、論理なら命題変数や論理式ですが、ここでは、圏Cの対象だと考えます。圏Cの対象をカンマで区切って並べたものをΓ、Δなどのギリシャ大文字で表します。対象の並びにも圏Cの対象とし…

…ら話題にするのは、“古典論理（風）のシーケント計算”と“コマンド言語によるプログラム”の対応です。コマンド言語とは、「コマンド」と呼ばれる処理の基本単位があり、コマンド達をパイプで結合してプログラムを作るスタイルのスクリプト言語です。具体例は、我々（檜山とKuwataさん）が開発しているCatyScriptを想定しています。シーケント計算とコマンド言語プログラミングの対応を構成するにあたって、中間にフローチャートを挟むと、とても分かりやすくなります。つまり、次のような対応関係…

…あれば否定も入れて、古典論理のすべての能力を使ってもいいでしょう。{A{f}B, B{f}A, C{f}D} のようなホーアトリプルの集合は、連言で解釈します。つまり、3つのホーアトリプルからなる集合は、次の1つの論理式と同じです。 A{f}B ∧ B{f}A ∧ C{f}D 完全に展開すれば： ∀x.[x∈A ⊃ f(x)∈B] ∧ ∀x.[x∈B ⊃ f(x)∈A] ∧ ∀x.[x∈C ⊃ f(x)∈D] ホーアトリプルをベースとしたホーア論理式に、適当な公理と推論規則を…

…表す記号）だとして、古典論理や直観主義論理のときと同様にシーケントを考えます。例えば、A, B → C, D のような形です。二項論理演算が「×」しかないので、シーケントの左右のカンマの解釈は両側とも「×」です。Tを真、⊥を偽として、古典論理では次のような推論が成立します。 A, B → C --------- A∧B → C A → B, C --------- A → B∨C T, A → B ---------- A → B A → ⊥, B ---------- A …

…ことはできるので（「古典論理は可換環論なんだよ」参照）、F2上の線形代数には持ち込めます。でも、x + x = 0 という足し算がどうも不自然に感じるときもあります。x + x = x とすると、いつも使っているブール代数になりますが、もはや体ではなく、線形代数のかなりの部分が使えなくなります。もうひとつ、リー代数などに比べると、計算に出てくる非可換代数は非可換性が激しいのです。例えば、アルファベットAから作った記号列のモノイド M = A* を考えて、適当な係数でモノイド代…

…縮めてみる」とか、「古典論理は可換環論なんだよ」なんかがあります。これらも、マジメに書いてあるみたい。そういえば、「古典論理は可換環論なんだよ」には、「当方記事には過ぎた続編」をtri_iroさんに書いていただきました。「イデアルと論理 番外の補足：ベキ等元と連結性」と「“古典論理＝可換環論”の計算と種明かし」も関連記事です。以上に挙げた記事は、「論理は位相や代数とも関係するんだぜー」みたいなハナシ。そして、「論理も位相も代数も計算科学に関係するんだぜー」が僕の言いたいことだ…

…なら、その論理計算は古典論理と同じようにできます。しかし、コンピュータによる計算だと、なかなか古典論理と同じにはいきません。部分的にしか定義されない述語の計算コンピュータのなかの関数はプログラムにより定義されます。プログラムにより定義された関数の宿命として、無限走行したり例外が発生したりで結果が得られないことがあります。つまり、述語の関数 D→{true, false} は部分関数となります。部分（かもしれない）関数 f:D→{true, false} があるとき、未定義な部…

…をベースにするので、古典論理のシーケント計算とは大きく異なる点があります。シーケントの左右におけるカンマの意味は同じです。右側でも左側でもカンマは「∧」（論理AND）の意味です。さらに、論理ANDは圏のモノイド積と解釈します。以下のような圏を順番に扱います。対応するシーケント計算もそれに従いだんだん複雑になります。 単なる圏 モノイド圏 対称モノイド圏 デカルト圏 デカルト閉圏 単なる圏のシーケント計算圏の対象は、命題 A、 B などで表現します。対象Aに対して恒等射があるこ…

…ついてある程度は知っておく必要があります。このブログ内に、論理の概念／用語の断片的な解説はけっこうありますから、ご興味があれば検索で拾ってみてください。 検索キーワード：古典 論理 検索キーワード：述語 論理 検索キーワード：線形論理 *1:マジメな注：「問題点を他の事情により帳消しにする」のは、現実の世界ではある程度許容されると思います。「遅刻はするが、仕事ができるから許す」とかは普通ですね。「仕事はカラッキシできないが、笑顔が可愛いから許す」となると、微妙な判断ですけど。

…¬）は存在し、意外と古典論理と似た推論が可能です。コンパクト論理におけるシーケントは、論理式が右側だけで左側には何もない形にできます。「演繹系とお絵描き圏論」で触れたゲンツェン／テイト／シュッテ（Gentzen-Tait-Shutte）スタイルの片側シーケント（one-sided sequent）です。右片側シーケントと双対的に左片側シーケントも定義できます。次のような感じです。線形代数における三位一体とシーケント計算コンパクト閉圏、絵算、線形代数、シーケント計算のなかで、多…

…えたんですが、普通の古典論理が無闇と役立ったので、実務論理の話もいいかも。Catyの型推論においても、ある種の演繹系と包含付き圏を使います。と、まー、ネタは割とあるでしょ。 [追記]Takaiさんから許可をいただいている http://www.flickr.com/photos/recompile_net/sets/72157603335973450/ から選ぶなら、次がモニャダラっぽいでしょうか。 [追記]「ストレージの線形代数： 泥臭いデータ操作の洗練された定式化」あたり…

…コレクション）を絞り込む目的に（つまりクエリ言語として）使えます。古典論理とデータ型に関する推論がそのまま素直に使える点がメリットだと思います。 *1:Catyではコレクションではなくテーブルと呼んでましたが、MongoDBの用語「コレクション」のほうがふさわしいと思うので、今後は「コレクション」にしようかと。 *2:LIKEパターンの場合、エスケープ文字が可変なのが困ったところです。 *3:基本述語が全域関数とは限りません。論理式に対するモデルは、一般に部分関数となります。