※上記の広告は60日以上更新のないWIKIに表示されています。更新することで広告が下部へ移動します。

更新日 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.

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

|新しいページ|検索|ページ一覧|RSS|@ウィキご利用ガイド | 管理者にお問合せ
|ログイン|