7

Prolog では、統合X = [1|X]は無限のリストを取得するための適切な方法ですか? SWI-Prolog には問題はありませんが、GNU Prolog は単にハングします。

ほとんどの場合、リストを次のように置き換えることができることを知っています

one(1).
one(X) :- one(X).

しかし、私の質問はX = [1|X], member(Y, X), Y = 1、「正気の」Prolog実装で式を使用できるかどうかです。

4

3 に答える 3

6

Prolog では、統合X = [1|X]は無限のリストを取得するための適切な方法ですか?

それは、無限リストを作成することが正気であると考えるかどうかによって異なります。ISO-Prolog では、統合のようなものX = [1|X]は発生チェック (STO) の対象となるため、未定義です。つまり、標準に準拠したプログラムは、そのような目標を実行してはなりません。これを回避するために、 がありunify_with_occurs_check/2ますsubsumes_term/2。また、インターフェイスが無限項を受信しないように保護するために、 がありacyclic_term/1ます。

現在のすべての実装は で終了しX = [1|X]ます。また、GNU Prolog は次のように終了します。

| ?- X = [1|X], acyclic_term(X).

no

しかし、より複雑なケースでは、合理的なツリーの統合が必要です。これを、フリーズrepeat 1 == repeat 1を引き起こすHaskell と比較してください 。ghci

通常の Prolog プログラムでの有理ツリーの使用に関しては、これは最初は非常に興味深いものですが、あまりうまく拡張できません。一例として、1980 年代の初めにはしばらくの間、文法は有理ツリーを使用して実装されると考えられていました。残念ながら、人々は DCG だけで十分満足しています。これが研究を離れない理由の 1 つは、Prolog プログラマーが存在すると想定している多くの概念が有理ツリーには存在しないためです。例として、有理ツリーの拡張を持たない辞書編集用語の順序付けを取り上げます。つまり、標準的な用語の順序を使用して比較できない有理ツリーがあります。(実際には、これは準ランダムな結果が得られることを意味します。)つまり、そのような用語を含む並べ替えられたリストを作成することはできません。これもまた、多くのビルトインがbagof/3無限項で確実に機能しなくなりました。

クエリの例では、次の定義を検討してください。

memberd(X, [X|_Xs]).
memberd(E, [X|Xs]) :-
   dif(E,X),
   memberd(E, Xs).

?- X = 1, Xs=[1|Xs], memberd(X,Xs).
X = 1,
Xs = [1|Xs] ;
false.

そのため、非終了を回避する簡単な方法がある場合があります。しかし、ほとんどの場合、何もありません。

于 2014-11-17T00:56:03.317 に答える
4

もちろん、無数の 1 を取得することはできませんが、有理項または循環項と呼ばれるものです。ただし、すべての Prolog システムが循環項をサポートしているわけではありません。合理的な用語をサポートするシステムには、CxProlog、ECLiPSe、SICStus、SWI-Prolog、YAP などがあります。ただし、有理項で実行できる計算に関しては、それらの間に違いがあることに注意してください。

次のようなクエリ:

X = [1|X], member(Y, X), Y = 1.

誘導のサポートが必要です。上記のすべてのシステムで使用できる、Logtalk での coinduction の移植可能な実装があります。Coinduction では、Prolog システムが ( などのクエリを使用してX = [1|X]) 合理的な用語を作成できること、合理的な用語を統合できること、および合理的な用語とのバインディングをあいまいでない方法で出力できることが必要です。

有理リストの要素を列挙 (またはテスト) する例については、以下を参照してください。

https://github.com/LogtalkDotOrg/logtalk3/blob/master/examples/coinduction/lists.lgt

この例の 2 つのサンプル クエリ:

?- {coinduction(loader)}.
...
% (0 warnings)
true.
?- X = [1|X], lists::comember(Y, X), Y = 1.
X = [1|X],
Y = 1 ;
false.

?- X = [1, 2, 3| X], lists::comember(Y, X).
X = [1, 2, 3|X],
Y = 1 ;
X = [1, 2, 3|X],
Y = 2 ;
X = [1, 2, 3|X],
Y = 3 ;
false.

合理的な用語と共導に興味がある場合は、Logtalk の共導の例にいくつかの個別の例と参考文献が含まれています。

于 2014-11-17T00:36:05.717 に答える