ソフトウェア科学特論: Scalaと命題論理

Table of Contents

1 概要

本稿は,プログラミング言語Scalaを用いて, 命題論理を取り扱うプログラムについて説明している. 命題論理については 命題論理 を参照のこと.

1.1 注意

本Webページ(およびPDF)の作成には Emacs org-mode を用いており, 数式等の表示は MathJax を用いています. IEでは正しく表示されないことがあるため, Firefox, Safari等のWebブラウザでJavaScriptを有効にしてお使いください. また org-info.js を利用しており, 「m」キーをタイプするとinfoモードでの表示になります. 利用できるショートカットは「?」で表示されます.

なお,ここに記載しているプログラムは,間違いを含んでいる可能性があります. 利用にあたっては十分チェックをしていただくようお願いします. また,わかりやすさを重視し,効率面での配慮はしていないため, 実用的な利用には問題がある可能性があります.

1.2 Scalaについて

Scalaの概要等については,以下のWebページを参照のこと.

2 命題論理式

2.1 命題論理式

テキストは 命題論理式の定義 の節を参照.

以下はScalaで命題論理式のクラスを記述した例である (prop01.scala).

 1:  abstract class Formula
 2:  object False extends Formula {
 3:    override def toString = "False"
 4:  }
 5:  object True extends Formula {
 6:    override def toString = "True"
 7:  }
 8:  case class Bool(name: String) extends Formula {
 9:    override def toString = name
10:  }
11:  case class And(f1: Formula, f2: Formula) extends Formula
12:  case class Or(f1: Formula, f2: Formula) extends Formula
13:  case class Imp(f1: Formula, f2: Formula) extends Formula
14:  case class Neg(f1: Formula) extends Formula
  • 1行目で,命題論理式のクラスFormulaをabstract classとして定義している.
  • 2行目で,偽の命題定数を表すオブジェクトFalseを定義している. 3行目は,その文字列表現を "False" と定義している.
  • 5行目で,同様に真の命題定数を表すオブジェクトTrueを定義している.
  • 8行目で,命題変数を表すクラスBoolを定義している. nameはそのインスタンス変数であり,命題変数の名前を表している. またその文字列表現をnameとして定義している.
  • 11行目で,連言を表すクラスAndを定義している. f1とf2は連言の要素であり,And(f1, f2) により命題論理式 (f1 ∧ f2) を表している.
  • 12行目以降で,同様に選言,含意,否定を表すクラス Or, Imp, Negを定義している.

2.1.1 実行例

$ scala
scala> :load prop01.scala
...
scala> val f = And(Bool("p"),Imp(Neg(Bool("q")),True))
f: And = And(p,Imp(Neg(q),True))
scala> val g = Or(f, Bool("r"))
g: Or = Or(And(p,Imp(Neg(q),True)),r)
  • まず \(p \land (\neg q \imp \T)\) を表すFormulaオブジェクトを生成し,変数 f に代入している.
    • Scalaのcase classは,new を記述せずにオブジェクトを生成できる.
  • 次に fr を表すFormulaオブジェクトを生成し,変数 g に代入している.

2.1.2 練習問題

  1. \(p \lor \neg q \lor r\) を表すオブジェクトを生成せよ.
  2. List(Bool("p"), Neg(Bool("q")), Bool("r")).reduceRight(And(_, _)) の 実行結果はどのような命題論理式を表すか (scala.collection.immutable.List の reduceRight および Scalaプログラミング入門 reduceとfold を参照).

2.2 演算子の利用

以下のような定義を Formula クラス中に記述すると, 挿入記法や前置記法が利用できる (prop02.scala).

1:  def && (that: Formula) = And(this, that)
2:  def || (that: Formula) = Or(this, that)
3:  def ==> (that: Formula) = Imp(this, that)
4:  def unary_! = Neg(this)
  • => は再定義できないため, ==> を含意記号として用いる.
  • unary_! は単項演算子 ! を定義している.

2.2.1 実行例

prop02.scala には前方参照があるため,REPL の :load では実行できない. scalac でコンパイルしてから実行する必要がある.

$ scalac prop02.scala
$ scala
scala> ! Bool("p") && (Bool("q") ==> Bool("r"))
res: And = And(Neg(p),Imp(q,r))

2.3 暗黙型変換の定義

以下のように Formula オブジェクトを定義し, Formula オブジェクト中のメソッドをimportすると, Scala の Symbol を 命題変数として利用できる (prop02.scala).

1:  object Formula {
2:    implicit def symbol2bool(p: Symbol) = Bool(p.name)
3:  }
  • implicit def は 暗黙型変換 (implicit conversion) の定義である. ここでは Symbol を Bool に変換するメソッドを定義している.
  • Scala コンパイラは, Symbol を Bool に変換することで型エラーがなくなる場合には, この変換を自動的に適用する.

