3

カスタム オペレータを定義しましょう++。equals

:- op(900, yfx, equals).
:- op(800, xfy, ++).

そして事実：

check(A equals A).

check/1次のすべての状況で true を返す述語、 let it be を作成しようとしています。

check( a ++ b ++ c ++ d equals c ++ d ++ b ++ a ),
check( a ++ b ++ c ++ d equals d ++ a ++ c ++ b),
check( a ++ b ++ c ++ d equals d ++ b ++ c ++ a ),
% and all permutations... of any amount of atoms
check( a ++ ( b ++ c ) equals (c ++ a) ++ b),
% be resistant to any type of parentheses

戻る

yes

これをPrologで実装する方法は? （コードスニペットをお願いします。それは可能ですか？何か不足していますか？）

Gnu-Prolog が推奨されますが、SWI-Prolog も使用できます。

PSコードはドラフトの「疑似コード」として扱い、小さな構文の問題は気にしないでください。

PPS '++' はまだ始まったばかりです。オペレーターをもっと増やしてほしい。そういうわけで、ものをリストに入れることは良い解決策ではないのではないかと心配しています.

さらに

さらに、クエリが可能であればいいでしょう（ただし、この部分は必須ではありません。最初の部分に答えることができれば、それで十分です）

check( a ++ (b ++ X) equals (c ++ Y) ++ b) )

可能な結果の1つ（他の人を見せてくれた@matに感謝）

X=c, Y=a

私は主に質問の最初の部分の解決策を探しています-「はい/いいえ」チェック。

X、Y の 2 番目の部分は、いい追加です。その中で、X、Y は単純なアトムでなければなりません。上記の例では、X、Y のドメインが指定されていますdomain(X,[a,b,c]),domain(Y,[a,b,c])。

4

2 に答える 2

5

あなたの表現は "defaulty" と呼ばれます: この形式の式を処理するには、"default" ケースが必要です。または、atom/1 (これは単調ではありません) を明示的にチェックする必要があります。パターン マッチングを直接使用してすべてのケースを処理することはできません。結果として、あなたのケースをもう一度考えてみてください：

check( a ++ (b ++ X) equals (c ++ Y) ++ b) )

あなたはこれが答えるべきだと言いますX=c, Y=a。ただし、答えることもできますX = (c ++ d), Y = (a ++ d)。この解決策も発生する必要がありますか? そうでない場合、単調ではないため、プログラムに関する宣言的なデバッグと推論が非常に複雑になります。あなたの場合、そのような式をリストとして表現することは理にかなっていますか? たとえば、[a,b,c,d] は [c,d,b,a] と等しいですか? 次に、ライブラリの述語 permutation/2 を使用して、そのような「式」が等しいかどうかを確認できます。

もちろん、デフォルトの表現で作業することも可能であり、多くの場合、それらはユーザーにとってより便利かもしれません (目標のデフォルトの表記法を持つ Prolog ソース コード自体、または Prolog 算術式を考えてみてください)。var/1 や atom/1 などの非単調述語や、 functor/3 や (=..)/2 などの用語検査述語を使用して、すべてのケースを体系的に処理できますが、通常は適切な宣言ソリューションを妨げたり、少なくとも妨げたりします。これは、すべてのケースをテストし、生成するためにあらゆる方向で使用できます。

于 2011-08-29T15:07:12.640 に答える
0

この質問はかなり古いですが、とにかく私の解決策を投稿します。私は余暇にプロローグを学んでいますが、これは非常に難しい問題であることがわかりました。

DCG と差分リストについて多くのことを学びました。残念ながら、リストを使用しない解決策は思いつきませんでした。マットが示唆したように、括弧に対処するために用語をフラットリストに変換しpermutation/2、リストを一致させるために使用して、++演算子の可換性を説明します...

これが私が思いついたものです：

:- op(900, yfx, equ).
:- op(800, xfy, ++).

check(A equ B) :- A equ B.

equ(A,B) :- sum_pp(A,AL,Len), sum_pp(B,BL,Len), !, permutation(AL, BL).

sum_pp(Term, List, Len) :- sum_pp_(Term, List,[], 0,Len).

sum_pp_(A, [A|X],X, N0,N) :- nonvar(A), A\=(_++_), N is N0+1.
sum_pp_(A, [A|X],X, N0,N) :- var(A), N is N0+1.
sum_pp_(A1++A2, L1,L3, N0,N) :-
    sum_pp_(A1, L1,L2, N0,N1), (nonvar(N), N1>=N -> !,fail; true),
    sum_pp_(A2, L2,L3, N1,N).

