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

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

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

参照用 記事

古典, 論理 の検索結果:

離散キューブ: 特に0次元と(-1)次元の話

…e ⇒ xi∈Z) 古典論理における含意〈ならば〉の扱いは、前件(⇒の左側)が偽ならば真になるので、 ∀i.(True) となり、定義の右辺は真です。 x∈R0 が格子点 :⇔ True R0に含まれる点はいかなる点も(実際は一個しかないが)格子点です。格子点の定義をε-格子点にしたところで、やはりいかなる点もε-格子点です。J0 = R0 であり、唯一の点が*だったので、*(0と呼んでもいいが)は格子点です。([追記]以下の「内部の点かどうか」の議論は、位相が絡んでいるので…

確率的論理のバリエーション

…論理で、構成の手法は古典述語論理に似ています。PS論理は、それとはちょっと別な原理と手法で構成されます。'PS'は確率空間〈probability space〉のことです。PS論理の意味論〈モデル〉は確率空間の圏で与えられると考えます。つまり、propositions as probability spaces というモットーです。PSを、確率空間を対象として確率保存マルコフ核を射とする圏とします。構文とモデルを区別せずに、PSの対象(つまり確率空間)をPS論理の“命題”と呼…

限量子と代入、ベック/シュバレー条件

…について説明します。古典的真偽値の集合を B = {0, 1} とします。0は偽で、1は真を表します。0 < 1 という順序を入れておきます。Pred(X) := Map(X, B) と定義します。Pred(X) は集合X上の述語〈命題関数〉の集合です。Pred(X) に所属する述語達を考えるとき、Xを論域〈domain of discourse | 議論の領域〉と呼びます。述語の“主語”となのるのは、論域の要素です。Pred(X) は順序集合になります。順序集合は自然に圏と…

確率論のカリー/ハワード/ランベック対応

…いので、通常の論理(古典論理)に比べれば単純で小さい論理です。単純型付きラムダ計算は、静的で強い型システムを持つ関数型プログラミング言語だと思えばいいです -- と言っても分かりにくいですね。現存する実用的関数型プログラミング言語の原型となっている計算系ですが、メチャクチャに単純・小規模なものです。型の構成法として、直積型〈ペア型〉と関数型〈指数型 | アロー型〉が使えます。この2つの理論体系は同一の構造を持ち、双方向の同型対応があります。連言含意論理と単純型付きラムダ計算が…

日常論理の数理論理

…」と言える推論でも、古典論理からみて間違っていることはあります。むしろ、古典論理では間違っているとされる(許容できない)推論が興味の対象です。タイトルは「日常論理“と”数理論理」ではなく、「日常論理“の”数理論理」です。つまり、数理論理として日常論理を扱いたいわけです。ただし、数理論理の常套手段が通用しないところもあるので、そこは変更します。それでも、態度・スピリットは数理論理のそれを踏襲します。日常論理を扱うからといって、人間の認知や行動を分析しようなんて気はサラサラありま…

多相関数と型クラス

…な等式で書くより、(古典論理の)論理式を使ったほうが楽です。論理式を使うときは、キーワード condition を先頭に置くことにします。 signature Monoid in Set { type U function m:U×U -> U function e:1 -> U condition lunit_cond : ∀x∈U.( m(e(1), x) = x ) condition runit_cond : ∀x∈U.( m(x, e(1)) = x ) condi…

多相関数の「パラメトリック性 vs 満足性」

…ここでは、常識的な(古典論理の)論理式を使うことにします。論理式の文法は知られていますが、「lengthらしさ」を記述するための基本語彙〈ボキャブラリー〉が必要です。基本語彙の定義には指標〈signature〉と呼ばれる形式が使われます。以下が、「lengthらしさ」を記述するための基本語彙を定義する指標です*1。 signature ListAndLength{ type X in Set function nilX : 1 -> List(X) in Set functi…

簡約多圏とシーケント計算

…ェンのオリジナルの(古典論理)シーケント計算は難しすぎるので、単純化して二項論理演算はひとつだけにします。そのように単純化した論理を総称してコンパクト論理と呼びます(ジラーは「コンパクト論理」と呼んでたと思うけど、一般的な言葉ではないです)。コンパクト論理の意味論は、唯一の二項論理演算を圏のモノイド積と解釈して遂行できるのではないか? と期待できます。コンパクト論理のシーケント計算 -- コンパクトシーケント計算であっても、意味論構成には多圏が必要そうです。やっぱり難しい! …

対称モノイド多圏(簡約版)

…足] 論理で出てくる古典論理のシーケントでは、矢印の左側のカンマと右側のカンマの解釈が違います。簡約多圏のシーケントでは、左右のカンマの扱いに違いはありません。簡約多圏のシーケントはより単純なシーケントなので、コンパクトシーケント〈compact sequent〉と呼ぶのが正確です。が、コンパクトシーケントしか出てこないので、単にシーケントで済ませます。 [/補足]多射fのシーケント〈プロファイル〉 (A1, ..., Am)→(B1, ..., Bn) は、混乱の恐れがなけ…

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

…ate〉と呼びます。古典論理で使っている述語はこのタイプの述語です。決定性述語の全体を Φ{0, 1}X と書きます。下付きの [0, 1] と {0, 1} は判読しにくいのでご注意(別な記法にしろってハナシはある)。 指示関数=指示述語 A∈ΣX に対して、χA:X→R を指示関数〈indicator function | characteristic function | 特性関数〉とします(文字'χ'はギリシャ文字カイ)。確率論では、別な意味の特性関数があるので、「指…

多様体の圏上の計算デバイス: 表示オペレータ

…参照してください。 古典的微分幾何・ベクトル解析のモダン化: 局所座標って何だ? 「接バンドルのホロノーム座標」のときと同様に、チャート〈局所座標〉は、x:M⊇U→Rm という部分写像だとみなします。部分写像の定義域は常に開集合だとします。部分写像の扱い方については、「快適な微分計算のための圏と微分公式 // 部分逆写像」も参考になるかも知れません。概ユークリッド空間と部分写像の圏多様体とみなしたRnをユークリッド空間と呼びます。多様体Xが、多様体としてユークリッド空間と同型…

前回記事への訂正・補足: 情報多様体の幾何

…です。期待多様体は、古典的な情報幾何の対象物、あるいは「各点が確率分布である多様体」のことです。期待多様体のリーマン計量は、フィッシャー情報計量〈Fisher information metric〉になります。情報幾何の起源とも言える計量です。共役接続ペア(の族)を作る場合も期待値を使います。期待値が関与するということは、パラメトリック統計モデルの文脈のなかで期待多様体が登場することです。純粋な幾何的文脈では期待多様体を定義できません。僕が、「多様体と確率・統計: 情報幾何の…

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

…性の」「二値的な」「古典的な」などに置き換えられます。そして、決定性/二値的/古典的であるシャープな世界Finは、そのままファジーな世界Chanに埋め込むことができるのです。この事実は、シャープな世界からファジーな世界への引っ越しの不安を緩和するものでしょう。述語の外延化pがA上のシャープな述語のとき、S = {x∈A | p} という集合が、述語pの外延〈extension〉として決まります。外延とは、述語pが表す性質を持つモノの全体の広がりのことです。集合Sからみたとき、…

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

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

今井健男さんの「計算機科学から見たディープラーニング」

… と解釈して、通常の古典論理の論理式に翻訳するなら: ∀x∈S.( P(x) ⇒ Q(C(x)) ) 今の説明は、あくまで従来型のプログラミングでのこと。ディープラーニングでの状況となると、プログラムコードCというのがハッキリしません。状態空間Sの確定も簡単ではないでしょう。古典論理やその変種をそのまま使うわけにもいきません。真偽がTrue, Falseの二値で決まるような世界ではないですから*6。先に「ホーア論理に始まりホーア論理に終わる」と言いましたが、「ホーア論理がすべ…

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

…条件記述の論理式は、古典一階述語論理をそのまま使えばいいでしょう。古典一階述語論理は、極めて安定した基盤です。素直に古典一階述語論理を使えば問題はありません。ただし、古典一階述語論理は計算の効率は芳しくないので、その点の考慮や工夫は別途必要です。関係とはデータベースにおいて主題的に考えるべき論理式は、“関係の性質”や“関係のあいだの関係”を記述する制約記述の論理式です。制約記述の論理式に関しては色々と問題がありますが、最大の問題は、制約記述の論理式に意識が向けられてないことで…

前層とフィルター

…デル論 2006年 古典論理は可換環論なんだよ 補足記事: “古典論理=可換環論”の計算と種明かし 補足記事: イデアルと論理 番外の補足:ベキ等元と連結性 2013年 超フィルター(ultrafilter)って何なんだ: 点? 確率測度? 前層と余前層位相空間X上のC値前層とは、Open(X)op→C の形の関手です。Open(X)上で定義された反変の関手になります。共変の関手 Open(X)→C のほうは、(C値の)余前層〈copresheaf〉とか前余層〈precosh…

論理式の集合とは何か?

…は、一番ポピュラーな古典論理を使うことにします。基本記号を全部挙げる目的と論理が決まったら、使う記号をすべて列挙します。このとき、記号を分類するガイドラインが役に立ちます。 定数記号 変数記号 演算記号〈関数記号〉 述語記号〈関係記号〉 論理記号〈論理結合子記号と限量子記号〉 補助記号 説明は後にして、各種の記号を並べてしまいます。 定数記号: '0', '1' 変数記号: すぐ下で定義する 演算記号: '+', '*' 述語記号: '=', '≦' 論理記号: '∧', '…

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

…は、計算の論理*1は古典論理(または直観主義論理)で十分でしたが、量子現象/量子計算に関わる論理は古典論理とはどうも異なるようです。量子を扱うための非古典論理が必要なんでしょう。クリス・ヒューネン〈Chris Heunen〉のこの本は、量子計算論とそれに関わる論理を基礎的〈foundational〉な立場から解説しています。具体的な量子アルゴリズムや応用事例は少数しか載ってません。紙幅のほとんどを基礎に費やしているからです。基礎的であることは易しいことを意味しません。実際、こ…

ポンプの補題とその使い方: 回文の例

…のままです。[/追記] *1:間違いを具体的に指摘するのが目的ではないので、URL参照はしません。 *2:画像: https://ja.wikipedia.org/wiki/手押しポンプ#/media/File:WellPump.JPG 神戸市市東灘区石屋川の公園にある井戸ポンプ *3:形式言語理論/数理言語学も言語学の一部門と考えるなら、今は数理的なアプローチしか考えない、ということ。 *4:厳密には、論理式を古典論理のシーケントの形に書いたときに、移項の原理が機能します。

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

…きないけど)。論理(古典論理*1)では、「Aである」と「Aでなくはない」は完全に同じです。日常言語の微妙さ・煩雑さを切り捨て、理想化・単純化することにより、強靭な推論能力が手に入るのです。日常言語を使っているかぎり、日常の論理、あるいは日常の非論理が混ざり込むことは避けられません。論理的推論のための人工言語を使うのが望ましいでしょう。そこで、プログラミング言語TypeScriptを(かなり無理クリに)使って、論理的命題の記述を試みてみます。本文中の例題を実行してみたい方は、最…

カッコイイけど使える線形代数とは?

…モダン化ここ最近、「古典的微分幾何・ベクトル解析のモダン化」というシリーズ記事を書いています。この一環として、古式テンソル計算のモダン化をやりたいな、と思っています。古式テンソル計算ってなに? -- 古いスタイルの(古典的、古式)微分幾何・ベクトル解析には、通常の(オーソドックスな)線形代数とはだいぶ違った線形計算体系が付属しています。これを、古式テンソル計算〈old-style tensor calculation〉と呼ぶことにします。上下の添字をあやつって計算する職人ワザ…

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

先日の記事「古典的微分幾何・ベクトル解析のモダン化: ダイレクトインデックス記法」で、上付き・下付き添字の説明をしたのですが、説明の対象である上付き・下付き添字以外に、上付き・下付き添字の記法を大量に使っている事実に気が付きました。随分とひどいオーバーロード〈多義的使用〉だわ。「過度のオーバーロードはやめよう」と主張している僕としては、ちょっと愕然としました。僕自身が上付き・下付き添字をどんな目的で使っているかを解説することにより、反省の材料にしたいと思います。また、「古典的…

双対ベクトル空間、これくらい知ってればイインジャナイ

…ダ記法に関しては、「古典的微分幾何・ベクトル解析のモダン化: ラムダ記法の利用 // 入力型と出力型を持つ型付きラムダ記法」をみてください。 (A・) := λx∈Mat(1, n).(A・x : Mat(1, m)) (・A) := λy∈Mat(m, 1).(y・A : Mat(n, 1)) (A・):Mat(1, n)→Mat(1, m) と (・A):Mat(m, 1)→Mat(n, 1) を組み合わせると、 ((A・), (・A)):(Mat(1, n), Mat(…

距離空間と位相空間と連続写像

…たことがあります。 古典論理は可換環論なんだよ (2006年) 一方で、我々が常識的に想定する「空間」は距離空間なので、距離から導かれた位相はやはり重要です。距離から導かれる位相の特徴付けは熱心に研究された課題で、幾つかの距離化定理〈metrization theorems〉があります。距離は、色々な位相空間の例を提供してくれますが、距離では定義できない位相空間もあります。距離と無関係な位相空間にも目を向けましょう、というお話でした。 *1:これはこれで、全開〈フルオープン〉…

指数関手と構文論・意味論

…言い方は、連続関数の古典的な定義とのアナロジーからです。 FがΦ-連続 ⇔ ∀Q∈Φ.( F(Lim(D:Q→C)) Lim(FD:Q→D) ) Limは図式(あるいは関手)の極限対象を取るオペレーターです。上記は共変関手の連続性でしたが、反変関手の場合は、余極限を取るオペレーターColimを用いて次の形に書いたほうが分かりやすいでしょう。 F(Colim(D:Q→C)) Lim(FD:Q→D) 反対圏を使えば、極限だけで話を済ませることができますが、共変・反変を区別する場合…

集合の宇宙論

…りませんけどね。一階古典述語論理の上の公理系としてのZFC集合論のモデル(意味的世界)をVとします。Vって何なんだ? にうまく答えることは僕にはできません(苦笑)。ともかく、したいことは何でもできる環境として、Vがあると思ってください。VをZFC宇宙と呼びます*2。ZFCの宇宙Vが一意的に存在するのかというと、そうでもないようです。ZFC集合論からは決定できない命題Pがあれば、Pが成立する宇宙とPの否定が成立する宇宙は別物です。しかしどちらもZFC集合論のモデルになれます。こ…

データベースとカン拡張と思い出

… after 量子と古典の物理と幾何@名古屋 @名古屋からスペースハイブのプレTQFTへ 僕が2007年から顔を出すようになった圏論勉強会は、さかいさんが主催者エライ人なのでさかい勉強会と呼びましょう。さかい勉強会は、「さかいさんが学部学生の頃から始まった」とたけをさんから聞きました。僕のこのブログ内での言及は2005年3月にあります(「なんと、圏論記事への言及が」)。さかいさんの「ヒビルテ」のアーカイブを探すと2005年10月に「第十回圏論勉強会」への言及があります。という…

現場の集合論としての有界素朴集合論

…べと言われれば、一階古典述語論理を選ぶ人が大多数でしょう。一階古典述語論理(first-order classical predicate logic/calculus)は、完成度が高く使いやすく強力な推論能力を持っています。一階古典述語論理を実際に使うときは、プレーンな体系ではなくて、定数記号/関数記号/述語記号/公理/推論規則を足してカスタマイズしてから使います。例えば、自然数の理論を展開したいなら、定数記号'0'、1変数関数(単項演算子)記号's'、2変数述語(2項関係…

奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか

…明がおかしい 3. 古典論理の定義を間違えている 4. 集合と集合論、述語と述語論理を混同して使っている 5. 二階論理の説明がおかしい 消極的提案: 第2章を削除する 積極的提案: 述語論理を活用した解説 奥野さんの発想の源泉(ただし想像) 「矛盾」て何なんだろう? 演繹データベースと矛盾: 奥野さんは(まーまー)正しかった 演繹データベースで出来ること 述語論理をチャンと使おう 外部世界をチャンと考慮しよう おわりに ことの発端: zhanponさんの批判先日、次のQii…