…値（または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つだけしか使わない体系もできます（これ変態ですけど）。許される推論の多寡＜たか＞によって古典論理と直観主義的…

…数です。束縛機構も、述語論理式やラムダ式と同じです。イプシロン項の意味εx.(x + 1 = 0) の場合、このイプシロン項が-1を表すことは直観的に明かです（これ以上は詮索しない）。しかし、εx.(x2 = 2) のとき、x2 = 2 であるxは２つあります。どっちを表すのでしょう？ また、xが実数の範囲で動くとき、εx.(x2 = -1) は何も表しません。「xの範囲を複素数まで拡げるんだ」って？ では、εx.(x ≠ x) ならどうでしょう？実は、P(x)がどんな命題で…

…返す関数を論理学では述語と呼びます。ですから、isDefinedは述語です。たぶんもうお気づきでしょうが、述語isDefinedは、examが無限走行すると真偽値を返せません。正確に言えば次のようになります。 exam(n)の計算が正常に停止するとき ⇒ isDefined(n) ＝ true exam(n)の計算の途中で異常事態を認識したとき ⇒ isDefined(n) ＝ false exam(n)の計算が無限走行するとき ⇒ isDefined(n) ＝ ⊥ つまり、…

…、通常、等式的な一階述語論理を枠組みに使います。このとき、ソート（型）を2つ準備します。つまり、対象を表すつもりのObjと射を表すつもりのMorです。例えば基本的な関数記号の“型”（プロファイル）は： dom:Mor→Obj cod:Mor→Obj id:Obj→Mor comp:Mor, Mor→Morこの標準的な方法をやめて、ソート（型）なしでやってみます。つまり、対象と射の区別はしません。すべてが射だといってもいいでしょう。二項関数記号compと二項述語記号compos…

…意味的な区別として、述語とコマンドがあります。 precicate ::= boolean | function command ::= function条件式（論理式）： condition ::= predicate | andExp | orExp | notExp | '(' condition ')' andExp ::= condition '&&' condition orExp ::= condition '||' condition notExp ::= '…

…。例えば、命題論理は述語論理の一部として埋め込めます。∨、∧、¬を使う論理と、⊃と⊥を使う論理は相互翻訳可能です。直観主義論理の証明は古典論理の証明とみなせます。こういった相互関係は、圏（として定式化した論理）のあいだの関手として表現可能です。2つの論理が事実上同じことはよくあるのですが、この事態は、“2つの圏が同値である”という形でうまいこと表現できます。圏の同値性には自然変換が必要なので、系統的な命題の書き換えとしての自然変換も“自然に”出現します。「証明とは何か？」とは…

…命題論理式が文だし、述語論理なら自由変数を持たない論理式を文と考えるのが普通です。自由変数を許した論理式を文と定義することもできそうです。詳細はともかくとして、論理ごとに論理文の集合Sが（そうしようと思えば）確定できることは、あまり異論がないかと思います。ところが、「ならば」に関してはいろいろなレベルの、いろいろな意味を持つ「ならば」が存在します。このことは「さまざまな『ならば』達」で述べました。とりあえず、問題にしている論理が証明論的システムならば証明可能性（以前使った記号…

…「プログラマのための述語論理」でも登場したやつです。 記号 意味 プログラミング言語での記号 ∧ かつ（連言） && ∨ または（選言） || ¬ ではない（否定） ! 論理計算については今特に説明しませんが、二重否定の除去「¬¬p = p」とか、ド・モルガンの法則「¬(p∧q) = (¬p)∨(¬q)」とかは使います。論理式とプログラムの実行文を区別したいので、次の約束をします。 A, Bなどの大文字 -- 文や文の並びなどを表す p, qなどの小文字 -- 条件、論理式を…

…「プログラマのための述語論理」で、暗黙的に“総称的な高階関数”が出現してしまいました。それで今日は、意図的に「Javaで高階関数を扱えるだろうか？ 」とやってみました。結論を先に言えば、ちょっとシンドい。関数オブジェクトまずは、関数オブジェクトを次のインターフェースで定義します。 public interface Function<X, Y> { Y apply(X x); } Functionをimplementsするクラスのインスタンスは、型がX→Yの関数です（そう思いこ…