2.3.1 実行例

scala> import Formula._
scala> ! 'p && ('q ==> 'r)
res: And = And(Neg(p),Imp(q,r))
  • Scala の Symbol は 'p のように名前の前にシングルクォーテーションを付けて記述する.

2.4 部分論理式

テキストは 部分論理式 の節を参照.

2.4.1 プログラム

以下は Scala での部分論理式の記述例である (prop03.scala). Formula に対し,f の部分論理式になっているかどうかを調べるメソッド isSubformula(f) を定義している.

 1:  abstract class Formula {
 2:    def && (that: Formula) = And(this, that)
 3:    def || (that: Formula) = Or(this, that)
 4:    def ==> (that: Formula) = Imp(this, that)
 5:    def unary_! = Neg(this)
 6:    def isSubformula(f: Formula): Boolean = f match {
 7:      case False | True | Bool(_) =>
 8:        this == f
 9:      case And(f1,f2) =>
10:        this == f || isSubformula(f1) || isSubformula(f2)
11:      case Or(f1,f2) =>
12:        this == f || isSubformula(f1) || isSubformula(f2)
13:      case Imp(f1,f2) =>
14:        this == f || isSubformula(f1) || isSubformula(f2)
15:      case Neg(f1) =>
16:        this == f || isSubformula(f1)
17:    }
18:  }
19:  object False extends Formula {
20:    override def toString = "False"
21:  }
22:  object True extends Formula {
23:    override def toString = "True"
24:  }
25:  case class Bool(name: String) extends Formula {
26:    override def toString = name
27:  }
28:  case class And(f1: Formula, f2: Formula) extends Formula
29:  case class Or(f1: Formula, f2: Formula) extends Formula
30:  case class Imp(f1: Formula, f2: Formula) extends Formula
31:  case class Neg(f1: Formula) extends Formula
32:  object Formula {
33:    implicit def symbol2bool(p: Symbol) = Bool(p.name)
34:  }

2.4.2 実行例

scala> val f = And(Bool("p"),Imp(Neg(Bool("q")),True))
f: And = And(p,Imp(Neg(q),True))
scala> val g = Neg(Bool("q"))
g: Neg = Neg(q)
scala> g isSubformula f
res: Boolean = true
scala> f isSubformula g
res: Boolean = false
  • 変数 f に \(p \land (\neg q \imp \T)\) が代入され, 変数 g に \(\neg q\) が代入されている.
  • gf の部分論理式であるが, fg の部分論理式ではない.

2.4.3 練習問題

  1. 命題論理式 f の部分論理式の集合を返すメソッド f.subformulas を Scalaで定義せよ. 以下の ??? の部分を完成させ Formula クラスのメソッドとして定義する方法と, 各クラスで定義する方法のどちらでも良い.
    def subformulas: Set[Formula] = this match {
      case False | True | Bool(_) =>
        Set(this)
      case And(f1,f2) =>
        ???
      case Or(f1,f2) =>
        ???
      case Imp(f1,f2) =>
        ???
      case Neg(f1) =>
        f1.subformulas | Set(this)
    }
    
    (解答例)

    prop04.scala を参照.

  2. \(((\neg p) \land ((\neg q) \imp r))\) の部分論理式をすべて求めよ.
    (解答例)

    以下を実行すれば \(p\), \((\neg p)\), \(q\), \((\neg q)\), \(r\), \(((\neg q) \imp r)\), \(((\neg p) \land ((\neg q) \imp r))\) の7つであることがわかる.

    scala> And(Neg(Bool("p")),Imp(Neg(Bool("q")),True)).subformulas
    res: Set[Formula] = Set(Neg(q), True, ..., p)
    

2.4.4 練習問題

  1. 命題論理式 f 中に出現する命題変数の集合を返すメソッド f.bools を Scalaで定義せよ. 以下の ??? の部分を完成させ Formula クラスのメソッドとして定義する方法と, 各クラスで定義する方法のどちらでも良い.
    def bools: Set[Bool] = this match {
      case False | True =>
        Set()
      case p: Bool =>
        Set(p)
      case And(f1,f2) =>
        ???
      case Or(f1,f2) =>
        ???
      case Imp(f1,f2) =>
        ???
      case Neg(f1) =>
        f1.bools
    }
    
    (解答例)

    prop05.scala を参照.

  2. \(((\neg p) \land ((\neg q) \imp r))\) の命題変数を求めよ.
    (解答例)

    以下を実行すれば \(p\), \(q\), \(r\) の3つであることがわかる.

    scala> And(Neg(Bool("p")),Imp(Neg(Bool("q")),Bool("r"))).bools
    res: Set[Bool] = Set(p, q, r)
    

3 真理値

3.1 真理値割当

