…数です。束縛機構も、述語論理式やラムダ式と同じです。イプシロン項の意味ε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)) …