述語は、sum_pp/3項を取り、それを被加数のフラットなリストに変換し、長さを返す (またはチェックする) 一方で、括弧の影響を受けない主力です。これは DCG ルール (差分リストを使用) に非常に似ていますが、長さを使用して、無限再帰につながる左再帰を破るのに役立つため、通常の述語として記述されています (それを打ち負かすのにかなりの時間がかかりました)。 .

グランド タームをチェックできます。

?- sum_pp(((a++b)++x++y)++c++d, L, N).
L = [a,b,x,y,c,d],
N = 6 ;
false.

また、ソリューションも生成します。

?- sum_pp((b++X++y)++c, L, 5).
X = (_G908++_G909),
L = [b,_G908,_G909,y,c] ;
false.

?- sum_pp((a++X++b)++Y, L, 5).
Y = (_G935++_G936),
L = [a,X,b,_G935,_G936] ;
X = (_G920++_G921),
L = [a,_G920,_G921,b,Y] ;
false.

?- sum_pp(Y, L, N).
L = [Y],
N = 1 ;
Y = (_G827++_G828),
L = [_G827,_G828],
N = 2 ;
Y = (_G827++_G836++_G837),
L = [_G827,_G836,_G837],
N = 3 .

演算子はequ/22 つの項を「統合」し、変数がある場合は解を提供することもできます。

?- a++b++c++d equ c++d++b++a.
true ;
false.

?- a++(b++c) equ (c++a)++b.
true ;
false.

?- a++(b++X) equ (c++Y)++b.
X = c,
Y = a ;
false.

?- (a++b)++X equ c++Y.
X = c,
Y = (a++b) ;
X = c,
Y = (b++a) ;
false.

eq/2 ルールでは

equ(A,B) :- sum_pp(A,AL,Len), sum_pp(B,BL,Len), !, permutation(AL, BL).

sum_pp への最初の呼び出しは長さを生成し、2 番目の呼び出しは長さを制約として受け取ります。最初の呼び出しが 2 番目のリストと一致することのない増え続けるリストを生成し続け、無限再帰につながる可能性があるため、カットが必要です。私はまだより良い解決策を見つけていません...

このような興味深い問題を投稿していただきありがとうございます。

/ピーター

編集: DCG ルールとして書かれた sum_pp_:

sum_pp(Term, List, Len) :- sum_pp_(Term, 0,Len, List, []).
sum_pp_(A, N0,N) --> { nonvar(A), A\=(_++_), N is N0+1 }, [A].
sum_pp_(A, N0,N) --> { var(A), N is N0+1 }, [A].
sum_pp_(A1++A2, N0,N) -->
    sum_pp_(A1, N0,N1), { nonvar(N), N1>=N -> !,fail; true },
    sum_pp_(A2, N1,N).

アップデート：

sum_pp(Term, List, Len) :-
    (    ground(Term)
    ->   sum_pp_chk(Term, 0,Len, List, []), !  % deterministic
    ;    length(List, Len), Len>0,
         sum_pp_gen(Term, 0,Len, List, [])
    ).

sum_pp_chk(A, N0,N) --> { A\=(_++_), N is N0+1 }, [A].
sum_pp_chk(A1++A2, N0,N) --> sum_pp_chk(A1, N0,N1), sum_pp_chk(A2, N1,N).

sum_pp_gen(A, N0,N) --> { nonvar(A), A\=(_++_), N is N0+1 }, [A].
sum_pp_gen(A, N0,N) --> { var(A), N is N0+1 }, [A].
sum_pp_gen(A1++A2, N0,N) -->
    { nonvar(N), N0+2>N -> !,fail; true }, sum_pp_gen(A1, N0,N1),
    { nonvar(N), N1+1>N -> !,fail; true }, sum_pp_gen(A2, N1,N).

sum_pp を 2 つのバリアントに分割します。1 つ目は、基本条件をチェックし、決定論的であるスリム バージョンです。2 番目のバリアントはlength/2、右の再帰が何かを生成する機会を得る前に左の再帰が逃げるのを防ぐために、ある種の反復的な深化を実行するように呼び出します。各再帰呼び出しの前に長さチェックを行うことで、これは以前よりも多くのケースで無限再帰証明になります。

特に、次のクエリが機能するようになりました。

?- sum_pp(Y, L, N).
L = [Y],
N = 1 ;
Y = (_G1515++_G1518),
L = [_G1515,_G1518],
N = 2 .

?- sum_pp(Y, [a,b,c], N).
Y = (a++b++c),
N = 3 ;
Y = ((a++b)++c),
N = 3 ;
false.
于 2013-11-30T05:15:59.553 に答える