…判定子 構文抽出子 述語と等式による条件 これは何をやっているのか？ 簡単な事例「高階関数を持たないが型の順序を持つラムダ計算」で出てきたラムダ計算の項を例とします。ラムダ抽象（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は集合の補集合を表します。∧を掛け算、∨を足し算とみなすと、ブール代数…

…値（または4値）論理述語制限も入るので、100%静的に解析可能であることを要求するのはちと無理があります。結局、動的型チェックとトランザクション処理を完全に外すことはできません。いずれにしても、総称（多相）を含めたCaty型システムの意味論を提示しておく必要があるのは確かです。そうでないと、「構文は変えたが意味論は変わらない」とか「意味領域に存在するが、構文ではまだサポートしてない」といった言明の根拠が無くなってしまいます。と、そんな事情で、Catyの総称型システムを手短に、…

…東京都")] という述語ラムダ式になります。この例に限らず、JSONインスタンスで書いた問い合わせは古典論理の論理式に翻訳できます。逆に、“基本述語を原子論理式として組み立てられた古典命題論理”の論理式（集合ブール代数の元）は、JSONインスタンスで表現可能です。ということは、他のいかなる問い合わせ言語と比べてもなんら遜色がないのです。問い合わせコマンドの全体は次のようになるでしょう。 { "gender" : "female", "birth" : { "year" : @…

…の部分集合です。単項述語記号としての「|-」と「|=」の意味左がカラッポの「|-」の意味は既に定義しました。真を表す記号true（特殊な文と考える）を使って次のように定義できます。 |- A ⇔ true |- A 左がカラッポの「|=」の意味は次のとおりです。 |= A ⇔ 任意のM∈Mod(S)に対して、M |= A 「|-」と「|=」は似た記号ですが、左辺を省略したときの扱いが全然違います。この点がどうも歪んでいるように感じます。もちろん、「そういうもんだ」と割り切れば…

…ア・トリプルの意味を述語論理の論理式で書けば、次のようになります。 A{E}B ⇔ ∀x.[x∈A ⊃ (Eval(x, E))∈B] ホーア・トリプル A{E}B 以外に、次の形の命題（論理式）も使います。 A⊆B （A, BはJsonの部分集合） A⊆B の形の論理式を包含関係式と呼ぶことにします。0は空集合、1は特定された単元集合*2を表す定数として使います。次の命題は1つの包含関係式で表せます。 a = b a∈A A = 0 それぞれ： {a}⊆{b} {a}⊆A …

…、「命題論理 vs 述語論理」「構文論 vs 意味論」「古典論理 vs 直観論理」みたいな分け方。いや、僕自身もこのテの分類に依拠しているし、教育コースとして伝統的でもあるんだけど、計算機のハナシだと、ここらへんが混じっちゃうんですよ。「分けたらクリアになる」って側面がないとも言えないけど、そういう分類に労力を使うのはかなりバカバカしい。「論理とはなにか？」で紹介したストラスバーガー（Lutz Strassburger）は、ナントカ論理とかカントカ論とかの区別は捨象した上で、…

…集合へ制限すること 述語を使う方法 ガードを使う方法 レトラクトを使う方法 どこがモナドなの？ Erlangでも引数チェックが必要なときErlangにおけるエラーの考え方と取り扱い方は独特のものがあります（「Erlang実験室：武士道と云ふは死ぬ事と見付けたり」参照）。Erlangでは、原則的にエラー関連処理はしません。しかし、次の点は注意すべきです。 アームストロングも注意してますが、ユーザーインターフェースを経由してくるイベント（人間が起源）や、WebのPOSTデータなど…

…どうかを調べる関数（述語）を defined として、 x.p が定義されていて有効な値を持つなら defined(x.p) は真 そうでないなら defined(x.p) は偽 と約束します。definedを実装しにくいプログラミング言語もあるでしょうが、このdefinedは説明のために使うものと考えてください。基本データ型として integer, number, string, boolean を採用します（JSONスキーマと同じです）。これらの型の名前は、型を判定する関…

…いかどうかを判定する述語（ブール値の関数）です。上の対話例で確認したことを通常の等式で書けば次のようですね。 f:[2]→[3]、i = id[2]、j = id[3] のとき： i;f = f f;j = f しりとりの圏の実装との違いしりとりの圏をJavaScriptで実装したときは、対象は整数、射は文字列でした。整数も文字列もJavaScriptの基本データなので、リテラルで表現できるし、等しさはJavaScriptの「==」で判定できます。今回の有限オーディナルと写像…

…んど常に、命題論理と述語論理は区別されますが、この区別は教育的に有害じゃないかと僕は思っています。構文論（証明論）と意味論（モデル論）の区別もまた伝統的です -- これは区別したほうがいいかも知れない、、、たぶん。論理式にどんな論理記号を許すかも、すごくバリエーションがあります。∧、∨、¬が一番普通でしょうが、⊃（含意）と⊥（矛盾）を採用する流儀もあります。論理記号を1つだけしか使わない体系もできます（これ変態ですけど）。許される推論の多寡＜たか＞によって古典論理と直観主義的…