…ばれるモノは、命題、述語、条件、真偽値、プロパティなどとも呼ばれます。そのようなモノを扱う計算が論理計算です。論理計算の舞台となる代数はブール代数やハイティング代数ですが、もう少し弱い構造として、論理半環（logical semiring）を定義します。「論理半環」は一般的な用語ではありませんのでご注意。論理半環の足し算（論理和）を∨、掛け算（論理積）を∧で表し、足し算と掛け算の単位元はそれぞれ0と1とします。論理半環はその名のとおり半環ですが、次の条件を加えます。 足し算が…

…論理で言えば、A上の述語（の意味）の全体です。埋め込み A→{0, 1}A の像は、離散的なディラック関数とでも呼べるものです。a∈A に対して： δa(x) = if (a = x) 1 else 0 a|→δaの対応を、同じ記号δを使って δA:A→{0, 1}A と記します。ところで、{0, 1}Aは、{0, 1}のA回の直積とみなせます。{0, 1}に離散位相を入れて、{0, 1}Aに直積位相（無限直積かもしれない）を入れれば、{0, 1}Aは位相空間です。そしてチコ…

…で、これは命題論理と述語論理を繋ぐものです。射影に対する随伴としての定式化もできます。また、存在限量子と全称限量子というペアが存在しますが、これも随伴の枠組で説明できます。となると、積分の周辺にもなにか随伴が潜んでいるのでしょうか？ 超フィルターモナドを生成する随伴は位相的に構成できますが、ジリィ・モナドに対応する随伴はどういうものでしょう？論理にはモデル論（「コンパクト空間と論理／モデル論」参照）、さらにはインスティチューション（抽象モデル論）がありますが、確率におけるイン…

…結果です。pを二項の述語（真偽値を値とする二引数の関数）だとして、ジョインJ（の集合）は次のように書けます。 J = {(s, t)∈S×T | p(s, t) } 二項の述語 p(s, t) として最もよく使われるのは、フィールド（カラム）値の等式です。「レコードsのフィールドfの値」を s.f と書くことにすると、s.f = t.g のような等式ですね。この場合のJは： J = {(s, t)∈S×T | s.f = t.g } この形のジョインは等値ジョインと呼ばれるこ…

…atural という述語で表現します。 /** テストサンプル */ command test-sample :: void -> Logical { [ [true, false, false, true], [4, 5, 6, 7] ] | zip-is-natural "to-string" "num:inc" }; この事例では、4つの対象A, B, C, Dには次のように型（集合）が代入されます。 A = boolean, B = integer, C = stri…

