F# で命題論理

# 1. 実装
##1.1 言語
**言語** とは構文規則に則った論理式の集合のこと

**命題論理の言語**は 以下の規則で再帰的に定める:

- 規則1: 原子命題記号は論理式
- 規則2: 論理式に NOT, AND, OR, IF したものは論理式
- 規則3: それ以外は論理式ではない

```fsharp
type VAR =
  | Proposition of string

type Formula =
  | Prime of VAR
  | NOT of Formula
  | AND of Formula * Formula
  | OR of Formula * Formula
  | IF of Formula * Formula
```

命題記号は文字列の内容を持てるようにした

##1.2 解釈

**解釈**とは 原子命題記号全体の部分集合。直観的に言えば 成り立っている事実をかき集めたもの:

```fsharp
type Interpretation = 
  | Interpretation of Set<VAR>
    static member Contains v (Interpretation ipn) = Set.contains v ipn
```

解釈を定めると**論理式の値**は 以下の規則で再帰的に決まる:

- 規則4: 原子命題記号の値はそれが解釈に含まれていれば`T`そうでなければ`F`
- 規則5: 論理式fがNOTされている時の値はfの値が`T`なら`F`で、`F`なら`T`
- 規則6: 論理式f1とf2がANDされている時の値は f1,f2の値が共に`T`なら`T`で、そうでないときは`F`
- 規則7: 論理式f1とf2がORされている時の値はf1,f2の値が共に`F`なら`F`で、そうでないときは`T`
- 規則8: 論理式f1とf2がIFされている時の値は「f1の値が`F`」か「f2の値が`T`」のとき`T`で、そうでないときは`F`

```fsharp
// 論理式の値
type FormulaValue =
  | T
  | F

let formulaValue (ipn:Interpretation) (wff:Formula) =
  let rec b f =
    match f with
      | Prime p -> Interpretation.Contains p ipn
      | NOT f1 -> not (b f1)
      | AND (f1, f2) -> (b f1) && (b f2)
      | OR (f1, f2) -> (b f1) || (b f2)
      | IF (f1, f2) -> (not (b f1)) || (b f2)
  if b wff then T else F
```

## 1.3 妥当性
**恒真式**とは任意の解釈で`T`の値を持つ論理式。直観的に言えば どんな場合でも成り立つ論理式。哲学的に言えば 分析的な真理。**恒偽式**とは任意の解釈で`F`の値を持つ論理式。**充足可能な式**とは`T`の値を持ちうる式:

注: ユーティリティ関数`powerset`は本稿末尾に記載

```fsharp
// 論理式の妥当性
type FormulaType =
  | Tautology
  | Contradiction
  | Satisfiable

let formulaType (allvars:VAR list) (wff:Formula) =
  let allipns = allvars |> powerset |> List.map (set >> Interpretation) 
  if List.forall (fun ipn -> (formulaValue ipn wff) = T) allipns 
  then Tautology
  else if List.forall (fun ipn -> (formulaValue ipn wff) = F) allipns 
  then Contradiction
  else Satisfiable
```

# 2. 実例
表示関数を定義:

```fsharp
// 表示関数
let rec meaning = function
  | Prime a -> a |> fun (Proposition p) -> p // unwrap
  | NOT a -> sprintf "%s ..でない" (meaning a)
  | AND (a,b) -> sprintf "「%s」かつ「%s」" (meaning a) (meaning b)
  | OR (a,b) -> sprintf "「%s」か「%s」のどちらか" (meaning a) (meaning b)
  | IF (a,b) -> sprintf "「%s」なら「%s」だ" (meaning a) (meaning b)

let analyze allvars wff =
  match formulaType allvars wff with
    | Tautology -> "<恒真>"
    | Contradiction -> "<恒偽>"
    | Satisfiable -> "<充足可能>"
  |> fun a -> sprintf "%s: %s" a (meaning wff) 
```

準備

```fsharp
let p = Proposition "東京は梅雨"
let q = Proposition "大阪は梅雨"
let allvars = [p;q]
let shows = analyze allvars >> printfn "%s"

let P = Prime p
let Q = Prime q
```

## 2.1 排中律・無矛盾律の例
$P, P\lor\lnot P, P\land\lnot P,\lnot(P\land\lnot P)$ という四つの論理式の分析結果を記載。当たり前の結果が得られた: 

```fsharp
P |> shows
OR (P, NOT P) |> shows
AND (P, NOT P) |> shows
NOT (AND (P, NOT P)) |> shows
(* 出力
<充足可能>: 東京は梅雨
<恒真>: 「東京は梅雨」か「東京は梅雨 ..でない」のどちらか
<恒偽>: 「東京は梅雨」かつ「東京は梅雨 ..でない」
<恒真>: 「東京は梅雨」かつ「東京は梅雨 ..でない」 ..でない
*)
```

## 2.2 前線形性の例
古典論理における $\to$ の奇妙な意味付けの例は $(P\to Q)\lor(Q\to P)$が恒真となること。実質含意のパラドックスともいわれる

```fsharp
OR (IF (P,Q), IF (Q,P)) |> shows

// <恒真>: 「「東京は梅雨」なら「大阪は梅雨」だ」か「「大阪は梅雨」なら「東京は梅雨」だ」のどちらか
```

## 2.3 三段論法の例
三段論法を命題論理の言語に写した $P\land(P\to Q)\to Q$ という論理式は恒真になる

```fsharp
IF ((AND (P, IF (P,Q))), Q) |> shows

// <恒真>: 「「東京は梅雨」かつ「「東京は梅雨」なら「大阪は梅雨」だ」」なら「大阪は梅雨」だ
```

# 3. 振り返り

- Set の上手いマッチの仕方がわからずに Set と List を行ったり来たりしてしまった。Setで `x::xs` みたいに要素ひとつとそれ以外のようなマッチをどう実現したらいいのだろう
- Satisfiableは `Satisfiable of string` として充足解の例を入れるという改良の余地がありそう
- discriminated union とマッチが非常に相性がよいと思った
- `formulaType`の実装が酷い
- VAR を管理する構造があるとよさそう。`VariableManager` とか。

# 4. おまけ
使ったユーティリティ関数`powerset`

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