Edited at

F# で様相論理


1. 論理式

原子命題(型:VAR)は論理式(型:Formula)になれる。また、論理式に論理語 $\lnot,\land,\lor,\to,\Box,\Diamond$を作用させたものは論理式になる。以上の帰納的定義により論理式型Formulaを実装できる:

type Formula =

| Atom of VAR
| NOT of Formula
| AND of Formula * Formula
| OR of Formula * Formula
| IF of Formula * Formula
| NEC of Formula
| POS of Formula
and VAR = Proposition of string


2. 解釈とフレーム

論理式に二値を与えるためにはまず解釈を定める必要がある。

解釈(型:Interpretation) は フレーム(型:Frame) と 付値 からなる。フレームは 可能世界(型:World)の全体 と 各世界間の到達可能関係から構成される(関係を集合としてあらわすと 到達可能性関係の型はSet<World*World>となる)。

付値は 原子命題から可能世界全体の部分集合への写像として定義される。直観的にいうと「各原子命題がどの世界で成立するか」を定める。(写像を集合としてあらわすと 付値の型はSet<VAR*Set<World>>となる)

type Interpretation = {

frame: Frame
valuation: Set<VAR*Set<World>>
}
and Frame = {
worlds: Set<World>
graphs: Set<World*World>
}
and World = World of string

(注1): 写像も関係も 関数として実装できる。つまり 到達可能性関係はWorld->World->boolな関数、付値は VAR->Set<World>な関数として。しかし後に見るように有限フレームで考える場合は、本稿のように集合として実装した方が容易。

(注2): どうせ集合で写像を表現するならば、付値の型は Set<VAR*World> で表現できるじゃないか、というツッコミはある。


3. 論理式の値

Formulaに二値FormulaValueを与えたい:

type FormulaValue = T | F

解釈を与えることで「解釈 ipn の下での ある世界 world における 論理式 wff の値」という概念を帰納的に定義できる:

let rec formulaValue wff world ipn =

match wff with
| Atom(p) ->
match ipn.valuation |> Set.exists (fun (v, ws) -> (v = p) && (Set.contains world ws)) with
| true -> T
| false -> F
| NOT(f) ->
match formulaValue f world ipn with
| T -> F
| F -> T
| AND(f1,f2) ->
match (formulaValue f1 world ipn), (formulaValue f2 world ipn) with
| T, T -> T
| _ -> F
| OR(f1,f2) ->
match (formulaValue f1 world ipn), (formulaValue f2 world ipn) with
| F, F -> F
| _ -> T
| IF(f1,f2) ->
match (formulaValue f1 world ipn), (formulaValue f2 world ipn) with
| T, F -> F
| _ -> T
| NEC(f) -> // world から到達可能な世界 w2 すべてで T か?
[ for w1, w2 in ipn.frame.graphs do
if w1 = world then
yield (formulaValue f w2 ipn) = T
]
|> List.forall id
|> function | true -> T | false -> F
| POS(f) -> // ♢f は ¬□¬f で定義される
formulaValue (NOT (NEC (NOT f))) world ipn


4. フレームでの妥当性

フレームを固定しよう。論理式が その下での 全ての解釈(フレームを固定しているので任意の付値と同義)の任意の世界 に対して値がTとなるとき、フレームで妥当という。妥当でない場合は反例を含むように型FormulaTypeInFrameを定義する:

type FormulaTypeInFrame =

| ValidFormula
| InvalidFormula of World * Interpretation // with counterexample

上記妥当性(もしくは反例)を作成する例を以下に挙げる(若干実装が汚い)

// ユーティリティ: べき集合

let rec powerset = function
| [] -> [[]]
| x::xs -> let ps = powerset xs in ps @ List.map (List.append [x]) ps

// ユーティリティ: X→Yな写像を全列挙(型: List<List<x,y>>)
let rec allmap xs ys =
match xs with
| [] -> [[]]
| x::xs2 -> allmap xs2 ys |> List.collect (fun zs -> List.map (fun y -> (x,y)::zs) ys)

// 本体
let formulaTypeInFrame frame allvar wff =
let ipns = [ for fn in allmap allvar (powerset (Set.toList frame.worlds)) ->
{ frame=frame; valuation=set (List.map (fun (v, ws) -> v, (set ws)) fn) }]
[ for ipn in ipns do for world in frame.worlds do yield (world, ipn) ]
|> List.tryFind (fun (world, ipn) -> (formulaValue wff world ipn) = F)
|> function
| Some (world, ipn) -> InvalidFormula (world, ipn)
| None -> ValidFormula