…「プログラマのための述語論理」は、説明にJavaScriptを使うべきだった（「みにくいアヒルの子 -- コンピューティング・サイエンスとJavaScript」も参照）。技巧的なJavaコードじゃ、分かるものも分からなくなる。手遅れだろうけど、JavaScriptで書き直し。述語の例 function positive(n) { return n > 0; } function zero(n) { return n === 0; } function empty(s) { r…

…み切り。表題どおり、述語論理の入り口を説明する目的があります。それと、ラムダ式もクロージャも高階の型／関数もないようなプログラミング言語（具体例にはJavaを使いますが）で、述語論理のような形式体系をどの程度表現できるかを試してみるのが、もうひとつの目的。それで、「やっぱりJavaみたいな言語はダメだ」と思うか、「けっこう、なんとかなるもんだ」と思うか、… さー、どちらでしょう。[追記]変なJavaのコードでワケワカになってしまうときは、「述語論理はJavaScripを使うべ…

…/ 真偽を返すなら boolean constraintIsSatisfied(Iterable<T1> V1, Iterable<T2> V2); // 違反のとき例外を返すなら void verifyConstraint(Iterable<T1> V1, Iterable<T2> V2) throws Exception;Javaに、for-in文、型総称、イテレータなどが入ったので、比較的自然に「述語論理式→プログラムコード」の翻訳が出来るようになりましたね、めでたい。

…)”など）付きの一階述語を直接扱えるような表明言語が必要となる。しかし、このような概念を採り入れることは言語の性質と守備範囲を完全に変えるだろうし、言語の習得は一層難しくなるだろう -- 実現性や効率の問題はいうもでもない。 さすが、現実主義的ミニマリストのメイヤー先生だ、潔癖にならない妥協的態度がステキ。契約（論理式）で対象を完全に記述しようなんて気張ると挫折するに決まっている、ほどほどが大事！※ 以下では「だ・である」調ホーア式と契約ホーア式（ホーア表明、ホーア制約）は、…

…all()が組み込み述語みたいなもので、論理記号（結合子）「||」で複合した論理式にfoobarという名前を付けていることになります。だから、foobarはユーザー定義述語ですね（fooまたはbarという名前のメソッドが呼ばれるタイミングを定義する述語）。どうでもいいけど、ポイントカットって、ポイントをカットするの？ それ以上切り分けることができない存在物をポイント（点）と呼ぶんじゃなかったかな、…違和感。それはそうとして、アスペクトのコードは、if-then-do、あるいは…

…tryProofは、述語を表現した式と引数を与えると、それから論理的な文を作るんだ。その文、まー命題と呼んでもいいけど、その証明を試みるんだ。」 記者「試みる？」 記者「そう。実際の証明作業は、証明サーバー上で動いている証明エンジンが頑張っている。それで、tryProofは証明エンジンに対して、命題が既に証明されているか、あるいは命題の否定が証明されているかを問い合わせる。」 記者「それだけ？」 ルデーゲ「うん、それだけ。証明エンジンがなかなか応答しないことがあるよ。証明エン…

…になってしまう。 「述語」の意味するところ次は、「述語」という用語に計算可能性は含まれない、という指摘。 述語は意味のある性質であればよく、真偽値を計算する関数が存在している必要はありません。 ウーン。ここは、「述語」という用語自体を取り出して辞書的に定義を与えているワケじゃないのだけど。willStopとかcanProveという関数は、それが実在するかどうかに関わらず、JavaScriptで書かれたプログラムだという流れ／前提で話をしていたのですけど。そうは受け取れませんか…

…ち真偽値を返す関数（述語と呼ぶのでした）は、自然言語では“何かに対する記述／主張”に対応します。例えば、「xは嘘つきです」はxに対する記述／主張です。この文のxに自分自身（私）を代入すると「私は嘘つきです」となり、有名な嘘つきのパラドックスが生じます。（嘘つきのパラドックにも、いずれは触れるつもりですが、とりあえず今日は「そんなのもあるよ」ってことで深入りしません。）●符号化とウロボロスさて、「プログラムを符号化して、その符号が再びプログラムで扱える」という状況を絵に描いてみ…

…lse）を返す関数を述語（predicate）と呼ぶ。 predDefは、述語の関数定義本体（を表す文字列）である。 canProve(predDef, someArg)は、predDefのargをsomeArgで置換した定義（あくまで文字列！）が、ある機械的定理証明系で証明可能であればtrue、反証可能（否定が証明可能）であればfalseを返す。 この状況で、次のコードを考えます。 var cannotProveDef = "if (canProve(arg, arg)) …