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

Table of Contents

1 概要

本稿は,プログラミング言語Scalaを用いて, 命題論理の推論体系に関するプログラムについて説明している. 命題論理の推論体系については 命題論理の推論体系 を参照のこと. Scalaと命題論理については Scalaと命題論理 を参照のこと.

1.1 注意

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

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

1.2 証明戦略

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

推論規則が \(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の証明探索プログラムは,必ず停止するので決定手続きである.

2 推論体系LKX

ここでは,命題論理の 推論体系LKX のScalaでの実装について説明する.

2.1 シーケント

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

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

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

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

2.2 証明図

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

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

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

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

2.3 証明探索

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

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

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

2.3.1 推論規則の適用

推論規則は, 左規則 (\({\rm L\F}\), \({\rm L\T}\), \({\rm L\land}\) など)の場合, 右規則 (\({\rm R\F}\), \({\rm R\T}\), \({\rm R\land}\) など)の場合, 公理規則の場合に分けて考える.

2.3.1.1 左規則の場合

まず,与えられたシーケントに対して,左規則を適用し, 上シーケントを求める関数 applyLeftRule を定義する.

1:  def applyLeftRule(sequent: Sequent): Option[(String,List[Sequent])] = {
2:    .....
3:  }

上シーケントは複数あるので List[Sequent] とし, また適用した推論規則の名称を String で返す. 適用できる規則が存在しない場合もあるので 結果のデータ型は Option[(String,List[Sequent])] とする.

まず,シーケントの前件中で命題変数以外の命題論理式を探す.

1:  def applyLeftRule(sequent: Sequent): Option[(String,List[Sequent])] = {
2:    val (a1, a2) = sequent.antecedent.span {
3:      case Bool(_) => true
4:      case _ => false
5:    }
6:    .....
7:  }

list.span(f) は list の先頭要素から連続して関数 f が真になる部分と 最初に偽になる要素以降の部分に分割する. case文の部分は匿名関数を定義している (Programming in Scala: Case Classes and Pattern Matching の Case sequences as partial functions 参照). すなわち sequent.atencedent の先頭から連続して命題変数となっているリストを a1 に代入し, 最初に命題変数以外となっている要素以降のリストを a2 に代入している.

a2 が空リストの場合は,前件のすべてが命題変数の場合であり, 公理以外に適用可能な推論規則は存在しないので None を返す.

 1:  def applyLeftRule(sequent: Sequent): Option[(String,List[Sequent])] = {
 2:    val (a1, a2) = sequent.antecedent.span {
 3:      case Bool(_) => true
 4:      case _ => false
 5:    }
 6:    if (a2.isEmpty)
 7:      None
 8:    else {
 9:      .....
10:    }
11:  }

a2 が空リストでない場合は, a1 を gamma1 (\(\G_1\)), a2 の tail 部分を gamma2 (\(\G_2\)), 後件を変数 delta (\(\D\)) に代入し, a2 の先頭要素である命題論理式のパターンに応じて処理を行う.

 1:  def applyLeftRule(sequent: Sequent): Option[(String,List[Sequent])] = {
 2:    val (a1, a2) = sequent.antecedent.span {
 3:      case Bool(_) => true
 4:      case _ => false
 5:    }
 6:    if (a2.isEmpty)
 7:      None
 8:    else {
 9:      val gamma1 = a1
10:      val gamma2 = a2.tail
11:      val delta = sequent.decendent
12:      a2.head match {
13:        case Bool(_) => .....
14:        case False => .....
15:        case True => .....
16:        case And(f1, f2) => .....
17:        case Or(f1, f2) => .....
18:        case Imp(f1, f2) => .....
19:        case Neg(f1) => .....
20:      }
21:    }
22:  }

Bool の場合はありえないが None を返す.

case Bool(_) =>
  None

False の場合は,規則名を "Lbot" とし,上シーケントは空リストを返す.

case False =>
  Some(("Lbot", Nil))

True の場合は,規則名を "Ltop" とし,上シーケントは \(\G_1, \G_2 \lra \D\) とする.

case True =>
  Some(("Ltop",
        Sequent(gamma1 ++ gamma2, delta) :: Nil))

And(\(A\), \(B\))の場合は,規則名を "Land" とし,上シーケントは \(\G_1,A,B,\G_2 \lra \D\) とする.

case And(f1, f2) =>
  Some(("Land",
        Sequent((gamma1 :+ f1 :+ f2) ++ gamma2, delta) :: Nil))

Or(\(A\), \(B\))の場合は,規則名を "Lor" とし,上シーケントは \(\G_1,A,\G_2 \lra \D\) と \(\G_1,B,\G_2 \lra \D\) とする.

case Or(f1, f2) =>
  Some(("Lor",
        Sequent((gamma1 :+ f1) ++ gamma2, delta) ::
        Sequent((gamma1 :+ f2) ++ gamma2, delta) :: Nil))

Imp(\(A\), \(B\))の場合は,規則名を "Limp" とし,上シーケントは \(\G_1,\G_2 \lra A,\D\) と \(\G_1,B,\G_2 \lra \D\) とする.

case Imp(f1, f2) =>
  Some(("Limp",
        Sequent(gamma1 ++ gamma2, f1 :: delta) ::
        Sequent((gamma1 :+ f2) ++ gamma2, delta) :: Nil))

Neg(\(A\))の場合は,規則名を "Lneg" とし,上シーケントは \(\G_1,\G_2 \lra A,\D\) とする.

case Neg(f1) =>
  Some(("Lneg",
        Sequent(gamma1 ++ gamma2, f1 :: delta) :: Nil))

ここで示した Imp(\(A\), \(B\)) と Neg(\(A\)) の上シーケントは, テキスト 推論体系LKX で示したものとは少し異なっている. しかし証明可能性は同等であるので,上のようにしても問題は生じない.

2.3.1.2 右規則の場合

同様に,与えられたシーケントに対して,左規則を適用し, 上シーケントを求める関数 applyRightRule を定義する.

 1:  def applyRightRule(sequent: Sequent): Option[(String,List[Sequent])] = {
 2:    val (d1, d2) = sequent.decendent.span {
 3:        case Bool(_) => true
 4:        case _ => false
 5:      }
 6:    if (d2.isEmpty)
 7:      None
 8:    else {
 9:      val gamma = sequent.antecedent
10:      val delta1 = d1
11:      val delta2 = d2.tail
12:      d2.head match {
13:        case Bool(_) =>
14:          None
15:        case False =>
16:          Some(("Rbot",
17:                Sequent(gamma, delta1 ++ delta2) :: Nil))
18:        case True =>
19:          Some(("Rtop", Nil))
20:        case And(f1, f2) =>
21:          Some(("Rand",
22:                Sequent(gamma, (delta1 :+ f1) ++ delta2) ::
23:                Sequent(gamma, (delta1 :+ f2) ++ delta2) :: Nil))
24:        case Or(f1, f2) =>
25:          Some(("Ror",
26:                Sequent(gamma, (delta1 :+ f1 :+ f2) ++ delta2) :: Nil))
27:        case Imp(f1, f2) =>
28:          Some(("Limp",
29:                Sequent(f1 :: gamma, (delta1 :+ f2) ++ delta2) :: Nil))
30:        case Neg(f1) =>
31:          Some(("Lneg",
32:                Sequent(f1 :: gamma, delta1 ++ delta2) :: Nil))
33:      }
34:    }
35:  }
2.3.1.3 公理規則の場合

最後に公理規則の場合を示す.

if (sequent.antecedent.exists(f => sequent.decendent.contains(f))) {
  Some(Proof(sequent, "Ax", Nil))
}

前件のリスト sequent.antecedent 中に後件のリスト sequent.decendent に含まれる命題論理式が存在すれば Some(Proof(sequent, "Ax", Nil)) を返す.

2.3.2 上シーケントの証明探索

以下は上シーケントのリスト seqs 中の各シーケントに対して, 証明図を求めるプログラム proveAll である.

 1:  def proveAll(seqs: List[Sequent]): Option[List[Proof]] = {
 2:    if (seqs.isEmpty)
 3:      Some(Nil)
 4:    else prove(seqs.head) match {
 5:      case None => None
 6:      case Some(proof) => proveAll(seqs.tail) match {
 7:        case None => None
 8:        case Some(proofs) => Some(proof :: proofs)
 9:      }
10:    }
11:  }

seqs が空リストなら,証明図のリストも空リストである. seqs が空リストでない場合は, 最初のシーケントに対する証明図を後述の prove で求め, それが None なら None を結果として返し, Some(proof) なら seqs の残りのリストに対して再帰的に証明図のリストを求めている. 再帰的に求めた証明図のリストが None なら None を結果として返し, Some(proofs) なら proofs の前に proof を加えたリストを返す.

2.3.3 プログラム全体

与えられたシーケントの証明図を求める関数 prove は以下のようになる.

 1:  def prove(sequent: Sequent): Option[Proof] = {
 2:    lazy val left = applyLeftRule(sequent)
 3:    lazy val right = applyRightRule(sequent)
 4:    if (sequent.antecedent.exists(f => sequent.decendent.contains(f))) {
 5:      Some(Proof(sequent, "Ax", Nil))
 6:    } else if (left != None || right != None) {
 7:      val (rule, seqs) = if (left != None) left.get else right.get
 8:      proveAll(seqs) match {
 9:        case None =>
10:          None
11:        case Some(proofs) =>
12:          Some(Proof(sequent, rule, proofs))
13:      }
14:    } else {
15:      None
16:    }
17:  }

2.3.4 実行例

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

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

$ scalac prop22.scala prop-seq01.scala
$ scala LKX
Some(Proof(Sequent(List(And(p,Or(q,r))),List(And(Or(p,q),Or(p,r)))),
Land,List(Proof(Sequent(List(p,Or(q,r)),List(And(Or(p,q),Or(p,r)))),
Lor,List(Proof(Sequent(List(p,q),List(And(Or(p,q),Or(p,r)))),
Rand,List(Proof(Sequent(List(p,q),List(Or(p,q))),
Ror,List(Proof(Sequent(List(p, q),List(p,q)),Ax,List()))),
Proof(Sequent(List(p,q),List(Or(p,r))),Ror,
List(Proof(Sequent(List(p, q),List(p,r)),Ax,List()))))),
Proof(Sequent(List(p,r),List(And(Or(p,q),Or(p,r)))),Rand,
List(Proof(Sequent(List(p,r),List(Or(p,q))),Ror,
List(Proof(Sequent(List(p, r),List(p,q)),Ax,List()))),
Proof(Sequent(List(p,r),List(Or(p,r))),Ror,
List(Proof(Sequent(List(p, r),List(p,r)),Ax,List()))))))))))

しかし,上の出力結果は複雑でわかりにくい.

2.3.5 プリティプリント

そこで,証明図をよりわかりやすく表示するためのプリティプリントプログラムを実装する.

まず,シーケントが \(A_1, A_2, \ldots, A_m \lra B_1, B_2, \ldots, B_n\) のように 表示されるように Sequent クラスの toString メソッドを定義する.

case class Sequent(antecedent: List[Formula], decendent: List[Formula]) {
  override def toString =
    antecedent.mkString(", ") + " --> " + decendent.mkString(", ")
}

mkString(delimiter) は List 等のクラスに用意されているメソッドで, 要素の文字列表現を delimiter で区切って並べた文字列を作成する.

次に Proof クラスにプリティプリントのメソッドを追加する (実際の記述は練習問題).

case class Proof(endsequent: Sequent, rule: String, subproofs: List[Proof]) {
  def pp(implicit indent: Int = 0) {
    ???
  }
}

実行結果は以下のようになる.

scala> import Formula._
import Formula._
scala> val seq = Sequent(List('p && ('q || 'r)),List(('p || 'q) && ('p || 'r)))
seq: Sequent = And(p,Or(q,r)) --> And(Or(p,q),Or(p,r))
scala> LKX.prove(seq).get.pp
And(p,Or(q,r)) --> And(Or(p,q),Or(p,r))  (Land)
  p, Or(q,r) --> And(Or(p,q),Or(p,r))  (Lor)
    p, q --> And(Or(p,q),Or(p,r))  (Rand)
      p, q --> Or(p,q)  (Ror)
        p, q --> p, q  (Ax)
      p, q --> Or(p,r)  (Ror)
        p, q --> p, r  (Ax)
    p, r --> And(Or(p,q),Or(p,r))  (Rand)
      p, r --> Or(p,q)  (Ror)
        p, r --> p, q  (Ax)
      p, r --> Or(p,r)  (Ror)
        p, r --> p, r  (Ax)

2.3.6 練習問題

  1. 上のプリティプリントプログラムを完成させよ.
    (解答例)

    prop-seq02.scala を参照.

3 TODO 融合原理

ここでは,命題論理の 融合原理 のScalaでの実装について説明する. 融合戦略としては一般の節についても完全な 線形融合戦略 を用いる.

3.1

 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:  }

3.2 証明

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

3.3 反駁プログラム

反復深化探索 (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:  }

3.4 実行例

プログラム全体は 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})))))

Date:

Author: 田村直之

Org version 7.8.02 with Emacs version 24

Validate XHTML 1.0