テキストは 真理値割当 の節を参照.

真理値割当を Scala の scala.collection.immutable.Map で表すことにする (Scalaプログラミング入門 Map を参照).

scala> val assignment = Map(Bool("p") -> true, Bool("q") -> false)
assignment: Map[Bool,Boolean] = Map((p,true), (q,false))

assignment(x) として値を求めた場合, キーとして登録されている命題変数に対しては値が返るが, 登録されていない命題変数に対してはエラーとなる.

scala> assignment(Bool("p"))
res: Boolean = true
scala> assignment(Bool("r"))
java.util.NoSuchElementException: key not found: Bool(r)

assignment.get(x) とすれば, Option[Boolean] 型の値として Some あるいは None が返り,エラーは生じない.

scala> assignment.get(Bool("p"))
res: Option[Boolean] = Some(true)
scala> assignment.get(Bool("r"))
res: Option[Boolean] = None

Scalaでは,このように Option 型を用いることが多い.

そこで,論理式 f の真理値を求める関数 value を Formula から Option[Boolean] への関数として定義することにする. すなわち,値が None であれば,真理値が未定義であることを表す.

たとえば \(A \land B\) の場合, \(A\) と \(B\) の真理値がどちらも Some(true) であれば Some(true), どちらかが Some(false) であれば Some(false), それ以外は None とする.

1:  case class And(f1: Formula, f2: Formula) extends Formula {
2:    def value(assignment: Map[Bool,Boolean]) =
3:      (f1.value(assignment), f2.value(assignment)) match {
4:        case (Some(true), Some(true)) => Some(true)
5:        case (Some(false), _) | (_, Some(false)) => Some(false)
6:        case _ => None
7:      }
8:  }
  • 3行目で f1 と f2 の真理値のペア (Tuple2 オブジェクト)を求めて, match-case 構文でペアに対するパターンマッチを行っている.
  • ペアの要素の両方が Some(true) なら 4行目にマッチし Some(true) が返る.
  • どちらかが Some(false) なら 5行目にマッチし Some(false) が返る.
  • いずれにもマッチしなければ 6行目が選択され None が返る.

プログラム全体は prop10.scala のようになる.

3.1.1 実行例

f は命題論理式 \(p \land \neg q\) を表す Formula とし, assignment は \(v(p) = \TV\) となる真理値割当 \(v\) を表す Map とする.

scala> val f = And(Bool("p"), Neg(Bool("q")))
f: And = And(p,Neg(q))
scala> val assignment = Map(Bool("p") -> true)
assignment: Map[Bool,Boolean] = Map((p,true))

この時 \(p \land \neg q\) の真理値は未定義であるが, \(v(q) = \FV\) となるように \(v\) を拡張すると \(p \land \neg q\) の真理値は真となる.

scala> f.value(assignment)
res: Option[Boolean] = None
scala> f.value(assignment + (Bool("q") -> false))
res: Option[Boolean] = Some(true)

3.2 充足可能性と恒真性

テキストは 充足可能性の定義恒真性の定義 の節を参照.

与えられた命題論理式の充足可能性や恒真性を判定するには, すべての真理値割当を考慮する必要がある.

そこで,すべての真理値割当を Scala の scala.collection.Iterator として返す メソッド assignments を以下のように Formula クラス中に定義する.

1:  def assignments(vs: Set[Bool]): Iterator[Map[Bool,Boolean]] =
2:    if (vs.isEmpty)
3:      Iterator(Map())
4:    else
5:      assignments(vs.tail).flatMap {
6:        as => Iterator(as + (vs.head -> false), as + (vs.head -> true))
7:      }
8:  def assignments: Iterator[Map[Bool,Boolean]] =
9:    assignments(bools)
  • assignments メソッドが呼び出されると, Formula 中の命題変数の集合 bools が求められ, それを引数として assignments メソッドが実行される (9行目).
  • 変数集合 vs が空ならば,空の Map だけが返される (3行目).
  • 変数集合 vs が空でなければ, assignments(vs.tail) により, 変数を一つ取り除いた集合に対して再帰的に真理値割当の Iterator を求める. 求まった各真理値割当 as に対し, 取り除いた変数を偽に割り当てる場合 (as + (vs.head -> false)), 真に割り当てる場合 (as + (vs.head -> true)) の2種類からなる Iterator を作成し, flatMap で真理値割当の Iterator にする.

3.2.1 実行例

以下は \(p \land q\) に対するすべての真理値割当を求めている. Iterator の値はそのままでは表示されないため, foreach(println) により各値を表示している. あるいは toList でリストに変換すれば表示される.

