一階述語で、定数とか関数の形とかの表現を定義してみる。 数理論理学の教科書などでは、普通はこういう定義だと思う。 定数記号をa,b,c,…とし、変数記号はx,y,z,…、関数記号をf,g,…とする。 このとき項は次のように定義される。 1) 定数記号は項である。 2) 変数記号は項である。 3) fを関数記号とし、t1,t2,…を項とするとき、f(t1,t2,…)は項である。 4) 1から3までで定義されるもののみが、項である。 まず、これを一階述語で書けないのは、いくつ
proverを作っているので、述語論理でproverを定義し、それの証明の様子をみてみたい。 とりあえずの目標としてUnificationをと考えたが、その前に必要なのはSubstitutionであり、そもそもExpressionの定義が必要。 表現(Expression; Expr)と呼んでいるのは当分はf(x,y)みたいなtermでよいと思うけれど、変数と定数の区別は気にしなくてよいだろう。(代入は論理の操作ではないので、述語記号やリテラルなどを区別したり、考える必要
clauseの集合Σが与えられた時、Σの中に存在する可能なすへてのmguの集合M = {<L1:L2>| ∀Li ∈ ∀c ∈Σ}は有限であり、Σからのどの証明もその各stepのmguはこのMのどれかのインスタンス(代入{x←t1} が {x←t2}のインスタンスである({x←t1} ⊑ {x←t2})とはt1⊑t2であること)になっている。 resolutionでは、pairとするclauseごとに共通変数がないことが必要なので、もしも同じ変数が出現していたら話がややこし
Σを論理式の集合(考えているのはclauseの集合でしかないけど)とし、そこに入力、出力の指定/条件をつけくわえると、あるプログラムPの仕様と考えることができるだろう。 このとき、ある入力の値に対して計算結果を得るPの計算過程は、もとのΣのある証明に対応する。対応するというのは、証明から計算過程を機械的につくれるし、計算過程から証明も機械的に作れるという意味でいう。 このような個別の証明は入力の値にそれぞれ存在するもので、決してプログラム自体が証明なのではない。そういう証
レシピを書いていたとき、証明ができやすいように、書き直すということを何度もやった。 ひとつの述語をあちこちで使い回すと、曖昧になり、証明を作るのが難しくなる。それを回避するため、述語をわけて書いてみたりした。 数学で、同じ定理を証明するのにいろいろな方法があるのと、簡単には比較できないけれど、そういうことはあるかもしれない。 証明のしやすさを考えて、述語の使い方を変えるのは、プログラムのアルゴリズムを工夫するのと同じような感覚なのかなと思う。 だとすると、prover
懐中電灯とはなにか?! 懐中電灯を通して、仕様と故障箇所検出について考えてみる。 1. 懐中電灯の目的 懐中電灯の目的は何か? 漠然と言えばそれは「闇を照らす」ことだと思う。 なにか ⇒ 闇を照らす … (1) の「なにか」にあたるもののひとつが懐中電灯と言えるだろう。 (1)には室内灯や街灯や車のライトなども含まれるから、「懐中電灯」と減退したい場合には「持ち歩きができる」という条件をつけるべきだ。 なにか ⇒ 闇を照らす ∧ 持ち運びができる … (2)
ケーキのレシピを述語論理で書いてみようと思う。 ケーキのレシピを調べてはみたものの、作ったこともないし、述語論理で書きやすいように変えているから、本当にケーキを作る人からみたら、これはケーキのレシピではないと言われるだろう。 こういうものを述語論理で書くとこんなふうになるかなという好奇心で書いていることを暖かく見守ってほしい。 料理のレシピは、アルゴリズムのようでアルゴリズムではない。なにかもっとふんわりとして、詳細は調理する人間に任されている何かだと思う。 そういうもの
noteにテキストをコピペすると、改行が無視されて全部くっついてしまう。 かと思えば、文章の塊は空行でブロックに分けられる。 つらい
真夜中に中央公園を通り抜けようと考えたのはなぜだったろうか。 深夜でも公園は取り囲まれているビルの灯りで隅々まで見通せる。タチの悪い乱暴者が潜んで いればすぐにわかるはずだ。それでも、夜の闇の塊はあちらこちらにおちているだろう。そんな公 園を誰が通り抜けようとしたのだろうか。 真夜中に中央公園を通り抜けていったのは誰だろう。 それは公園の向こう側にある託児所に預けていた子供を引き取りに行こうと考えていた誰かかも しれない。託児所の終了時間が迫っていて公園を通り抜けなければ
∀と∃と反証法、1引数の場合 (1)]の続き。 4. Σ2=Σ1 ∪ {-B(3), -B(4), -B(5)}の場合 [述語論理で反証に迷う(1引数の場合) 1]では、1と2の枡についてだけ考えてきたが、最初に、コインが置かれる枠が5つあると書いたのに、1と2以外の枠については何も触れてこなかった。コインを頭に思い浮かべているならば、暗黙のうちに{-B(3), -B(4), -B(5)}は前提となっていたかもしれない。 暗黙にそう思っていたとしても、 Σ1 ⊢ -B
述語論理でResolutionを使う場合、命題論理と同じく反証法(refutation)を用いることになる。そこで、述語論理で新しく登場した∃xや∀yを含むconjectureについて、どういうことになるのかを考えてみる。 最初は1引数の述語の場合について考える。 次のような状況であるとする。 例) 黒いコインを2枚を、5つの(1から5まで番号がついている)枠に適当に置いて、それをセンサーで識別する。センサーはその結果をFactとして論理式を作り出力する。たとえば
Unificationは2つの式(論理式や項)から、代入mguを計算するアルゴリズムである。 以下に示す例では、x, y, zは変数、a, b, cは定数、f, g, kは関数記号とする。 2つの式とmguの例) t1,t2 を式として、<t1:t2>でunificationした結果のmguを表す。 (1) <a : b> : unifyできない (2) <f(a) : g(b,c)> : unifyできない (3) <x:b> = {x←b} (4) <f(
Resolutionでは、Unificationによってmguという代入を作るが、Resolutionで用いる代入はすべてこのmguである。2つのclausesが共通の変数を持たないように、変数名を付け替える操作で代入を使う場合は、別の方法で作ることになるが、以下の話ではそれは気にしなくていい。 まず、表現(式)に代入を適用する操作を次のように定義しておく。 代入表現 代入は、siが記号(定数や変数)で、eiは表現(式)であるとして、 {s1←e1, s2←e2, …
矛盾については命題論理だけで話ができた。 ここでは、述語論理のresolutionについてまとめたい。 命題論理のresolutionでそうだったように、2つのclausesからresolventを作るという形式は述語論理でも変わらない。 見た目の違いといえば、命題論理ではPとかQとか書いていたことを、述語論理ではP(x,y)とかQ(f(a))とか引数をもつ表現まで拡張するところだろうか。 このようにxとかyという変数も使えるようになる。 変数については、限量子と呼ぶ
Relational Database(RDB)は関係に基づいているので述語論理と関係が深い。少し論文を探したが、その関係をはっきりと書いたものが見つからなかったので覚書として少し書く。探し方が足りないとか、自明だから書かれていないとかいう話なのかもしれない。あるいは演習問題にあるとか。 RDBについてそんなに深い知識がないので、おかしなところもあるんだろうな。 RDBでは表の列に名前をつけるが、それは述語の引数に名前をつけるようなもので、二つの方法をお互いに変換できるの
例3) ボールの運動の述語論理での記述 ここでは運動について考えてみたい。 あるボール(色は白い)が、定規(0から9まで目盛がふってある)の上を運動をすることを考える。 その様子を定規の横に並行に並べられた10台のセンサー(S0からS9と名付ける)で観測する。 動画は扱わなくて、1秒に一回光を当て、センサーはそのときの静止画から、ボールが目盛のどこにあるのかを観測する。 実験の概念図 ⚪—-→ ボール +---+---+---+---+... 0
