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

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

# 1.項と式
- 項`Term`の再帰的定義
  - 変数記号`SymbolV`と定数記号`SymbolC`は項。項に関数記号`SymbolF*`を作用させたものは項。
- 式`Formula`の再帰的定義
  - 項に関係記号`SymbolP*`を作用させたものは式。式に論理語`SymbolL*`を作用させたものは式。
  - 二項関係記号 `=` が存在する

```fsharp
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`を与えたい:

```fsharp
type FormulaValue = T | F
```

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

 - 議論対象となる 存在物`Thing`、およびその集合(議論領域・ドメイン)を定める
 - 議論領域上での「変数」「定数/名前」「関数」「関係」に対して
    - 言語の「変数記号」「定数記号」「関数記号」「関係記号」を対応付ける
 - さらに「変数記号」に`Thing`を対応付ける

```fsharp
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`に対応付けることができる:

```fsharp
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`とする:

```fsharp
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` を定義。テンプレートとなる解釈を作る。:

```fsharp
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を取ってくる:

```fsharp
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ではないよね、という言明: 正しい

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

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

```fsharp
// ∀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に勝てるよねという言明: 正しい

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

### 絶対に勝てる方法がある（偽）
そんな手は存在しない。

```fsharp
// ∃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 に勝てるから: 正しい

```fsharp
// ∀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!$ の例。

```fsharp
// ∀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
```