scala> val f = And(Bool("p"), Bool("q"))
f: And = And(p,q)
scala> f.bools
res: Set[Bool] = Set(p, q)
scala> f.assignments
res: Iterator[Map[Bool,Boolean]] = non-empty iterator
scala> f.assignments.foreach(println)
Map(q -> false, p -> false)
Map(q -> false, p -> true)
Map(q -> true, p -> false)
Map(q -> true, p -> true)
scala> f.assignments.toList
res: List[Map[Bool,Boolean]] = List(Map((q,false), (p,false)), ...)

3.2.2 練習問題

  1. 命題論理式が充足可能かどうかを判定するメソッド satisfiable を Formula クラス中に定義せよ.
    (解答例)
    def satisfiable =
      assignments.exists(this.value(_) == Some(true))
    
  2. 命題論理式が恒真かどうかを判定するメソッド valid を Formula クラス中に定義せよ.
    (解答例)
    def valid =
      assignments.forall(this.value(_) == Some(true))
    
  3. 命題論理式を充足するすべての真理値割当の Iterator を返すメソッド satAssignments を Formula クラス中に定義せよ.
    (解答例)
    def satAssignments =
      assignments.filter(this.value(_) == Some(true))
    
  4. 以下の各命題論理式について恒真性,充足可能性を答えよ.
    • \((p\land q)\imp (p\lor r)\)
    • \(p\land q\)
    • \(p\land \neg p\)
    • \(\neg p\lor p\)

3.3 論理的同値

テキストは 論理的同値 の節を参照.

\(\equ\) にあたる演算子 <==> を Formula 中に定義する (prop12.scala 参照).

def <==> (that: Formula) = And(Imp(this, that), Imp(that, this))

以下の例では Formula オブジェクトの暗黙型変換を import している.

scala> import Formula._

\(p \equ p\) は恒真である.

scala> ('p <==> 'p).valid
res: Boolean = true
scala> 'p <==> 'p valid  // Scalaではドット(.)を省略できる
res: Boolean = true

論理的同値関係 \(\Equ\) にあたる equiv を Formula 中に定義する.

def equiv(that: Formula) = (this <==> that).valid

\(p \land (p \lor q)\) と \(p\) は論理的に同値である.

scala> ('p && ('p || 'q)).equiv('p)
res: Boolean = true
scala> 'p && ('p || 'q) equiv 'p  // Scalaではドットやカッコを省略できる
res: Boolean = true

3.3.1 練習問題

以下のそれぞれを確認せよ.

  1. \(p \land q \Equ \neg(\neg p \lor \neg q)\)
  2. \(p \lor q \Equ \neg(\neg p \land \neg q)\)
  3. \(p\imp (q\imp r) \Equ (p\land q)\imp r\)
  4. \((p\land q)\imp (r\lor s) \Equ \neg p\lor \neg q\lor r \lor s\)
  5. \((\neg p\lor \neg q)\land(\neg p\lor q)\land(p\lor\neg q)\land(p\lor q) \Equ \F\)

3.4 標準形

3.4.1 否定標準形

テキストは 否定標準形 の節を参照.

以下は Formula クラス中に否定標準形 (NNF)を求めるメソッド toNNF を定義した例である.

 1:  def toNNF(implicit negative: Boolean = false): Formula = this match {
 2:    case False =>
 3:      if (negative) True else this
 4:    case True =>
 5:      if (negative) False else this
 6:    case Bool(_) =>
 7:      if (negative) Neg(this) else this
 8:    case And(f1, f2) => {
 9:      val g1 = f1.toNNF(negative)
10:      val g2 = f2.toNNF(negative)
11:      if (negative) Or(g1, g2) else And(g1, g2)
12:    }
13:    case Or(f1, f2) => {
14:      val g1 = f1.toNNF(negative)
15:      val g2 = f2.toNNF(negative)
16:      if (negative) And(g1, g2) else Or(g1, g2)
17:    }
18:    case Imp(f1, f2) =>
19:      Or(Neg(f1), f2).toNNF(negative)
20:    case Neg(f1) =>
21:      f1.toNNF(! negative)
22:  }
  • 1行目で,変換する式に否定がかかっているかどうかを示すフラグ negative が省略された場合 false としいる.
  • 2行目,4行目,6行目は,それぞれ False, True, 命題変数の変換である.
  • 8行目は And(f1, f2) の形の Formula を変換する場合である. まず f1f2 のそれぞれを否定標準形 g1g2 に変換し, negative の場合 Or(g1, g2), negative でない場合 And(g1, g2) を返す.
  • Or, Imp も同様に変換する.
  • Neg(f1) の場合,negative フラグを反転して f1 を変換する.

