DLVルールが安全でない

Question

DLV（Disjunctive Datalog）で作業を開始していますが、コード実行時に「ルールは安全ではありません」というエラーが報告されています。ルールは次のとおりです。

foo(R, 1) :- not foo(R, _) 

私はマニュアルを読んで、「循環依存関係は許可されていません」と見ました。私はこれがエラーを報告されている理由だと思いますが、この声明がどのようにDLVに問題があるのか​​よくわかりません。最終的な目標は、述語が定義されていない場合に何らかの初期化を行うことです。

より正確には、パラメータR（および他のもの）で 'foo'が発生していない場合は、パラメータRと1で定義します。定義されると、ルールは再びトリガされません。だから、これは私の意見では本当の再帰ではありません。

この問題の解決方法に関するコメントは歓迎します。

---

私はおそらく、ルール本体にパラメータRを一致させるために別の述語が必要であることに気付きました。このような何か：

foo(R, 1) :- not foo(R, _), bar(R) 

以来、それ以外のfooのオカレンス（R、_）がないかどうかを知る方法はありません。私は自分自身を明確にしたかどうかわかりません。

とにかく、これはどちらか特定するには:(

Answer 1

エラー「ルールが安全ではありません」動作しません：。このすべての最初の環式または非環式の依存関係とは何の関係もありません同じエラーメッセージがために現れます非環状プログラム：

foo2(R, 1) :- not foo(R,_), bar(R). 

問題は、プログラムが実際に安全ではないということです（http://www.dlvsystem.com/html/DLV_User_Manual.html#SAFETY）負のルール上のセクション（アンカー＃AEN375で述べたように、私は唯一の私に2つのリンクを使用させていただいております。答え：

Variables, which occur in a negated literal, must also occur in a positive literal in the body.

_が匿名変数であることを確認します。すなわち、プログラム

foo(R,1) :- not foo(R,_), bar(R). 

は同等として書かれた（とと等価である）ことができ

foo(R,1) :- not foo(R,X), bar(R). 

匿名変数（DLVマニュアル、アンカー＃のAEN264 - セクションの最後に）だけに私たちを許可しますルール内で一度しか出現しない変数の名前を作るのを避けます（つまり、ある値があり、それはまったく気にしない変数ですが、それでも変数です）。そして、否定は否定であるため、 「真の否定」（またはしばしば呼ばれる「強い否定」）ではなく、3つの安全条件のどれもが規則によって満たされていない。

非常に大まかで高レベルの安全性の直観は、プログラムのすべての変数がある有限領域に割り当てられることを保証することです。bar（R）を追加することでRになります。ただし、匿名変数_の場合も同じでなければなりません。

デフォルト値を定義する実際の問題： として指摘されているようにlambda.xy。ここで問題となるのは、DLVのAnswer Set（または安定したモデル）のセマンティクスです。あるルールでそれを実行しようとしても解決策はありません。 安全なプログラムを入手するために、上記の問題を置き換えることができます。 、意図したとおりに答えは、であると仮定{FOO（1,2）、バー（1）バー（2）、FOO（2,1）} ：

foo(1,2). bar(1). bar(2). 
tmp(R) :- foo(R,_). 
foo(R,1) :- not tmp(R), bar(R). 

によってこれが安定なモデルを持っていませんしかし、tmp（R）： - foo（R、_）はtmp（2）を含む必要があるので、これは有効なモデルではありません。しかし、 "not tmp（2）"はもはや真ではなく、したがってモデルにfoo（2,1）を持つことは、モデルの必要最小限性に違反します。 （これは正確には起こっておらず、直感的ではありません。詳細な技術的な詳細については、回答セットプログラミングの記事で見つけることができます。したがって、問題を解決するためには、何らかの形で「サイクルを壊す」必要があります。一つの可能​​性は次のようになります。

foo(1,2). bar(1). bar(2). bar(3). 
tmp(R) :- foo(R,X), X!=1. 
foo(R,1) :- bar(R), not tmp(R). 

すなわち、明示的に我々は値が1と異なっている場合にのみ、中間原子にRを追加することを示すことによって、モデル内のfoo（2,1）を有するTMPと矛盾しません（2）ではなく、もモデルの一部です。もちろん、これはもはやfoo（R、1）がデフォルト値または入力として存在するかどうかを区別することはできませんが、必要でない場合は...

もう一つの可能​​性は、代わりにいくつかのfoo1。私。

foo1(R,X) :- foo(R,X). 
tmp(R) :- foo(R,_). 
foo1(R,1) :- bar(R), not tmp(R). 

そして、fooの代わりにfoo1を使用してください。