(注1): formulaTypeInFrame の引数に「登場する命題原子記号のList」である allvar が必要なのは実装をサボったため。与えられた論理式wffに登場する命題原子記号を列挙するユーティリティを実装すれば回避可能。

(注2): ループ総数について: 論理式に登場する原子命題記号を $N$個, 可能世界の総数を $W$ 個とすると、付値は $2^{WN}$ 通りある。さらに全ての世界でのチェックが入るので総計 $W\cdot 2^{WN}$ のイテレーションが必要。古典論理の描像つまり $W=1$では $2^N$ 通りになり いつもの真理表の行数に一致する。


5. 実例

幾つかの例。小野『情報科学における論理』4章 を参照。


5-1. □P→P は成り立つか?

以下のようなフレームを考える:

A -> B -> C

ただし 大文字は自分自身に到達可能な世界を表す

実装したコードで書くとこうなる:

let a = World "A"

let b = World "B"
let c = World "C"
let frame = { worlds=set [a;b;c]; graphs=set [a,a; b,b; c,c; a,b; b,c] }

このフレームにおいては、$\Box P\to P$ は成立する。なお $\Box\Box P\to \Box P$は成立しない:

let p = Proposition "p"

let P = Atom p
// □P→P はValidFormula に評価される
let wff1 = IF (NEC P, P)
formulaTypeInFrame frame [p] wff1

// □P→□□P はInvalidFormula に評価される
// 偽な例として 世界 A 、付値 P ↦ [A, B] が得られた
let wff2 = IF (NEC P, NEC (NEC P)) // □P→□□P はInValid
formulaTypeInFrame frame [p] wff2

$\Box P\to P$ は「必然的にPならば Pである」と読みたくなるので当たり前のように見えるが、フレームを少しイジって反射性を失わせると成立しなくなる:

// 反射性を世界Cで無くす

let frame2 = { worlds=set [a;b;c]; graphs=set [a,a; b,b; a,b; b,c] }
// □P→P はもはや成り立たない
// 偽な例は 世界:C 付値:p ↦ []
formulaTypeInFrame frame2 [p] wff1


5-2. □♢P→♢□P は偽になるか?

以下のような解釈を考えると $\Box\Diamond P\to \Diamond\Box P$ は(少なくとも)世界 a で成立しなくなる:

a -> b -> c


d
ただし小文字は自身に到達不能とする
Pの付値は {c}

コードで確かめてみた:

let a = World "A"

let b = World "B"
let c = World "C"
let d = World "D"
let frame = { worlds=set [a;b;c;d]; graphs=set [a,b; b,c; b,d;] }
let p = Proposition "p"
let P = Atom p
let wff = IF (NEC (POS P), POS (NEC P))
let ipn = { frame=frame; valuation=set [p,set[c]] }
formulaValue wff a ipn // F ということで確かに成り立たない

// コンピュータは 世界C, pの付値 [] を偽な例として示している
// これは自明な解なのであまりうれしくはない
formulaTypeInFrame frame [p] wff


6. フレームの性質

フレームの性質と証明体系の公理がぴったり一致する。例えば、 a.反射性b.推移性 という制限を掛けたときの論理式の妥当性と 体系S4での定理が一致する(S4 の完全性定理)。a, b に加え c.対称性 を加えると 体系S5での定理と一致する (S5の完全性定理)。

よって、フレームに対して、どの体系が対応しているのかを判定するような処理は重要だろう(例えば機械的にフレームを自動生成していったときにS4フレームだけとりだすとか)。F# のActive Patterns として実装してみた(テストは一切していない):

let (|S4Frame|S5Frame|AnotherFrame|) { worlds=worlds; graphs=graphs } =

let isR = worlds |> Set.forall (fun w -> Set.contains (w,w) graphs)
let isS = graphs |> Set.forall (fun (w1,w2) -> Set.contains (w2,w1) graphs)
let isT = [ for w1,w2 in graphs ->
[ for y1,y2 in graphs do
if y1 = w2 then yield Set.contains (w1,y2) graphs
]
|> List.forall id
]
|> List.forall id

match isR, isT, isS with
| true, true, true -> S5Frame
| true, true, false -> S4Frame
| _ -> AnotherFrame


7. 振り返り


  • 力尽きた。決定手続きがあるらしいがよくわかっていない