さらに,真部分論理式として True や False が現れないようにする (prop20b.scala).

 1:  def toNNF(implicit negative: Boolean = false): Formula = this match {
 2:    case False =>
 3:      if (negative) True else this
 4:    case True =>
 5:      if (negative) False else this
 6:    case Bool(_) =>
 7:      if (negative) Neg(this) else this
 8:    case And(f1, f2) =>
 9:      if (negative)
10:        Or(Neg(f1), Neg(f2)).toNNF(false)
11:      else
12:        (f1.toNNF(negative), f2.toNNF(negative)) match {
13:          case (_, False) | (False, _) => False
14:          case (f1, True) => f1
15:          case (True, f2) => f2
16:          case (f1, f2) => And(f1, f2)
17:        }
18:    case Or(f1, f2) =>
19:      if (negative)
20:        And(Neg(f1), Neg(f2)).toNNF(false)
21:      else
22:        (f1.toNNF(negative), f2.toNNF(negative)) match {
23:          case (f1, False) => f1
24:          case (False, f2) => f2
25:          case (_, True) | (True, _) => True
26:          case (f1, f2) => Or(f1, f2)
27:        }
28:    case Imp(f1, f2) =>
29:      Or(Neg(f1), f2).toNNF(negative)
30:    case Neg(f1) =>
31:      f1.toNNF(! negative)
32:  }

各クラスに toNNF を定義したプログラムは prop20.scala の通りである.

3.4.2 選言標準形と連言標準形

3.4.2.1 Literalクラスと節の表現

まず,命題変数あるいはその否定を表すリテラルを表すクラス Literal を定義する.

case class Literal(p: Bool, negative: Boolean) {
  override def toString =
    if (negative) "-" + p else "+" + p
}

正リテラルなら +p, 負リテラルなら -p のように表示される.

連言節あるいは選言節の集合表現を Literal の集合, すなわち Set[Literal] として表現する.

3.4.2.2 Formulaでの定義

まず Formula クラスに抽象メソッドとして toDNF と toCNF を定義する (Scala では本体のないメソッド定義は抽象メソッドとなる).

abstract class Formula {
  .....
  def toDNF: Set[Set[Literal]]
  def toCNF: Set[Set[Literal]]
}
3.4.2.3 FalseとTrueの場合

False の場合,DNF は空集合,CNF は空集合の集合である.

object False extends Formula {
  .....
  def toDNF = Set()
  def toCNF = Set(Set())
}

逆に True では,DNF は空集合の集合,CNF は空集合となる.

object True extends Formula {
  .....
  def toDNF = Set(Set())
  def toCNF = Set()
}
3.4.2.4 Boolの場合

Bool の場合,DNF も CNF も命題変数をリテラルとした集合の集合である.

case class Bool(name: String) extends Formula {
  .....
  def toDNF = Set(Set(Literal(this, false)))
  def toCNF = Set(Set(Literal(this, false)))
}
3.4.2.5 Andの場合

And(f1, f2) の場合,CNF は f1f2 のそれぞれを CNF に変換し, それらの和集合を求めれば良い.

def toCNF = f1.toCNF | f2.toCNF

DNF の場合は f1f2 のそれぞれを DNF に変換し, それぞれの各連言節を分配して和集合を求める必要がある. すなわち,それぞれの DNF が \(DNF_1\) と \(DNF_2\) の時, \(\{C_1 \cup C_2 \mid C_1 \in DNF_1,\ C_2 \in DNF_2 \}\) が求める DNF である. これは Scala の for内包表記 (for-comprehension) を用いれば簡潔に記述できる (Programming in Scala: For expressions 参照).

def toDNF =
  for { c1 <- f1.toDNF; c2 <- f2.toDNF } yield c1 | c2

c1 および c2f1.toDNF および f2.toDNF のそれぞれの要素として, すべての組合せについて c1c2 の和集合を c1 | c2 で求め, それらを要素とする集合を toDNF の結果として求めている.

同様の処理は flatMap と map を用いて以下のようにも記述できるが, for内包表記のほうがわかりやすい.

def toDNF =
  f1.toDNF.flatMap(c1 => f2.toDNF.map(c2 => c1 | c2))
3.4.2.6 Orの場合

OrAnd の場合と双対的に記述すれば良い.

def toDNF = f1.toDNF | f2.toDNF
def toCNF =
  for { c1 <- f1.toCNF; c2 <- f2.toCNF } yield c1 | c2
3.4.2.7 Impの場合

Imp は,一旦 NNF に変換してから DNF あるいは CNF に変換する.

def toDNF = toNNF.toDNF
def toCNF = toNNF.toCNF
3.4.2.8 Negの場合

Neg(f1) も一旦 NNF に変換し, それが Neg(Bool(p)) の形をしていれば負リテラル一つだけからなる DNF あるいは CNF に変換し, 他の形ならば toDNF あるいは toCNF を適用すれば良い.

