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

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

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

命題論理の推論体系 で述べた各推論体系では， 証明図の満たすすべき条件を定めており， どのように証明図を構成するかの方法については定めていない．

推論規則が \(A\) から \(B\) を導く時， 証明図を \(A\) から \(B\) の順で構成していく方法を 前向き推論 (forward reasoning)と呼び， \(B\) から \(A\) の逆順で構成していく方法を 後向き推論 (backward reasoning)と呼ぶ． たとえばLKの場合，証明図を上から下へ構成する場合， 前向き推論であり，下から上へ構成する場合は後向き推論となる．

また推論規則の選択が常に一意に定まる決定的な処理手順で良い体系と， 複数の選択肢から適切なものを選ぶ必要のある非決定的な処理手順が必要な体系がある． たとえばLKで後向き推論を行う場合，非決定的な処理手順が必要だが， LKXの場合は決定的な処理手順で良い(どの推論規則を選択しても良い)．

非決定的な処理手順が必要な体系については，探索を行う必要がある． 探索の方法には，以下のようなものがある．

• 幅優先探索 (breadth first search)
• 深さ優先探索 (depth first search)
• 反復深化探索 (iterative deepening search)

幅優先探索では，1ステップの推論で得られる部分証明図をすべて求め， つぎに2ステップの推論で得られる部分証明図をすべて求め，というように nステップの推論で得られる部分証明図の集合を徐々に拡大していく手順を， 証明図全体が得られるまで続けるという方法である． この方法は，推論ステップが少ない場合には効率的であるが， 推論ステップが多い場合には大量のメモリを必要とする．

深さ優先探索では，適用可能な複数の推論規則からいずれかを選択し， 推論のステップを進めていく． 証明図が得られればそれで完了であり， 証明図が得られなければ後戻り(バックトラック)し， 別の選択肢に進む． プログラムの再帰的な処理と相性が良く，少量のメモリしか必要としないが， 無限に推論規則を適用できる場合に手続きが停止しない問題点がある．

深さ優先探索のこの問題点を解消する方法として反復深化探索がある． 反復深化探索では，推論ステップの深さを制限する値を定め， その制限値を順次増やしていく． たとえば，最初は1ステップの深さ制限で深さ優先探索を行い， 証明図が得られなければ，次に2ステップの深さ制限で深さ優先探索を行う． この深さ制限の値を順次増やすことで無限に推論規則を適用することを防いでいる． 同様の推論を何度も行うことになるが， 幅優先探索と比較してもそれほど多くなるわけではないことが知られている．

これらの探索手続きが必ず停止し， 与えられた問題が証明可能かどうかを正しく判定する時， その探索手続きは 決定手続き (decision procedure)であると呼ばれる． 証明可能な場合のみ停止し，証明不能な場合には停止しないこともある場合， その探索手続きは 半決定手続き (semi-decision procedure)であると呼ばれる． 後述のLKXの証明探索プログラムは，必ず停止するので決定手続きである．

テキストは シーケント の節を参照．

シーケントは，前件 (antecedent)部分である命題論理式の列と 後件 (decendent)部分である命題論理式の列からなる．

case class Sequent(antecedent: List[Formula], decendent: List[Formula])

命題論理式の列は List で表現している． 命題論理式の順序にはよらず， また複数の命題論理式は一つだけと同じなので， List ではなく Set で表現することも命題論理の場合は可能だが， 線形論理などの他の論理体系への適用も考慮して List で表現している．

テキストは 証明図 の節を参照．

証明図のクラスは以下のように定義する．

case class Proof(endsequent: Sequent, rule: String, subproofs: List[Proof])

endsequent は終シーケント，rule は終シーケントを導くのに利用した推論規則の名称， subproofs は上シーケントのそれぞれに対する証明図の List である．

ここでは，与えられたシーケントを終シーケントとする証明図を探索する プログラムをScalaで作成する．

LKXの体系は，LKとは異なり， 適用可能などの推論規則を適用しても良いようになっている． すなわち，あるシーケントを終シーケントとする証明図を探索する場合， そのシーケントを下シーケントとするどの推論規則を適用して 上シーケントを求めても良い． これは，下シーケントが証明可能であれば，必ず上シーケントのすべてが 証明可能となるように規則を定めているからである．

なお，このことはLKについては成り立たない． したがって，LKで証明探索を行う場合は，後戻り処理 (バックトラッキング)を 実装する必要があり，LKXの証明探索よりは複雑になる．

 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:    def resolve(that: Clause, lit: Literal) =
11:      Clause((literals - lit) | (that.literals - lit.complement))
12:    override def toString =
13:      literals.mkString("{", ", ", "}")
14:  }

1:  abstract class Proof
2:  case class Input(clause: Clause) extends Proof
3:  case class Resolution(clause: Clause, side: Clause, subproof: Proof) extends Proof

反復深化探索 (iterative deepening search)

 1:  object LinearResolution {
 2:    def refute(depth: Int, center: Clause, clauses: Set[Clause], subproof: Proof): Iterator[Proof] =
 3:      if (center.isEmpty)
 4:        Iterator(subproof)
 5:      else if (depth <= 0)
 6:        Iterator()
 7:      else
 8:        for {
 9:          lit <- center.literals.iterator
10:          clause <- clauses.iterator
11:          if clause.literals.contains(lit.complement)
12:          val resolvent = center.resolve(clause, lit)
13:          if ! resolvent.tautology
14:          if ! clauses.contains(resolvent)
15:          val proof = Resolution(resolvent, clause, subproof)
16:          refutation <- refute(depth-1, resolvent, clauses + resolvent, proof)
17:        } yield refutation
18:    def refute(clauses: Set[Clause], maxDepth: Int): Iterator[Proof] =
19:      if (clauses.exists(_.isEmpty))
20:        Iterator(Input(Clause()))
21:      else
22:        for {
23:          depth <- (1 to maxDepth).iterator
24:          clause <- clauses.iterator
25:          val proof = Input(clause)
26:          refutation <- refute(depth, clause, clauses, proof)
27:        } yield refutation
28:  }

プログラム全体は prop-res01.scala に示す通りである．

これは以下のようにして実行できる．

$ scalac prop22.scala prop-res01.scala
$ scala
scala> val c1 = Clause(Set(Literal(Bool("p"), true), Literal(Bool("q"), true)))
c1: Clause = {-p, -q}
scala> val c2 = Clause(Set(Literal(Bool("p"), true), Literal(Bool("q"), false)))
c2: Clause = {-p, +q}
scala> val c3 = Clause(Set(Literal(Bool("p"), false), Literal(Bool("q"), true)))
c3: Clause = {+p, -q}
scala> val c4 = Clause(Set(Literal(Bool("p"), false), Literal(Bool("q"), false)))
c4: Clause = {+p, +q}
scala> val clauses = Set(c1, c2, c3, c4)
clauses: Set[Clause] = Set({-p, -q}, {-p, +q}, {+p, -q}, {+p, +q})
scala> LinearResolution.refute(clauses, 4).next
res: Proof = Resolution({},{-q},
             Resolution({+q},{+p, +q},
             Resolution({-p},{-p, +q},
             Resolution({-q},{+p, -q},
             Input({-p, -q})))))