述語規則の本体で全称量指定子を使用したい、つまり次のようなもの
A(x,y) <- ∀B(x,a), C(y,a).
これは、C(y, a ) の各aに対して、B(x, a ) が常に (x, a ) に一致する x を持つ場合にのみ、A(x,y) が真であることを意味します。
Datalog では、ルール本体で境界付けられたすべての変数がデフォルトで存在量指定子であるため、aも存在量指定子になります。述語規則の本体で全称量指定子を表現するにはどうすればよいですか?
ありがとうございました。
PS 私が使用している Datalog エンジンは logicblox です。
基本的な考え方は、論理公理を使用することです
∀ x φ( x ) ⇔ ¬∃<em>x ¬φ( x )
ルールを存在量指定子のみが必要な形式にします (否定とともに)。直観的には、これは通常、最初に回答の補数を計算し、次にその補数を計算して最終的な回答を生成することを意味します。
たとえば、グラフG ( V , E ) が与えられ、グラフ内の他のすべての頂点に隣接する頂点を見つけたいとします。Datalog ルール本体で全称量化が許可されている場合、次のように記述できます。
Q(x) <- ∀y E(x,y).
これを全称量指定子なしで書くには、最初に他のすべての頂点に隣接していない頂点を計算します。
NQ(x) <- V(x), V(y), !E(x,y).
次に、その補数を答えとして返します
Q(x) <- V(x), !NQ(x).
同じ種類のトリックが SQL でも使用できますが、SQL にも普遍量指定子がありません。