sorting - ISO Prolog で対応する安全な用語比較述語を定義 (および命名) する方法は?

Question

標準用語順序 (ISO/IEC 13211-1 7.2 用語順序) は、変数を含むすべての用語に対して定義されます。これには良い用途があります — の実装を考えてみてsetof/3ください。これにより、8.4 用語比較のビルトインのクリーンで論理的な多くの使用法が、あらゆる場所で imps (命令型構造の短縮形) を使用した宣言型の悪夢になります。8.4 用語比較機能:

8.4 用語の比較

8.4.1 (@=<)/2、(==)/2、(\==)/2、(@<)/2、(@>)/2、(@>=)/2。
8.4.2 比較/3 .
8.4.3 並べ替え/2 .
8.4.4 キーソート/2 .

例を挙げると、次のことを考慮してください。

?- X @< a.
true.

これは成功するので、

7.2 タームオーダー

順序付けterm_precedes (3.181) は
、用語Xterm-precedes が term に先行するかどうかを定義しYます。

XとYが同一の用語である場合、 X term_precedes Y
とY term_precedes Xは両方とも false です。

Xとの型が異なる場合Y: Xterm_precedesYの
型がの型のX前にY次の順序である場合:
variable先行floating pointする 先行integer
する 先行atomするcompound。

注 — 用語の順序をテストする組み込みの述語
は、8.4 で定義されています。
...

したがって、すべての変数は より小さいですa。しかし、一度Xインスタンス化されます：

?- X @< a, X = a.
X = a.

結果は無効になります。

それが問題です。これを克服するために、制約を使用するか、コアの動作のみに固執してinstantiation_error.

7.12.2 エラー分類

エラーは次の形式に従って分類されError_termます。

a)引数またはそのコンポーネントの 1 つが変数であり、
インスタンス化された引数またはコンポーネントが必要な場合、インスタンス化エラーが発生します。
の形をしていinstantiation_errorます。

このようにして、インスタンス化エラーが発生しない限り、結果が適切に定義されていることが確実にわかります。

の場合、制約を使用するか、クリーン インスタンス化エラーを生成するかの(\==)/2いずれかが既に存在します。dif/2iso_dif/2

iso_dif(X, Y) :-
   X \== Y,
   ( X \= Y -> true
   ; throw(error(instantiation_error,iso_dif/2))
   ).

だから私の質問は何ですか: ISO Prologで対応する安全な用語比較述語を定義 (および名前付け) する方法は? 理想的には、明示的な用語トラバーサルなしで。たぶん明確にするために：上記iso_dif/2では、トラバーサルという明示的な用語を使用していません。と の両方が内部的に用語(\==)/2を(\=)/2トラバースしますが、このオーバーヘッドは(=..)/2orによる明示的なトラバーサルと比較して非常に低くなりますfunctor/3, arg/3。

Answer 1

@coredump の回答に基づいているため、これは完全にオリジナルの回答ではありません。

1 種類のクエリlt/2(明示的な用語トラバーサルを行う参照実装) が正しく答えられない場合があります。

| ?- lt(b(b), a(a,a)).

no
| ?- @<(b(b), a(a,a)).

yes

その理由は、用語の標準的な順序では、ファンクタ名を比較する前にアリティが考慮されるためです。

第二に、lt/2変数の比較に関しては、常に instatiation_error をスローするとは限りません。

| ?- lt(a(X), a(Y)).

no

---

ここに、明示的な参照実装の別の候補を書きます。

lt(X,Y):- var(X), nonvar(Y), !, throw(error(instantiation_error)).
lt(X,Y):- nonvar(X), var(Y), !, throw(error(instantiation_error)).

lt(X,Y):-
    var(X),
    var(Y),
    ( X \== Y -> throw(error(instatiation_error)) ; !, false).

lt(X,Y):-
    functor(X, XFunc, XArity),
    functor(Y, YFunc, YArity),
    (
        XArity < YArity, !
      ;
        (
            XArity == YArity, !,
            (
                XFunc @< YFunc, !
              ;
                XFunc == YFunc,
                X =.. [_|XArgs],
                Y =.. [_|YArgs],
                lt_args(XArgs, YArgs)
            )
        )
    ).

lt_args([X1|OtherX], [Y1|OtherY]):-
    (
        lt(X1, Y1), !
      ;
        X1 == Y1,
        lt_args(OtherX, OtherY)
     ).

