A.1.2 関係計算・述語論理形式 - Model Base

更新日 2011-09-03
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ]

---

本文3.5.2から察するに、"述語論理形式"とは限量子Qを含む

Q x: e | F

の形式のことを指していると思われる。

関係rの各性質(非空的、推移的、非反射的、、、)について、 A.1.1の記述と自分で考えた述語論理形式の記述が同値になるか否かの検査記述を以下のように書いてみた。

 assert ReformulateOK {
   all r: univ->univ {
     -- nonempty
     (some r) iff (some x, y: univ | x->y in r)
     -- transitive
     (r.r in r) iff (all x, y, z: univ | (x->y in r and y->z in r)=> x->z in r)
     -- irreflexive
     (no iden & r) iff (no x: univ | x->x in r)
     -- symmetric
     (~r in r) iff (all x, y: univ | x->y in r => y->x in r) 
     -- functional
     (~r.r in iden) iff (all x: univ | lone y: univ | x->y in r)
     -- injective
     (r.~r in iden) iff (all y: univ | lone x: univ | x->y in r)
     -- total
     (univ in r.univ) iff (all x: univ | some y: univ | x->y in r)
     -- onto
     (univ in univ.r) iff (all y: univ | some x: univ | x->y in r)
     }
   }
 check ReformulateOK for 4

ちなみにスコープはA.1.1と同様に4要素としてみる。 Ctrl+E で反例の検索を実行すると、

Executing "Check ReformulateOK for 4"
  Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
  13211 vars. 256 primary vars. 49440 clauses. 1610ms.
  No counterexample found. Assertion may be valid. 62921ms.

となり、反例は見つからなかった。