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. 振り返り

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