LoginSignup
2
1

More than 3 years have passed since last update.

@41semicolon(41semicolon)

F# で1階述語論理 （ジャンケンの分析）

Last updated at Posted at 2019-06-27

等号付き1階述語論理を実装し ジャンケンの解釈の下でいくつかの分析

1.項と式

  • 項Termの再帰的定義
    • 変数記号SymbolVと定数記号SymbolCは項。項に関数記号SymbolF*を作用させたものは項。
  • 式Formulaの再帰的定義
    • 項に関係記号SymbolP*を作用させたものは式。式に論理語SymbolL*を作用させたものは式。
    • 二項関係記号 = が存在する
type Term =
  | TermAV of SymbolV
  | TermAC of SymbolC
  | TermC1 of SymbolF1 * Term
  | TermC2 of SymbolF2 * Term * Term
and SymbolV = Variable of string 
and SymbolC = Constant of string 
and SymbolF1 = Function1 of string 
and SymbolF2 = Function2 of string 

type Formula =
  | FormulaA1 of SymbolP1 * Term
  | FormulaA2 of SymbolP2 * Term * Term
  | FormulaAE of Term * Term // equality
  | FormulaC1 of SymbolL1 * Formula
  | FormulaC2 of SymbolL2 * Formula * Formula
  | FormulaCX of SymbolLX * Formula
and SymbolP1 = Predicate of string 
and SymbolP2 = Relation2 of string 
and SymbolL1 = | NOT
and SymbolL2 = | AND | OR | IF
and SymbolLX = | FORALL of SymbolV | EXISTS of SymbolV

（注1）: 変数記号SymbolVは stringと同型なので どの変数記号を採用するかは 言語ごとに決めることができる。一方、理論的には 変数記号は1階言語で共通。つまりSymbolV は SymbolL1 などの論理語(具体的には $\lnot$)と同様に型に組み込むのが自然だが、実装の都合でこうなった（なお、定数記号等は言語ごとに異なりうるのでこの実装で問題ない）

（注2）: 簡単のため関数記号および関係記号にはアリティ1と2しか対応していないが拡張は容易。一方 任意のアリティを受け付けるようにする 例えば TermC of SymbolF * List<Term>などの方向性もあるが、型の安全性を意識して却下した。

（注3）: 量化子のシンボルは変数に依存すると記述したが(SymbolLX = | FORALL of SymbolV...) これは適当ではないかもしれない。量化子は単一のシンボルとして、合成式としてFormulaCX of SymbolLX * SymbolV * Formula のようにした方が論理学に近い気がする。

2. モデルと値

論理式Formulaに 二値FormulaValueを与えたい:

type FormulaValue = T | F

解釈Interpretationは おおよそ以下のように構成する:

  • 議論対象となる 存在物Thing、およびその集合(議論領域・ドメイン)を定める
  • 議論領域上での「変数」「定数/名前」「関数」「関係」に対して
    • 言語の「変数記号」「定数記号」「関数記号」「関係記号」を対応付ける
  • さらに「変数記号」にThingを対応付ける
type Interpretation = {
  variables: Map<string, SymbolV>; // just for our implement
  domain: Set<Thing>;
  xmap: Map<SymbolV, Thing>; // also called Valuation
  cmap: Map<SymbolC, Thing>;
  f1map: Map<SymbolF1, Thing -> Thing>;
  f2map: Map<SymbolF2, Thing -> Thing -> Thing>;
  p1map: Map<SymbolP1, Thing -> bool>;
  p2map: Map<SymbolP2, Thing -> Thing -> bool>;
}
and Thing = Thing of string

解釈を定めるとTermの値を帰納的にThingに対応付けることができる:

let rec termValue t ipn =
  match t with
    | TermAC c -> Map.find c ipn.cmap
    | TermAV v -> Map.find v ipn.xmap
    | TermC1 (fs, t) -> (Map.find fs ipn.f1map) (termValue t ipn)
    | TermC2 (fs, t1, t2) -> (Map.find fs ipn.f2map) (termValue t1 ipn) (termValue t2 ipn)

同様に 解釈を定めるとFormulaの値を帰納的にFormulaValueに対応付けることができる。少しややこしいのは $\forall x \phi$ の値。「$x$の全ての変異において$\phi$がT」であった時にのみTとする:

let rec formulaValue wff ipn =
  match wff with
  | FormulaA1 (ps,t) ->
      let p = Map.find ps ipn.p1map
      if (p (termValue t ipn)) then T else F
  | FormulaA2 (ps,t1,t2) ->
      let p = Map.find ps ipn.p2map
      if (p (termValue t1 ipn) (termValue t2 ipn)) then T else F
  | FormulaAE (t1, t2) ->
      if ((termValue t1 ipn) = (termValue t2 ipn)) then T else F
  | FormulaC1 (ls,f) ->
      match ls, (formulaValue f ipn) with
        | NOT, T -> F
        | NOT, F -> T
  | FormulaC2 (ls,f1,f2) ->
      match ls, (formulaValue f1 ipn), (formulaValue f2 ipn) with
        | AND, T, T -> T
        | AND, T, F
        | AND, F, T
        | AND, F, F -> F
        | OR, T, T
        | OR, T, F
        | OR, F, T -> T
        | OR, F, F -> F
        | IF, T, T -> T
        | IF, T, F -> F
        | IF, F, T
        | IF, F, F -> T
  | FormulaCX (ls,f) ->
      match ls with
        | FORALL v -> // iterate all mutations
          ipn.domain
          |> Set.forall (fun th ->
            let ipn2 = { ipn with xmap = (Map.add v th ipn.xmap) } // v-mutate
            match formulaValue f ipn2 with | T -> true | F -> false )
          |> fun b -> if b then T else F
        | EXISTS v -> // iterate possibly all mutations 
          ipn.domain
          |> Set.exists (fun th ->
            let ipn2 = { ipn with xmap = (Map.add v th ipn.xmap) } // v-mutate
            match formulaValue f ipn2 with | T -> true | F -> false )
          |> fun b -> if b then T else F