def toDNF = toNNF match {
  case Neg(Bool(p)) =>
    Set(Set(Literal(Bool(p), true)))
  case nnf =>
    nnf.toDNF
}
def toCNF = toNNF match {
  case Neg(Bool(p)) =>
    Set(Set(Literal(Bool(p), true)))
  case nnf =>
    nnf.toCNF
}
3.4.2.9 プログラム全体

プログラム全体は prop21.scala のようになる.

3.4.3 練習問題

  1. \(p\imp q\) の選言標準形,連言標準形を求めよ.
  2. \((p\lor q)\land \neg(p\land q)\) の選言標準形,連言標準形を求めよ.

3.4.4 標準形の簡単化

テキストは 充足同値 の節を参照.

ここまでの方法で得られる標準形には,冗長な表現が含まれることがあるため, それらを簡単化する方法を考える.

3.4.4.1 定数除去

たとえば \(\T \lor p\) の DNF を求めると以下のように空節が含まれる.

scala> True || 'p toDNF
res: Set[Set[Literal]] = Set(Set(), Set(+p))

DNF で空の連言節は \(\T\) を表しており, \(A \lor \T \Equ \T\) より空の連言節を含む DNF 全体は \(\T\) と論理的に同値である. したがって,上の DNF として Set(Set()) が返されるほうが望ましい.

そこで And 中の toCNF を以下のように変更する.

def toCNF = {
  val cnf = f1.toCNF | f2.toCNF
  if (cnf.contains(Set())) Set(Set()) else cnf
}

Or 中の toDNF も同様に変更する.

def toDNF = {
  val dnf = f1.toDNF | f2.toDNF
  if (dnf.contains(Set())) Set(Set()) else dnf
}
3.4.4.2 相補リテラル対が含まれる場合

節に相補リテラル対が含まれる場合も簡単化できる (CNFの場合,トートロジー除去に対応する).

たとえば \((p \lor q) \land \neg p\) の DNF を求めると以下のようになる.

scala> ('p || 'q) && ! 'p toDNF
res: Set[Set[Literal]] = Set(Set(+p, -p), Set(+q, -p))

最初の連言節 \(\{p, \neg p\}\) には, \(p\) と \(\neg p\) という相補リテラル対が含まれている. \(A \land \neg A \Equ \F\) また \(A \land \F \Equ \F\) であるので, 相補リテラル対の含まれている連言節は \(\F\) と論理的に同値である. さらに \(A \lor \F \Equ A\) であるので, そのような連言節は DNF から削除できる.

そこで,まず Literal クラスに相補リテラルを求めるメソッド complement を追加する.

case class Literal(p: Bool, negative: Boolean) {
  def complement = Literal(p, ! negative)
  .....
}

次に And クラスの toDNF を以下のように変更する.

def toDNF =
  for {
    c1 <- f1.toDNF; c2 <- f2.toDNF
    if c1.forall(lit => ! c2.contains(lit.complement))
  } yield c1 | c2

for内包表記中に if で条件を記述すると, その条件を満たすものだけが要素となる. 上記の場合,連言節 c1 中のどのリテラルも, その相補リテラルが連言節 c2 に含まれないことが条件である.

同様の処理は flatMap, map, filter を用いて以下のようにも記述できる.

def toDNF =
  f1.toDNF flatMap { c1 =>
    f2.toDNF filter { c2 =>
      c1.forall(lit => ! c2.contains(lit.complement))
    } map { c2 =>
      c1 | c2
    }
  }

同様に Or クラスの toCNF を以下のように変更する.

def toCNF =
  for {
    c1 <- f1.toCNF; c2 <- f2.toCNF
    if c1.forall(lit => ! c2.contains(lit.complement))
  } yield c1 | c2
3.4.4.3 プログラム全体

プログラム全体は prop22.scala のようになる.

さらには節間の包摂関係をチェックし冗長な節を省くこともできるが(包摂除去), ここでは行わない.

3.4.5 練習問題

  1. 包摂除去を行うプログラムを作成せよ.

3.4.6 Tseitin変換

テキストは Tseitin変換 の節を参照.

Tseitin変換は,与えられた命題論理式と充足同値な CNF を求める.

3.4.6.1 Clauseクラス

まず CNF の選言節を表すクラス Clause を定義する.

 1:  case class Clause(literals: Set[Literal] = Set()) {
 2:    def isEmpty =
 3:      literals.isEmpty
 4:    def tautology =
 5:      literals.exists(lit => literals.contains(lit.complement))
 6:    def contains(lit: Literal) =
 7:      literals.contains(lit)
 8:    def + (lit: Literal) =
 9:      Clause(literals + lit)
10:    override def toString =
11:      literals.mkString("{", ", ", "}")
12:  }
  • Clause は Literal の集合として定義している.
  • isEmpty は選言節が空節かどうかを調べる.
  • tautology は選言節がトートロジーかどうかを調べる.
  • contains は与えられたリテラルを含んでいるかどうかを調べる.
  • + は与えられたリテラルを追加した選言節を求める.
  • toString は選言節の文字列表現を定義している.