述語lt_args(Xs, Ys)は、対応する引数のペアが存在する場合に true でありXi、前のすべてのペアに対してYiおよびlt(Xi, Yi)となります(たとえば、はtrue です)。Xj == YjXjYjlt_args([a,X,a(X),b|_], [a,X,a(X),c|_])

クエリの例:

| ?- lt(a(X,Y,c(c),_Z1), a(X,Y,b(b,b),_Z2)).

yes
| ?- lt(a(X,_Y1,c(c),_Z1), a(X,_Y2,b(b,b),_Z2)).
uncaught exception: error(instatiation_error)

Answer 2

これは、実用的なアプローチであると私が信じているもののスケッチです。ゴールlt(X, Y)とを考えてみましょうterm_variables(X, XVars), term_variables(Y, YVars)。

定義の目的は、さらなる具体化が用語の順序を変更する可能性があるかどうかを判断することです (7.2)。したがって、責任のある変数を直接見つけたいと思うかもしれません。term_variables/2用語の順序に関連するのとまったく同じ方法で用語をトラバースするため、次のことが成り立ちます。

用語の順序を変更するインスタンス化がある場合、その変更を確認するためにインスタンス化する必要がある変数は、リスト prefixes XCs、YCsof XVars、およびYVarsそれぞれのいずれかにあります。

1. XCs、YCs、XVars、およびYVarsが同一である、または

2. XCsYCs最後の要素まで同一である、または

3. XCsとは、一方のリストがさらに要素を持ち、もう一方のリストが対応する変数リストまたはYCsと同一である最後まで同一です。XVarsYVars

興味深い特殊なケースとして、 と の最初の要素がXVars異なるYVars場合、関連性をテストする変数はそれらだけです。したがって、これには共通変数がない場合も含まれますが、それよりもさらに一般的です。

Answer 3

この回答では、 iso-prolog組み込み述語(§8.4.1、「未満の用語」)safe_term_less_than/2の単調な類似物である predicate を提示します。主なプロパティは次のとおりです。 (@<)/2

• 再帰項の明示的な走査。

• 特に、prolog-coroutining機能に基づいていwhen/2ます。

  • 比較は徐々に進行する場合があります。

    • インスタンス化が不十分な場合は常に「フリーズ」
    • 最も重要な用語の具体化が変わるたびに「目覚める」

  • 比較の現在の最前線は、明示的な (LIFO) スタックとして表されます。

  • 現在の状態は、残りのゴールに直接渡されます。

---

次のコードは、sicstus-prologバージョン 4.3.2で開発およびテストされています。

safe_term_less_than(L, R) :-                    % exported predicate
   i_less_than_([L-R]).

上記の の定義はsafe_term_less_than/2、次の補助述語に基づいています。

i_less_than_([LR|LRs]) :-
   Cond = (?=(L,R) ; nonvar(L),nonvar(R)),
    when (Cond, i_lt_step_(L,R,LRs)).

