日々の流転

λ. 有限領域での推移閉包の公理化

昨日も書いたように、推移閉包は一般には一階述語論理では表現できないので、領域を有限に限定した場合でも領域のサイズの上限 n に依存した形、たとえば以下のような形でしか表現できないと思い込んでいた。

• ∀x,y. T_k(x,y) ⇔ R(x,y) ∨ σ₁ ∨ … ∨ σ_n-2
• where σ_n := ∃z₁,…,z_n. R(x,z₁) ∧ R(z₁,z₂) ∧ … ∧ R(z_n-1,z_n) ∧ R(z_n,y)

Automating First-Order Relational Logic なんかでも、「The transitive closure is obtained by applying an operator that computes closure using iterative doubling, as explained in [15].」と、もう少し賢いけれども、やはり領域のサイズの上限に依存した形を使うとあったし……

だけど、これは誤りで、昨日も言及した“First-Order Logic as a Lightweight Software Specification Language - The ETPTP Toolkit”(Michel Rijnders) によると、モデル発見器 Paradox の作者の Koen Claessen が、(有限領域の場合の)領域のサイズに依存しないような形式化を考えた*1そうだ。 この論文では反射推移閉包の場合で説明していて、関数記号 s と関係記号 C を新たに導入して、以下のような公理を導入する。

• (I1) ∀x. T(x, x)
• (I2) ∀x, y. R(x, y) → T(x, y)
• (I3) ∀x, y, z. T(x, y) ∧ T(y, z) → T(x, z)
• (E1) ∀x, y. T(x, y) ∧ x ≠ y → R(x, s(x, y))
• (E2) ∀x, y. T(x, y) ∧ x ≠ y → T(s(x, y), y)
• (C1) ∀x, y. ￢C(x, x, y)
• (C2) ∀x, y, z, v. C(x, y, v) ∧ C(y, z, v) → C(x, z, v)
• (E3) ∀x, y. T(x, y) ∧ x ≠ y → C(x, s(x, y), y)

説明されてみれば「なるほど」と思うのだけど、こんな方法があったのかと感動した。 Koen Claessen すげー

本当に出来ているか Alloy で確認する

本当に反射推移閉包を公理化できているか、例によってAlloyで確認してみる。

まずは上記の公理をAlloyで書いてみる。今回はちょっとAlloy風に書いてみた。

sig U {
  R : set U,
  T : set U,
  s: U -> one U,
  C: U -> U
}
fact {
  all x : U | x in x.T
  R in T
  T.T in T
  all x : U, y : x.T | x!=y => (s[x,y] in x.R and y in s[x,y].T)
  all x, y: U | not (x->x in y.C)
  all v : U | (v.C) . (v.C) in v.C
  all x : U, y : x.T | x!=y => x->s[x,y] in y.C
}

pred show() { }
run show

assert T_is_RTc_of_R {
  all x : U | x.T = x.*R
}
check T_is_RTc_of_R for 6

それで、「run show」を実行すると、

Executing "Run show"
   Solver=minisat(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   939 vars. 75 primary vars. 1308 clauses. 34ms.
   Instance found. Predicate is consistent. 19ms.

というような感じで、反射推移閉包になっている例が出てくる。 Nextを押して更に幾つか例を作ってみても、どれも反射推移閉包になっているっぽい。

それならばと、今度は「Check T_is_RTc_of_R for 6」を実行すると、

Executing "Check T_is_RTc_of_R for 6"
   Solver=minisat(jni) Bitwidth=4 MaxSeq=6 SkolemDepth=1 Symmetry=20
   7640 vars. 516 primary vars. 12305 clauses. 136ms.
   No counterexample found. Assertion may be valid. 617ms.

という感じで、6要素までの領域では確かに反射推移閉包になっているようだ。

さらに、SATソルバーとして「Minisat with Unsat Core」を選択して、「Check T_is_RTc_of_R for 6」を実行すると、今度は Core というのが出てきて、以下のようにソースがハイライトされる。 ハイライトされている部分は、ここから論理式をひとつでも取り除いたら、反例(TがRの反射推移閉包になっていない例)が発見できてしまうような論理式の集合を表している。 この場合には公理全体が含まれているので、どの公理もTがRの反射推移閉包であることを表現するのに欠かせない公理であることがわかる。