…作るときに必要になる述語（predicate）や関係（relation）も定義しています。 /** 集合の包含関係 */ function s_included(a1, a2) { return a1.every(function(item) {return (a2.indexOf(item) > -1);}); } /** 集合の共通部分 */ function s_intersection(a1, a2) { // 重複は除外されない return a1.filter(f…

…「複合データ構造への述語適用」の部分は説明なしだとちょっと分かりにくいかも。[追記]説明してない「複合データ構造への述語適用」のArrayCloseとObjectCloseが間違っていたので修正しました。まったくいらんことをしてましたね。 function ArrayClose(x, parr){ return ArrayOpen(x, isUndefined, parr); } function ObjectClose(x, pobj){ return ObjectOpen…

…推測できるでしょう。述語論理で出てくる限量子（量化子）は束縛子の例です。より具体的には、全称限量子∀と存在限量子（特称限量子）∃は束縛子です。これらの記号は、直後に変数を伴って、その後に続く論理式内の変数を束縛します。∀x.F、∃x.F のとき、論理式F内の変数xは束縛変数になります*1。自由変数を含む式に構文的に作用して、自由変数を何らかの意味で束縛する記号的作用素が束縛子ってことになります。もうひとつ典型的な束縛子はラムダ記号λです。λx.E によって、式E内の変数xを束…

…は辛い作業」を人間に代わって片付けてくれるのです。メタプログラミングにより、親切で勤勉な妖精さんを創りだすことができます。レイフィケーションとメタプログラミング、それにより創り出された妖精さん達は、ゲーデルの発想からの派生物のなかでもとても実利的なものだと思います。 *1:このときの説明は、概念的には少しSmalltalkっぽくて、記法はJavaに近いものを採用しました。 *2:isCode(n) という述語があって、この述語が真である領域上で定義された部分関数なら十分です。

…判定子 構文抽出子 述語と等式による条件 これは何をやっているのか？ 簡単な事例「高階関数を持たないが型の順序を持つラムダ計算」で出てきたラムダ計算の項を例とします。ラムダ抽象（lambda abstraction）の構文をBNFで定義してみると： Abst ::= 'λ' LambdaList '.' Expr ここで、'λ' や '.' に絶対的な必然性があるわけではなくて、次のようでもかまいません。 Abst ::= 'lambda' LambdaList '->' E…

…alse, ⊥} として圏TotPtRelの対象と考えることもできますから、否定を使った計算を排除しているわけではありません。ですが、A上の述語 A→Ω は、結果を出さないこと（結果が⊥）もあれば、どっちつかずの値（{true, false}、{true, false, ⊥}）となることもあります。集合圏Setや関係圏Relに比べると、圏TotPtRelはヤヤコシイ面があります。しかし、このヤヤコシサが現実を反映しているのだとすれば、より精密なモデルなのだとも言えるでしょう。

…ゼロかどうかを調べる述語isZeroが前もってあるとして、これらを使って自然数の普通の足し算を定義しましょう。succ(n) のような関数形式ではなくて、n.succ のようなメソッド風の記法を採用します（左から右に読めるように）。代入の記号は「:=」とします。 def (n, m).add is { p := m.isZero; branch { p then n, not p then (n, m.pred).add.succ } } JavaScriptで普通に書くなら…

…の場合の係数域は論理述語のブール代数、非可換の場合の係数域は自己遷移の非可換半多元環となり、かなり違った様相を呈します。論理述語のブール代数が、自己遷移の半多元環のなかに（対角Δに含まれる遷移として）埋め込めるので、お互いに関係付けることはできますけどね。あと、それから…フレーム付き双圏の双加群とは別なタイプの例として、コボルディズム圏があります。1セルがコボルディズムで、左フレームが始境界、右フレームが終境界です。2セルは、コボルディズムのあいだの幾何的写像で、境界を境界に…

…、論理式を作るには、述語記号や関係記号を決める必要があります。型の議論では、「値がある型を持つ／値がある型に所属する」という主張が基本的なので、所属関係を表す記号「∈」を導入します。「∈」は集合に関して使う記号ですが、Sets-as-Typesの立場なので、型と集合は同一視してもかまいません。気になるようでしたら「:」に置き換えて読んでください。述語・関係記号が二項関係記号「∈」だけで、左に項（値の項）、右に型項を置く規則（構文的な制限）なら、原子論理式は、「項∈型項」という…

…べます。その後、高階述語論理に少し触れます。 前回のエントリー：型推論に関わる論理の概念と用語 その1 シリーズ目次： その1 その2 その3 その4 その5 その6 番外（型理論ってば） 型推論の話についていけない事情型推論について調べたり勉強したりしようとすると、ゴチャゴチャしていてメンドクサイんですよ。同義語／類義語が無闇に多くて、人によって言葉の使い方が違うのです。そうなると、書かれたモノを読むときの負担が大きくてイヤになっちゃう。きちんとした教科書なら定義もちゃんと…

…に言うと、命題論理と述語論理の境界を引くのもあまり意味がないと思います（「論理とはなにか？」も参照）。型理論では型が対象物なので、型を表す式が型項、型に関する主張や判断を表す式が型論理式、または型命題ということになります。型項（type term）を type expression と呼ぶことは多いのですが、これを直訳すると「型式」、「ケイシキ」と読まれちゃうので、僕は「型表現」を使うことがあります。型表現と型項は同義語です。項の構成法項は次のような素材から組み立てます。 定…

…、軸、ノードテスト、述語（predicate）という3つの部分からなり、次の形です。 軸::ノードテスト[述語] 述語は条件式です。ノードテストも条件式ですが、頻繁に使う条件をノードテストにしたって感じですね。述語が不要なら、正式記法であってもブラケットごと省略可能です。「XPathの要点を少し抽象的にまとめておく」で述べたように、軸はコンテキストノードを受け取り、全順序付きノードセットを返す関数です。13種の軸があります。略記の方法も付記して軸の名前を列挙すると： ance…

…、軸とノードテストと述語（predicate）からなります。ステップは、コンテキストに対して評価されます。ほとんどの場面でコンテキストノードセットは使われず、コンテキストノードだけで計算ができますが、述語（predicate）の評価のときに、コンテキストノードセット内の順序（position）が使われます。与えられたコンテキストを (C, x) とします。ステップの軸がaなら、a(x) は全順序付きノードセットです。ノードテストと述語は、a(x) の部分ノードセットを選び出す…

論理に出てくる述語（predicate）をコンピュータの文脈で考えると、適当なデータ領域Dの上で定義され、真偽値（trueまたはfalse）を戻り値とする関数になります。述語を数学的な関数と捉えるなら、その論理計算は古典論理と同じようにできます。しかし、コンピュータによる計算だと、なかなか古典論理と同じにはいきません。部分的にしか定義されない述語の計算コンピュータのなかの関数はプログラムにより定義されます。プログラムにより定義された関数の宿命として、無限走行したり例外が発生し…

…グ言語PLで書かれた述語（boolean値の関数）だとします。PLで書かれた関数は、LLのなかの関数記号にバインドしていいのでした。同じ記号somePredicateをLLの関数記号（述語記号）としても使ってしまいます。データ領域Dの具体的なデータaを取ってきて、somePredicate(a) をLL内で考えると、これはLLの命題です。この命題をAと置いてみれば： A ≡ somePredicate(a) もし、命題Aのコード化がデータaだとすると、これは次のような意味を持…

…operties）、述語（predicates）でしょう。一番分かりやすい例は、P(A) = Pow(A)（ベキ集合）です。いずれにしても、property, predicate, powerですから頭文字は'P'。以下では、P(A)を真偽値の集合だと考えます。真偽値とは言っても二値とは限らず、正しさの度合いを測る何らかの量のことです。真偽値の集合はブール代数やハイティング代数*1の構造を持ちますが、ここではとりあえず順序集合と考えます。つまり、P(A)は順序集合の圏Ordの…

…割り算の余り /* 述語／関係の命令 */ var EQ = 20; // スタックトップと二番目が等しいかどうか var LT = 21; // スタックトップ ＜ 二番目 かどう /* 論理演算の命令 */ var AND = 30; // 論理アンド var OR = 31; // 論理オア var NOT = 32; // 論理ノット /* 流れ制御の命令 */ var $$$ = 40; // ラベルを付ける var JMP = 41; // ラベルの場所にジャンプ…

…の命令 定数の命令 述語／関係の命令 論理演算の命令 流れ制御の命令 ブロックスコープと変数の命令 スタック操作の命令 ネイティブ関数呼び出しの命令 その1 その3 サンプル RAC1の特徴RAC0は、単に算術式の評価ができるだけでしたが、RAC1には次の機能を持たせます（その予定）。 変数を使える。 制御構造を持つ。 整数以外に真偽値（boolean）もデータとする。 JavaScriptにより機能を拡張できる。 変数に関しては、ネスト可能なブロックスコープを仮想機械のレベ…

…、値ではなくて集合（述語と言っても同じ）を入出力仕様に使って、型推論も行えたらいいなー、とか少し期待してます。例えば、式Eと式Fのパイプライン結合に関する推論規則は次のようですが、値x, y, zを条件に変更するようなことです。 Σ; x {E} → Γ; y Γ; y {F} → Δ; z -------------------------------------------[comp] Σ; x {E|F} → Δ; z x, y, z を P, Q, Q', Rという条…

…領域A上で定義された述語（真偽値を値とする関数）の集合だと解釈するとわかりやすいでしょう。H(A, B) に含まれる3つ組 (p, f, q) は p{f}q と書きます。p{f}q と書いたら、(p, f, q)∈H(A, B) を暗黙に仮定します*1。p{f}q の意味は「x∈A が p を満たすなら、f(x) は q を満たす」と解釈すると、確かにホーアトリプルだと思えます。もちろん、この解釈は説明のための一例であり、仕様構造の定義は公理的に与えられます。圏C上に仕様構…

…では、言葉（定数項や述語記号）を定義しても、その形式的体系の能力に何の影響もありません。定義をたくさん導入した後で、それらの定義を駆使して証明した命題は、追加の定義が一切無い元の体系でも証明できます。高級言語でプログラミングして出来る計算は、機械語だけでも書けるようなものです。あるいは、(let x := E in F) というlet式を考えてください。このlet式は、事前にxを定義してそれから（xを含む）式Fを評価しますが、実際は (λx.F)・E と同じです。(λx.F)…

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

…で定義された単項基本述語*3をもとにして、述語論理の論理演算（AND, OR, NOT, ∀, ∃）を使って組み立てた論理式の体系になっています。JSONの複合データ構成法である配列構成とオブジェクト構成にも対応しています。これは、JSONインスタンスからなる集合を定義する論理式の言語となっており、与えられた集合（コレクション）を絞り込む目的に（つまりクエリ言語として）使えます。古典論理とデータ型に関する推論がそのまま素直に使える点がメリットだと思います。 *1:Catyでは…

…かというと、「条件（述語、性質）、部分集合、ヴァリデータ、ベキ等射、EPペア」などがよく似た概念なので、条件をもとに作った拡張圏も、ベキ等射をもとに作った拡張圏も似たりよったりということです。メイヤーのCommandとQuery（教えに背く）バートランド・メイヤーは、2種類の望ましいメソッド種別を提唱しています。オブジェクト指向のクラスを、状態空間Sとその上の写像としてモデル化します。オブジェクトのある時点での状態は、Sの一点で表現され、オブジェクトの振る舞いはS上の運動（通…

…す。このような関数を述語（predicate）とか性質（property）とか呼びますが、ここでは条件とか命題という言葉を使います。pがS上の条件であるとき、条件を満たす点の全体はSの部分集合になります。それを [p] と書くことにします。 [p] = {s∈S | p(s) = 1} 次の法則が成立します。 [p∧q] = [p]∩[q] [p∨q] = [p]∪[q] [¬p] = [p]c 上付きのcは集合の補集合を表します。∧を掛け算、∨を足し算とみなすと、ブール代数…