i_lt_step_(L, R, LRs) :-
   ( L == R
   -> i_less_than_(LRs)
   ; term_itype(L, L_type),
      term_itype(R, R_type),
      比較(Ord、L_type、R_type)、
      ord_lt_step_(Ord, L, R, LRs)
   ）。

term_itype(V, T) :-
   (   var (V) -> throw (エラー( instance_error ,_))
   ;  float (V) -> T = t1_float(V)
   ;  整数(V) -> T = t2_integer(V)
   ;  callable (V) -> T = t3_callable(A,F), functor (V, F, A)
   ; スロー (エラー (システム エラー、_))
   ）。

ord_lt_step_(<, _, _, _)。
ord_lt_step_(=, L, R, LRs) :-
   (  化合物(L)
   -> L =.. [_|Ls],
      R =.. [_|Rs],
      フレーズ(args_args_paired(Ls,Rs), LRs0, LRs),
      i_less_than_(LRs0)
   ; i_less_than_(LRs)
   ）。

args_args_paired([], []) --> [].
args_args_paired([L|Ls], [R|Rs]) --> [LR], args_args_paired(Ls, Rs).

サンプルクエリ:

| | ?- safe_term_less_than(X, 3).
プロローグ:trig_nondif(X,3,_A,_B),
プロローグ:trig_or([_B,X],_A,_A),
prolog:when(_A,(?=(X,3);nonvar(X),nonvar(3)),user:i_lt_step_(X,3,[])) ?
はい
| | ?- safe_term_less_than(X, 3), X = 4.
番号
| | ?- safe_term_less_than(X, 3), X = 2.
X = 2 ? ;
番号
| | ?- safe_term_less_than(X, a).
プロローグ:trig_nondif(X,a,_A,_B),
プロローグ:trig_or([_B,X],_A,_A),
prolog:when(_A,(?=(X,a);nonvar(X),nonvar(a)),user:i_lt_step_(X,a,[])) ? ;
番号
| | ?- safe_term_less_than(X, a), X = a.
番号
| | ?- safe_term_less_than(X+2, Y+1), X = Y.
番号

以前の回答と比較すると、次のことがわかります。

• 残りの目標の「テキスト量」は、一種の「肥大化」しているように見えます。
• クエリ?- safe_term_less_than(X+2, Y+1), X = Y.は失敗します。当然のことです。

Answer 4

この回答は、以前に提示した回答のフォローアップsafe_term_less_than/2です。

次は何ですか？compare/3—想像を絶する安全な変種scompare/3:

scompare(Ord, L, R) :-
   i_scompare_ord([LR], Ord)。

i_scompare_ord([], =)。
i_scompare_ord([LR|Ps], X) :-
   ((?=(L , R);nonvar(L),nonvar(R)), i_one_step_scompare_ord(L,R,Ps,X)) の場合。

i_one_step_scompare_ord(L, R, LRs, Ord) :-
   ( L == R
   -> scompare_ord(LRs, Ord)
   ; term_itype(L, L_type),
      term_itype(R, R_type),
      比較(Rel、L_type、R_type)、
      ( 相対\== (=)
      -> Ord = Rel
      ;  化合物(L)
      -> L =.. [_|Ls],
         R =.. [_|Rs],
         フレーズ(args_args_paired(Ls,Rs), LRs0, LRs),
         i_scompare_ord(LRs0, Ord)
      ; i_scompare_ord(LRs , Ord)
      )
   ）。

述語term_itype/2とは、前に定義args_args_paired//2したものと同じです。

Answer 5

なんてこった！_ 私もやってみます！

lt(X,Y) :-
   X \== Y,
   (  X \= Y
   -> term_variables(X,Xvars),
      term_variables(Y,Yvars),
      list_vars_excluded(Xvars,Yvars,XonlyVars),
      list_vars_excluded(Yvars,Xvars,YonlyVars),

      _   = s(T_alpha),
      functor(T_omega,zzzzzzzz,255), % HACK!

      copy_term(t(X,Y,XonlyVars,YonlyVars),t(X1,Y1,X1onlyVars,Y1onlyVars)),
      copy_term(t(X,Y,XonlyVars,YonlyVars),t(X2,Y2,X2onlyVars,Y2onlyVars)),
      maplist(=(T_alpha),X1onlyVars), maplist(=(T_omega),Y1onlyVars),
      maplist(=(T_omega),X2onlyVars), maplist(=(T_alpha),Y2onlyVars),

      % do T_alpha and T_omega have an impact on the order?
      (  compare(Cmp,X1,Y1),      
         compare(Cmp,X2,Y2)
      -> Cmp = (<)                % no: demand that X @< Y holds
      ;  throw(error(instantiation_error,lt/2))
      )

   ;  throw(error(instantiation_error,lt/2))
   ).

いくつかの補助的なもの：

listHasMember_identicalTo([X|Xs],Y) :-
   (  X == Y
   -> true
   ;  listHasMember_identicalTo(Xs,Y)
   ).

list_vars_excluded([],_,[]).
list_vars_excluded([X|Xs],Vs,Zs) :-
   (  listHasMember_identicalTo(Vs,X)
   -> Zs = Zs0
   ;  Zs = [X|Zs0]
   ),
   list_vars_excluded(Xs,Vs,Zs0).

いくつかテストしてみましょう (GNU Prolog 1.4.4 を使用):

?- lt(a(X,Y,c(c),Z1), a(X,Y,b(b,b),Z2))。
はい
?- lt(a(X,Y,b(b,b),Z1), a(X,Y,c(c),Z2))。
番号
?- lt(a(X,Y1,c(c),Z1), a(X,Y2,b(b,b),Z2))。
キャッチされていない例外: error(instantiation_error,lt/2)
?- lt(a(X,Y1,b(b,b),Z1), a(X,Y2,c(c),Z2))。
キャッチされていない例外: error(instantiation_error,lt/2)
?- lt(b(b), a(a,a))。
はい
?- lt(a(X), a(Y))。
キャッチされていない例外: error(instantiation_error,lt/2)
?- lt(X, 3).
キャッチされていない例外: error(instantiation_error,lt/2)
?- lt(X+a, X+b)。
はい
?- lt(X+a, Y+b)。
キャッチされていない例外: error(instantiation_error,lt/2)
?- lt(a(X), b(Y))。
はい
?- lt(a(X), a(Y))。
キャッチされていない例外: error(instantiation_error,lt/2)
?- lt(a(X), a(X))。
番号

---

2015-05-06 を編集

の実装を、 2 つの新しい変数ではなく、とlt/2を使用するように変更しました。T_alphaT_omega

• lt(X,Y)(と) の 2 つのコピーとX(X1と) の 2 つのコピーを作成します。X2YY1Y2
• と の共有変数は、と、および と によってもX共有Yされます。X1Y1X2Y2
• T_alphaは、標準的な順序で ( 、 、、で)他のすべての用語の前に来ます。X1X2Y1Y2
• T_omega は、標準的な順序で他のすべての用語の後に来ます。
• Xコピーされた用語では、含まれているが含まれていない変数Y(およびその逆) はT_alpha/で統合されT_omegaます。
  • これが用語の順序に影響を与える場合は、まだ順序を決定できません。
  • そうでない場合は、完了です。

これで、@false によって与えられた反例が機能します。

?- lt(X+1,1+2).
uncaught exception: error(instantiation_error,lt/2)
?- X=2, lt(X+1,1+2).
no

Answer 6

次！これは私の以前の試みよりもうまくいくはずです:

lt(X,Y) :-
   X \== Y,
   (  X \= Y
   -> term_variables(X,Xvars),
      term_variables(Y,Yvars),

      T_alpha is -(10.0^1000),  % HACK!
      functor(T_omega,z,255),   % HACK!

      copy_term(t(X,Y,Xvars,Yvars),t(X1,Y1,X1vars,Y1vars)),
      copy_term(t(X,Y,Xvars,Yvars),t(X2,Y2,X2vars,Y2vars)),
      copy_term(t(X,Y,Xvars,Yvars),t(X3,Y3,X3vars,Y3vars)),
      copy_term(t(X,Y,Xvars,Yvars),t(X4,Y4,X4vars,Y4vars)),

      maplist(=(T_alpha),X1vars), maplist(maybe_unify(T_omega),Y1vars),
      maplist(=(T_omega),X2vars), maplist(maybe_unify(T_alpha),Y2vars),
      maplist(=(T_omega),Y3vars), maplist(maybe_unify(T_alpha),X3vars), 
      maplist(=(T_alpha),Y4vars), maplist(maybe_unify(T_omega),X4vars),

      % do T_alpha and T_omega have an impact on the order?
      (  compare(Cmp,X1,Y1),     
         compare(Cmp,X2,Y2),
         compare(Cmp,X3,Y3),
         compare(Cmp,X4,Y4),
      -> Cmp = (<)                % no: demand that X @< Y holds
      ;  throw(error(instantiation_error,lt/2))
      )

   ;  throw(error(instantiation_error,lt/2))
   ).

補助は、 と の両方でmaybe_unify/2発生する変数を扱います。XY

maybe_unify(K,X) :-
   (  var(X)
   -> X = K
   ;  true
   ).

GNU-Prolog 1.4.4 で確認:

?- lt(a(X,Y,c(c),Z1), a(X,Y,b(b,b),Z2)).
yes
?- lt(a(X,Y,b(b,b),Z1), a(X,Y,c(c),Z2)).
no
?- lt(a(X,Y1,c(c),Z1), a(X,Y2,b(b,b),Z2)).
uncaught exception: error(instantiation_error,lt/2)
?- lt(a(X,Y1,b(b,b),Z1), a(X,Y2,c(c),Z2)).
uncaught exception: error(instantiation_error,lt/2)
?- lt(b(b), a(a,a)).
yes
?- lt(a(X), a(Y)).
uncaught exception: error(instantiation_error,lt/2)
?- lt(X, 3).
uncaught exception: error(instantiation_error,lt/2)
?- lt(X+a, X+b).
yes
?- lt(X+a, Y+b).
uncaught exception: error(instantiation_error,lt/2)
?- lt(a(X), b(Y)).
yes
?- lt(a(X), a(Y)).
uncaught exception: error(instantiation_error,lt/2)
?- lt(a(X), a(X)).
no
?- lt(X+1,1+2).
uncaught exception: error(instantiation_error,lt/2)

?- lt(X+X+2,X+1+3).                                       % NEW
uncaught exception: error(instantiation_error,lt/2)