一階述語論理
Menu論理とは言葉で表せること、その関係、特に、仮定から導かれる正しいことを表すものである。論理式には変数があり、変数の値が決まると論理式の真偽が決まる。
正しいと仮定する論理式、あるいは、それ自身で真とわかる論理式は公理と呼ばれる。いくつかの論理式の真偽から、別な論理式の真偽を決める推論規則というのを決める。そうすると、公理から推論で得られる真である論理式の集合が得られる。
例えば、1 = 1 は、それ自身正しい論理式である。変数X を使って X = 1 とすると、X の値が 0 に決まると X = 1 は偽となる。X = 1 から、X + 1 = 2 を推論するような規則を与えることができる。
論理式の作り方
論理は、まず、＊ 論理式の構文
を定義する。これは話言葉、書き言葉の文法に相当する。構文は、BNFなどの文法規則で定義しても良い。
それから、その構文の意味を定義する。この意味は構文要素に対して、日常言語で与える。「こういう意味にしよう」ということである。
構文要素には変数というものがあり、構文要素の変数に対応する値が対応する。ここでの値は、やはり日常言語で与える。
変数と構文の構築に沿って、論理式の意味を定める規則を決める。これにより、すべての変数の値が決まった論理式に対して真偽が定義される。
constant : 'a' | 'b' | 'c' ;
variable : 'X' | 'Y' | 'Z' ;
function-name : 'f' | 'g' | 'h' ;
expression : constant | variable | funciton | expression , expression ;
function : funciton-name '(' expression ')' ;
例えば、a は定数。X は変数。f(a,X) は変数X を含む関数になる。g(h(a)) のように入れ子にしても良い。= の様に両側に引数を置くようにしても良い。定数は引数のない関数と考えても良い。
X = a
たぶん、定数はもっとたくさんあるが、ここでは、a b c しか使わない。
次に、論理式を定義する。
predicate-name : 'p' | 'q' | 'r' ;
predicate : predicate-name | predicate -name '(' expression ')' ;
引数がないもの許そう。 p,q(X),r(a,X),q(f(X)) などが述語になる。
述語は論理記号によって結合される
logical-statement : predicate
| logical-statement '∧' logical-statement
| logical-statement '∨' logical-statement
| '¬' logical-statement
| '∀' variable '=>' logiccal-statement
| '∃' variable '=>' logiccal-statement
| '(' logical-statement ')'
;
それぞれ、「かつ」「または」「でない」「すべてのXで」「あるXで」の意味になる。必要があれば()を用いる。
さらに、
logical-expression '→' logical-expression
を、
'¬' logical-expression '∨' logical-expression
として定義する。ここで、
p → q → r
は、
p → ( q → r )
とする。
さらに constantを表す変数C,D 、logical-expression を表す変数P,Q,R を使う。これは logical-expression には含まれない。
Agda で書いてみる
この授業は Agda でやる授業なので。なるべく、さぼろう。data で構文を定義していく。これは単なるデータ構造になる。
data Var : Set where
X : Var
Y : Var
Z : Var
expression はこんな感じ。() は Agda ががんばってくれる。
data Expr : Set where
var : Var → Expr
a : Expr
b : Expr
c : Expr
f : Expr → Expr
g : Expr → Expr
h : Expr → Expr
_,_ : Expr → Expr → Expr
述語は statement で定義してしまう。
data Statement : Set where
p : Expr → Statement
q : Statement
r : Statement
_∧_ : Statement → Statement → Statement
_∨_ : Statement → Statement → Statement
¬ : Statement → Statement
all_=>_ : Var → Statement → Statement
exist_=>_ : Var → Statement → Statement
普通の Agda で構文の拡張は簡単にできる。
_⇒_ : Statement → Statement → Statement
x ⇒ y = ( ¬ x ) ∨ y
例えば
test2 : Statement
test2 = ¬ ( q ∧ ( all X => p ( f ( var X ))))
論理式の意味
論理式なので、それは真か偽かどちからなはずである。論理式 P に対して真偽を割り当てる関数
M : Statement → Boolを定義したい。
定数の意味は、それ自身とする。expression も、その構文自身とする。こうすると、expression に対する意味関数をさぼることができる。
M q M (p a) M (p a ∨ q) M (all x => p x)
などが有効なものになる。M を interpretation という。
M q M (p a)
これらは勝手に決める。つまり、M は勝手に決めた分だけ種類がある。M は Bool だから、
M (x ∧ y) = M0 x Data.Bool.∧ M0 y
M (x ∨ y) = M0 x Data.Bool.∨ M0 y
M (¬ x) = not (M0 x)
とするべきだろう。ここでMの中の ∧ と Data.Bool.∧ が別なものであることを理解しよう。右側が意味になる。
最後に量化記号の意味を定義する y の中に現れる変数 x を定数 c に置き換える操作を y [ x / c ] とする。
M (all x => y) = 任意の定数Cに対して、M (y [ x / c ]) = true
M (∃ x => y) = あるの定数Cに対して、M (y [ x / c ]) = true
だが、今は、限られた定数しかないので、
M (all x => y) = M0 ( y [ x / a ] ) Data.Bool.∧ M0 ( y [ x / b ] ) Data.Bool.∧ M0 ( y [ x / c ] )
M (∃ x => y) = M0 ( y [ x / a ] ) Data.Bool.∨ M0 ( y [ x / b ] ) Data.Bool.∨ M0 ( y [ x / c ] )
残りは false とする。
置換の実装
置換は構文的なものなので定数が決まっていれば簡単に実装できる。
subst-expr : Expr → Var → (value : Expr ) → Expr
subst-expr (var X ) X v = v
subst-expr (var Y ) Y v = v
subst-expr (var Z ) Z v = v
subst-expr (f x ) n v = f (subst-expr x n v)
subst-expr (x , y ) n v = (subst-expr x n v) , (subst-expr y n v)
subst-expr x n v = x
_[_/_] : (orig : Statement ) → Var → (value : Expr ) → Statement
(p x ) [ n / v ] = p ( subst-expr x n v )
q [ n / v ] = q
r [ n / v ] = r
(x ∧ y) [ n / v ] = (x [ n / v ] ) ∧ (x [ n / v ])
(x ∨ y) [ n / v ] = (x [ n / v ] ) ∨ (x [ n / v ])
(¬ x) [ n / v ] = ¬ (x [ n / v ] )
(all x => y) [ n / v ] = all x => (y [ n / v ])
(∃ x => y) [ n / v ] = ∃ x => (y [ n / v ])
subst-expr は _[_/_] と同じ記号を使いたいが、Agda では許してもらえない。
interpretation の例
{-# TERMINATING #-}
M0 : Statement → Bool
M0 q = true
M0 r = false
M0 (p a ) = true
M0 (x ∧ y) = M0 x Data.Bool.∧ M0 y
M0 (x ∨ y) = M0 x Data.Bool.∨ M0 y
M0 (¬ x) = not (M0 x)
-- we only try simple constant, it may contains arbitrary complex functional value
M0 (all x => y) = M0 ( y [ x / a ] ) Data.Bool.∧ M0 ( y [ x / b ] ) Data.Bool.∧ M0 ( y [ x / c ] )
M0 (∃ x => y) = M0 ( y [ x / a ] ) Data.Bool.∨ M0 ( y [ x / b ] ) Data.Bool.∨ M0 ( y [ x / c ] )
M0 _ = false
{-# TERMINATING #-} は Agda が停止性を確認できないために必要になる。これを取るためには、式の大きさを定義してやると良いが...
トートロジー
P <=> Q を (x ⇒ y) ∧ (y ⇒ x )で定義する。 これは M(P) ≡ M(Q) と同じである。
P <=> P
は true である。任意の interpretaion に対して、P がTの時に、|= P とする。
|= P <=> P
である。これを Agda で定義するには、interpretation の可変部分を分離する必要がある。
De Morgan の法則
述語の論理記号の定義から、
M ( ¬ ( P ∨ Q ) ) ≡ M ( ¬ P ∧ ¬ Q )
M ( ¬ ( P ∧ Q ) ) ≡ M ( ¬ P ∨ ¬ Q )
PとQは、TまたはFなので、論理式の意味からわかる。つまり、
|= ¬ ( P ∨ Q ) = ¬ P ∧ ¬ Q
|= ¬ ( P ∧ Q ) = ¬ P ∨ ¬ Q
さて、量化記号は今の場合は、
M ( ∀ X => ¬ p(X) ) = M(¬ p(a) ∧ ¬ p(b) ∧ ¬ p(c) )
= M(¬ ( p(a) ∨ p(b) ∨ p(c) ))
= M( ¬ ( ∃ X . p(X) ))
これを定数がいくらたくさんあってもなりたつとしよう。
|= ∀ X => ¬ p(X) = ¬ ( ∃ X => p(X) )
|= ∃ X => ¬ p(X) = ¬ ( ∀ X => p(X) )
ここで= の左辺と右辺のXは、お互いに影響を与えない。
あるいは、 ∃ X => p(X) を ¬ ( ∀ X => ¬ p(X) ) で定義しても良い。
論理式の例
Clausal Normal Form
論理式は複雑な入れ子を持つことができるので、かなり複雑怪奇なものを書ける。これをDe Morganを使って決まった形に落とそう。ここでの目標は、任意の一階述語論理式を、
( P ∧ Q ∧ R ) → ( Q ∨ R )
のような形(節形式 Clausal form) にすることである。P,Q,R は変数や関数を引数に持つ述語である。否定も量化記号もないので、かなり簡単になっている気がする。
シーケント代数と呼ばれる形式だと、左右を逆に、
Q , R :- P , Q , R
の様に書く。:- は←に相当する。
まず、
P → Q は ¬ P ∨ Q で置き換える
( P ∧ Q) ∨ R は ( P ∨ R ) ∧ ( Q ∨ R ) で置き換えて、
否定の付いている括弧や量化記号があったら、その否定をどんどん中に入れてしまうことができる。量化記号の変数名が重なったら、別な名前に換えておこう。
¬ ( P ∨ Q ) = ¬ P ∧ ¬ Q
¬ ( ∃ X . p(X) ) = ∀ X . ¬ p(X)
¬ ( ∀ X . p(X) ) = ∃ X . ¬ p(X)
ここで、
∃ X . p(X,Y)
とかがあったら、X は Y に依存して決まるなんらかの値である。この値をそういう関数f_Xがあると考える。
∃ X . p(X,Y) = p(f_X(Y),Y)
これをスコーレム関数という。引数は量化記号の範囲で決まる。スコーレム関数を使って∃をすべて取り除くことができる。
∀ X の方は、全部、外側に持っていってしまって構わない。ただし変数の名前は別にする必要がある。
∀ X . p(X) ∧ ∀ X . q(X)
を単に変数だけにして、
p(X) ∧ q(Y)
とする。
これを続けると、括弧の入れ子をすべて取ることができる。
この段階で、論理式は¬が付いたり付かなかったりする述語が∨とで繋がったものが、∧ で繋がったものになる。
( P11 ∨ P12 ∨ .. P1n ) ∧ ( P11 ∨ P12 ∨ .. P1n ) ... ∧ ( Pm1 ∨ Pn2 ∨ .. Pmn )P11 は¬付いたり付かなかったりする述語である。ここで、( P11 ∨ P12 ∨ .. P1n ) 一つだけに着目しよう。
¬が付いているものを左に移動する。
¬P1 ∨ ¬P2 ∨ ¬P3 ∨ ¬P4 ... ∨ Q1 ∨ Q2 ∨ Q3 ∨ Q4 ...
という形になる。
¬ (P1 ∧ P2 ∧ P3 ∧ P4 ... ) ∨ Q1 ∨ Q2 ∨ Q3 ∨ Q4 ...
これは、
(P1 ∧ P2 ∧ P3 ∧ P4 ... ) → ( Q1 ∨ Q2 ∨ Q3 ∨ Q4 ... )
となる。これで、元の論理式を節形式の集合で表すことができた。
シーケント代数の構文では、
Q1 , Q2 , Q3 , Q4 ... :- P1 , P2 , P3 , P4 ...
と書く。
節形式への変換の例
例えば「共通の父親がいるならば兄弟である」を一階述語論理で表現してみよう。
∀ X . ( ∀ Y . ( ( ∃ Z . ( father(X,Z) ∧ father(Y,Z) ) → brother(X,Y) ) ))
ここで、father(X,Z) は Z が X の父親であることを表す述語であるとする。例えば、
father(luke, anakin)
father(leia, anakin)
を仮定すると、brother(luke,leia) となる。
まず、→を展開する。
∀ X . ( ∀ Y . ( ∀ Z . ¬ (father(X,Z) ∧ father(Y,Z) )) ∨ brother(X,Y) ) )
¬ father(X,Z) ∨ ¬ father(Y,Z) ∨ brother(X,Y)
father(X,Z) ∧ father(Y,Z) → brother(X,Y)
これで節形式に変換できた。シーケント代数では、
brother(X,Y) :- father(X,Z) , father(Y,Z)
節形式での推論
節形式は左辺の中、あるいは右辺の中の項の順序を問わない、つまり、それらを入れ替える推論が許される。
Q1 , Q2 , Q3 , ... |- P1 , P2 , P3 ...
----------------------------------------------------------
Q2 , Q1 , Q3 , ... |- P2 , P1 , P3 ...
推論前の式を上に推論後の式を下に書く。複数の項をまとめてΣとかΓを使って表すこともある。
Q2, Q1, Σ |- Γ
----------------------------------------------------------
Q1, Q2, Σ |- Γ
既に正しい式には、項を追加することができる。
Σ |- Γ
----------------------------------------------------------
Q , Σ |- Γ
Σ |- Γ
----------------------------------------------------------
Σ |- Γ , Q
重複している項は一つにして良い。
Q, Q, Σ |- Γ
----------------------------------------------------------
Q , Σ |- Γ
Σ |- Γ, Q , Q
----------------------------------------------------------
Σ |- Γ Q
以上をStructual Ruleという。
共通する項を左辺と右辺に持つ二つの節形式があったら、その共通する項を消すことができる。(cut rule)
Σ |- Q, Γ Σ' , Q |- Γ'
----------------------------------------------------------
Σ , Σ ' |- Γ , Γ'
C |- C は無条件に正しい。空節 |- は矛盾を表す。
証明
証明したい式 Q を、
Q |-
の用に左辺に置く。これは¬ Q、つまり、Qの否定を仮定する。これから空節(矛盾)が導かれれば証明できたことになる。
証明時の仮定は、|- P の用に右辺に置く。
引数がある場合
項に変数な引数のあれば、それに具体的な値を与えることができる。この時に、左右にある変数には同じ値を代入する必要がある。
q(X) |- p(X)
------------------------------------------------------------------------------
q(a) |- p(a)
これを単一化(unification)、変数への代入を具象化(instantiation)という。
例えば、X = Y で XとYが等しいというのは、
X = X |-
と書ける。
X = X |- |- Y = a, q(Y)
------------------------------------------------------------------------------
a = a |- |- a = a , q(a)
------------------------------------------------------------------------------
|- q(a)
a = b のように値を与えると、この項は X = X で消去できない。つまり、証明できない。
単一化 (unification )
述語が変数を含む時には置き換え時に相互の変数の値を合わせる必要がある。定数が異なれば合わせることはできない。
片方が変数であれば、反対側の値、または、変数とする。
関数の引数に付いては、引数それぞれについて単一化をおこなう。
X = X |- |- f(a) = f(a)
------------------------------------------------------------------------------
f(a) = f(a) |- |- f(a) = f(a)
------------------------------------------------------------------------------
|-
片方が変数な場合、
X = X |- |- f(a) = f(Y)
------------------------------------------------------------------------------
f(a) = f(a) |- |- f(a) = f(a)
------------------------------------------------------------------------------
|-
さらに複雑な場合、
X = X |- |- f(X, a) = f(Y, Y)
------------------------------------------------------------------------------
f(a, a) = f(a, a) |- |- f(a, a) = f(a, a)
------------------------------------------------------------------------------
|-
関数が二重の場合、
X = X |- |- f(X, a) = f(g(Y), Y)
------------------------------------------------------------------------------
f(g(a,) a) = f(g(a), a) |- |- f(g(a), a) = f(g(a,) a)
------------------------------------------------------------------------------
|-
X = f(X) のようなものは、f(f(....)) を生成してしまう。これは論理的な意味を表さないと考える。(X = X で消去できない)
X = X |- |- f(X, a) = f(g(X), Y)
あるいは、
X = X |- |- f(X) = X
の様な場合に、これが起きる。単一化の最中に同じ変数が出てくると起きるので、Occur Check と呼ばれる。
推論の例
¬ brother(luke,leia) を仮定すると矛盾が出ることを示そう。
father(luke, anakin) |-
father(leia, anakin) |-
brother(X,Y) |- father(X,Z) , father(Y,Z)
これが仮定である。ここに、
|- brother(luke,leia)
を加える。
brother(X,Y) |- father(X,Z),father(Y,Z)
------------------------------------------------------------------------------
brother(luke,leia) |- father(luke,Z),father(leia,Z) |- brother(luke,leia)
------------------------------------------------------------------------------
|- father(luke,Z),father(leia,Z) father(luke, anakin) |-
------------------------------------------------------------------------------
|- father(leia,anakin) father(leai, anakin) |-
------------------------------------------------------------------------------
|-
ここで、変数 X Y,Z は単一化で、具体的な値に変えてから推論を行っている。
置き換えるべき節の組合せは多く、自明でない。特に、単一化が絡むと組合せの数が多くなる。しかし、単純に解ける場合もある。
Prolog
Prolog は head |- body という節の集合で、head に一つしか述語を許さない Horn Clause という形式を使っている。こうすると、置き換えは body に現れた head にしか起こらない。また、body に現れた述語のheadを機械的に探すことで自動的に推論が進む。
これを、bodyに現れた述語を順に実行すると考えると、プログラムの実行の様に見える。
Prolog の構文では、
father(luke, anakin) .
father(leia, anakin) .
brother(X,Y) :- father(X,Z) , father(Y,Z).
と記述する。
?- brother(luke,leia).
が証明するべき goal になる。
まず、brother に対する head を持つ節を探す。
brother(X,Y) :- father(X,Z) , father(Y,Z).
ここで brother(luke,leia) を brother(X,Y) と unification する。
brother(luke,leia) :- father(luke,Z) , father(leia,Z).
Prolog はbodyの最初の述語 father(luke,Z) に対するhead を持つ節を探す。
father(luke, anakin) :- .
これとのunificationを行う。Z は anakin となる。最後の father(leia,anakin) を探すと、空節が得られるので証明終となる。
この時に、Z = anakin は brother(luke,leia) の反例に必要な interpretation になっている。
SWI-Prolog
% swipl
Welcome to SWI-Prolog (threaded, 64 bits, version 7.4.2)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.
For online help and background, visit http://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).
?- [user].
|: father(luke, anakin) .
|: father(leia, anakin).
|: brother(X,Y) :- father(X,Z) , father(Y,Z).
|: ^Dtrue.
?- brother( luke, anakin).
false.
?- brother( luke, leia ).
true.
Prolog の限界
Prolog は Horn clause しか許さない。左辺に複数の述語がくる場合は、右辺に否定として移動してやることができる。
p , q : - r, s.
p : - not(q), r, s.
否定を証明できないと思うと、not(q) は失敗した時に成功する二階の述語になる。しかし、この述語は停まるとは限らない。停まる場合を finite failure という。
なので、任意の論理式をPrologとして扱うことは一般的にはできない。
問題 2.1
論理式、節形式、PrologAgda による First order logic の実装
First Order logic の意味と命題の値の計算Clausal form への変換