3.4.6.2 Tseitinオブジェクト

次にTseitin変換の関数を含むオブジェクト Tseitin を定義する.

1:  object Tseitin {
2:    def transform(formula: Formula): Set[Clause] = {
3:      .....
4:    }
5:  }
  • transform がTseitin変換を行う関数である.
3.4.6.3 Boolオブジェクト

Tseitin変換では新しい命題変数を作り出す必要がある. そこで,以下のように Bool オブジェクトを定義する (これは Bool クラスと同じファイルで定義しなければならない).

1:  object Bool {
2:    var count = 0
3:    def apply() = synchronized {
4:      count += 1
5:      new Bool("_" + count)
6:    }
7:  }
  • Bool オブジェクトは Bool クラスの随行オブジェクト (companion object)と呼ばれる. Scala では,Javaでのクラス変数 (static変数)やクラスメソッド (staticメソッド)に あたるものは随行オブジェクト中に定義する.
  • apply() メソッドは Bool() により呼び出される. すなわち Bool() と Bool.apply() は同じ動作を行う.
  • apply メソッドでは count の値をインクリメントし, 新しい命題変数を作成している. なお synchronized キーワードは, apply メソッドの呼び出しをスレッド・セーフにするためである.

Bool() を実行するたびに新しい命題変数が作成される.

scala> Bool()
res: Bool = _1
scala> Bool()
res: Bool = _2
3.4.6.4 flattenAndとflattenOr

Tseitin変換の本体を定義する前に, And や Or の入れ子を命題論理式の Set に変換する関数 flattenAnd と flattenOr を Tseitin オブジェクト中に定義する.

 1:  def flattenAnd(f: Formula): Set[Formula] = f match {
 2:    case And(f1, f2) =>
 3:      flattenAnd(f1) | flattenAnd(f2)
 4:    case _ =>
 5:      Set(f)
 6:  }
 7:  def flattenOr(f: Formula): Set[Formula] = f match {
 8:    case Or(f1, f2) =>
 9:      flattenOr(f1) | flattenOr(f2)
10:    case _ =>
11:      Set(f)
12:  }
  • flattenAnd は And(And(a,b),And(c,d)) のような論理式を 集合 {a,b,c,d} に変換する.
  • flattenOr は Or(Or(a,b),Or(c,d)) のような論理式を 集合 {a,b,c,d} に変換する.
3.4.6.5 transformNNF

Tseitin変換の対象は NNF に限定して良い. そこで実際にTseitin変換を行う transformNNF を transform関数の内部関数として定義する.

 1:  def transform(formula: Formula): Set[Clause] = {
 2:    def transformNNF(f: Formula): Set[Clause] = {
 3:      .....
 4:    }
 5:    formula.toNNF match {
 6:      case False =>
 7:        Set(Clause())
 8:      case True =>
 9:        Set()
10:      case nnf => {
11:        var cnf = transformNNF(nnf)
12:        .....
13:      }
14:    }
15:  }
  • transform(formula) が呼び出されると, 5行目でまず formula を NNF に変換する.
  • それが False の場合は空節だけからなる集合 Set(Clause()) を結果の CNF として返す.
  • True の場合は空集合 Set() を結果の CNF として返す.
  • どちらでもなければ,transformNNF で CNF を求める.
3.4.6.6 Mapの利用

Tseitin変換では直接 CNF に変換できない部分を新しい命題論理式で置換える. たとえば \(A \land (B \lor (C \land D))\) の \(C \land D\) の部分を 新しい命題変数 \(p\) で置換える処理を行う.

そこで,どの部分論理式をどの命題変数で置換えたかを Map に記録しておく. また置換え対象の部分論理式は,flattenAnd を用いて命題論理式の集合に変換しておくことにする.

したがって Map の定義を追加するとともに, 以下のように transform の実体を定義する.

 1:  def transform(formula: Formula): Set[Clause] = {
 2:    var map: Map[Set[Formula],Bool] = Map()
 3:    def transformNNF(f: Formula): Set[Clause] = {
 4:      .....
 5:    }
 6:    formula.toNNF match {
 7:      case False =>
 8:        Set(Clause())
 9:      case True =>
10:        Set()
11:      case nnf => {
12:        var cnf = transformNNF(nnf)
13:        while (! map.isEmpty) {
14:          val (fs, p) = map.head
15:          map -= fs
16:          cnf |= fs.flatMap(f => transformNNF(Or(Neg(p), f)))
17:        }
18:        cnf
19:      }
20:    }
21:  }
  • map は transform 関数中の内部変数として定義している. したがって map は,transform の呼出し時点で初期化され, transform のスコープ中からのみ利用可能である.
  • 3行目 transformNNF の定義は後述する.
  • 12行目で,与えられた命題論理式をNNFに変換し, transformNNF でTseitin変換したCNFを cnf に代入している.
  • map 中に置換えた命題論理式と命題変数が登録されているので, while ループでそれらに対してTseitin変換を行い, cnf に追加している.