3. 実例: ジャンケン

ジャンケンを1階言語の言葉で表現してみる。言語に以下を含ませる:

  • 存在物は「グー」「チョキ」「パー」
    • Thing "G", Thing "C", Thing "P"
    • （注）: 存在物は解釈なのでホントはここに含めるべきでない
  • 定数記号はなし
  • 変数記号は x, y, z
    • Variable "x", Variable "y", Variable "z"
  • 関数記号には「・・の次」（例：「グー」の次は「チョキ」）
    • Function1 "next"
  • 関係記号には「・・は・・より強い」
    • Relation2 "x wins, y loses"

3-1. 準備

変数記号x,y,z, 単項関数記号 nxt, 2項関係記号 win を定義。テンプレートとなる解釈を作る。:

let ipn0 = { // template
  domain = set [Thing "G";Thing "C";Thing "P"];
  variables = Map ["x",Variable "x";"y",Variable "y";"z",Variable "z"];
  xmap = Map.empty;
  cmap = Map.empty;
  f1map= Map.empty;
  f2map= Map.empty;
  p1map= Map.empty;
  p2map= Map.empty
}
let nxt = Function1 "next"
let win = Relation2 "x wins, y loses"

3-2. 解釈を固定した ジャンケンの真理

winやnxtに対して僕らが期待する実装で解釈を固定しよう。固定した解釈の下での式の値を表示する関数も定義。あとすぐ使えるように変数x,yを取ってくる:

let nxtImpl = function
  | Thing "G" -> Thing "C"
  | Thing "C" -> Thing "P"
  | Thing "P" -> Thing "G"
  | x -> failwith (sprintf "oops%A" x) 
let winImpl a b =
  match (a,b) with
    | Thing "G", Thing "C"
    | Thing "C", Thing "P"
    | Thing "P", Thing "G" -> true
    | _ -> false 
let ipn = 
  { ipn0 with
      f1map = Map [(nxt,nxtImpl)];
      p2map = Map [(win,winImpl)]; }
let show wff = 
  match formulaValue wff ipn with
    | T -> "YES"
    | F -> "NO"
  |> printfn "%s"
let x = Map.find "x" ipn.variables // すぐ使えるように取ってくる
let y = Map.find "y" ipn.variables
let z = Map.find "z" ipn.variables

いくつかの論理式の値が僕らの直観と一致することをみよう:

自身の次は 自身でない

例えば Gの次はCなのでGではないよね、という言明: 正しい

// ∀x.next(x)≠x: 全てのxについてxの次は 自身でない
FormulaCX (FORALL x, FormulaC1 (NOT, FormulaAE (TermC1 (nxt, TermAV x), TermAV x)))
|> show // -> YES

自身の次の次の次は 自身である

例えば C の次の次の次は C なので一致する。という正しい言明:

// ∀x.next(next(next(x)))=x: 全てのxについてxの次の次の次は 自身である
FormulaCX (FORALL x, FormulaAE (TermC1 (nxt, TermC1 (nxt, TermC1 (nxt, TermAV x))), TermAV x))
|> show // YES

どの手を出しても勝てる手がある

GならPに勝てるし、CならPに勝てるよねという言明: 正しい

// ∀x∃y.Win(x,y): 全てのxには勝つ相手がいる
FormulaCX (FORALL x, FormulaCX (EXISTS y, FormulaA2 (win, TermAV x, TermAV y)))
|> show // YES

絶対に勝てる方法がある（偽）

そんな手は存在しない。

// ∃x∀y.Win(x,y): 全てに勝つものがいる
FormulaCX (EXISTS x, FormulaCX (FORALL y, FormulaA2 (win, TermAV x, TermAV y)))
|> show  // NO

xがyに勝ったならxの次はyの次に勝つ

Gの次は Cの次に勝てる。なぜなら C は P に勝てるから: 正しい

// ∀x∀y.(Win(x,y) → Win(next(x), next(y))): 全てのx,yについて xがyに勝てばnext(x)はnext(y)に勝つ
let f1 = (FormulaA2 (win, TermAV x, TermAV y))
let f2 = (FormulaA2 (win, TermC1 (nxt, TermAV x), TermC1 (nxt, TermAV y)))
FormulaCX (FORALL x, FormulaCX (FORALL y, FormulaC2 (IF, f1, f2)))
|> show // YES

どの手を出しても勝てる相手は1つしかいない

数について扱っていないのにこのような言明を肯定できるのは興味深い。いわゆる $\exists!$ の例。

// ∀x∀y. (Win(x,y) → ∃z. y≠z ⋀ Win(x,z))
// xがyに勝つ時、y以外にxが勝つ相手がいる → これがFになる
// つまり、どの手を出しても勝てる相手は1つしかいない
let f1 = FormulaA2 (win, TermAV x, TermAV y)
let f2 = FormulaCX (EXISTS z, FormulaC2 (AND,
   FormulaC1 (NOT, FormulaAE (TermAV y, TermAV z)),
   (FormulaA2 (win, TermAV x, TermAV z))))
FormulaCX (FORALL x, FormulaCX (FORALL y, FormulaC2 (IF, f1, f2)))
|> show // NO
2
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
2
1