3.4.6.7 transformNNF

transformNNF の定義は以下のようになる.

 1:  def transformNNF(f: Formula): Set[Clause] =
 2:    flattenAnd(f).map(g => {
 3:      val lits = flattenOr(g).map {
 4:        case p: Bool =>
 5:          Literal(p, false)
 6:        case Neg(p: Bool) =>
 7:          Literal(p, true)
 8:        case f: And => {
 9:          val conj = flattenAnd(f)
10:          if (! map.contains(conj)) {
11:            val p = Bool()
12:            map += conj -> p
13:          }
14:          Literal(map(conj), false)
15:        }
16:      }
17:      Clause(lits)
18:    })
3.4.6.8 プログラム全体と実行結果

プログラム全体を示す (prop-tseitin01.scala 参照).

 1:  case class Clause(literals: Set[Literal] = Set()) {
 2:    def isEmpty =
 3:      literals.isEmpty
 4:    def tautology =
 5:      literals.exists(lit => literals.contains(lit.complement))
 6:    def contains(lit: Literal) =
 7:      literals.contains(lit)
 8:    def + (lit: Literal) =
 9:      Clause(literals + lit)
10:    override def toString =
11:      literals.mkString("{", ", ", "}")
12:  }
13:  object Tseitin {
14:    def flattenAnd(f: Formula): Set[Formula] = f match {
15:      case And(f1, f2) =>
16:        flattenAnd(f1) | flattenAnd(f2)
17:      case _ =>
18:        Set(f)
19:    }
20:    def flattenOr(f: Formula): Set[Formula] = f match {
21:      case Or(f1, f2) =>
22:        flattenOr(f1) | flattenOr(f2)
23:      case _ =>
24:        Set(f)
25:    }
26:    def transform(formula: Formula): Set[Clause] = {
27:      var map: Map[Set[Formula],Bool] = Map()
28:      def transformNNF(f: Formula): Set[Clause] =
29:        flattenAnd(f).map(g => {
30:          val lits = flattenOr(g).map {
31:            case p: Bool =>
32:              Literal(p, false)
33:            case Neg(p: Bool) =>
34:              Literal(p, true)
35:            case f: And => {
36:              val conj = flattenAnd(f)
37:              if (! map.contains(conj)) {
38:                val p = Bool()
39:                map += conj -> p
40:              }
41:              Literal(map(conj), false)
42:            }
43:          }
44:          Clause(lits)
45:        })
46:      formula.toNNF match {
47:        case False =>
48:          Set(Clause())
49:        case True =>
50:          Set()
51:        case nnf => {
52:          var cnf = transformNNF(nnf)
53:          while (! map.isEmpty) {
54:            val (fs, p) = map.head
55:            map -= fs
56:            cnf |= fs.flatMap(f => transformNNF(Or(Neg(p), f)))
57:          }
58:          cnf
59:        }
60:      }
61:    }
62:  
63:    def main(args: Array[String]) {
64:      import Formula._
65:      val f = ('p1 && 'p2 && 'p3) || ('q1 && 'q2 && 'q3)
66:      Tseitin.transform(f).foreach(println)
67:    }
68:  }

実行には,命題論理の基本的定義をしているプログラム prop.scala も必要である.

以下に実行結果を示す.

$ scalac prop.scala prop-tseitin01.scala
$ scala
scala> import Formula._
scala> val f1 = ('p1 && 'p2 && 'p3) || ('q1 && 'q2 && 'q3)
f1: Or = Or(And(And(p1,p2),p3),And(And(q1,q2),q3))
scala> Tseitin.transform(f1).foreach(println)
{-_2, +q3}
{-_1, +p1}
{-_1, +p2}
{-_1, +p3}
{-_2, +q2}
{-_2, +q1}
{+_1, +_2}
scala> val f2 = ('p1 && 'p2 && 'p3 && 'p4) || ('q1 && 'q2 && 'q3 && 'q4)
f2: Or = Or(And(And(And(p1,p2),p3),p4),And(And(And(q1,q2),q3),q4))
scala> Tseitin.transform(f2).foreach(println)
{-_4, +q2}
{-_4, +q1}
{-_4, +q3}
{-_3, +p4}
{-_4, +q4}
{+_3, +_4}
{-_3, +p1}
{-_3, +p2}
{-_3, +p3}

Date:

Author: 田村直之

Org version 7.8.02 with Emacs version 24

Validate XHTML 1.0