5

バリアント述語のこれら 2 つの実装に論理的な違いはありますか?

variant1(X,Y) :-
 subsumes_term(X,Y),
 subsumes_term(Y,X).

variant2(X_,Y_) :-
  copy_term(X_,X),
  copy_term(Y_,Y),
  numbervars(X, 0, N),
  numbervars(Y, 0, N),
  X == Y.
4

1 に答える 1

5

構文バリアントであることのテストvariant1/2も実装もしていません。variant2/2しかし、さまざまな理由で。

目標variant1(f(X,Y),f(Y,X))は成功するはずですが、失敗します。両側に同じ変数が表示される場合、variant1/2期待どおりに動作しないことがあります。これを修正するには、次を使用します。

variant1a(X, Y) :-
   copy_term(Y, YC),
   subsumes_term(X, YC),
   subsumes_term(YC, X).

目標variant2(f('$VAR'(0),_),f(_,'$VAR'(0)))は失敗するはずですが、成功します。明らかに、その引数に何も発生しvariant2/2ないと仮定します。'$VAR'/1

ISO/IEC 13211-1:1995 では、バリアントを次のように定義しています。

7.1.6.1 用語の変形

前者の変数から後者の変数への全単射が存在sし、後者の項が前者の各変数を

X
Xs

ノート

1 たとえば、f(A, B, A)は のバリアントf(X, Y, X)、
g(A, B)は のバリアントg(_, _)、P+Qは のバリアントです
P+Q。

bagof/3
2 (8.10.2) およびsetof/3(8.10.3)を定義する場合、バリアントの概念が必要です。

Xs上記は変数名ではなく ( X)であることに注意してくださいs。これsは代入の特殊なケースである全単射です。

ここで、すべての例は、変数がたまたま互いに素であるbagof/3およびでの典型的な使用法を参照していますが、より微妙なケースは、共通の変数がある場合です。setof/3

論理プログラミングでは、通常の定義はむしろ次のとおりです。

VTは、次のような σ と θ が存在する場合のバリアントです。

  • Vσ とTは同一です
  • Tθ とV同じです

つまり、両方が一致する場合、それらはバリアントです。ただし、マッチングの概念は、Prolog プログラマーにとってかなりなじみがありません。つまり、形式ロジックで使用されるマッチングの概念です。これは、多くの Prolog プログラマーをパニックに陥れるケースです。

と を検討f(X)してくださいf(g(X))。f(g(X))合うかf(X)合わないか 多くの Prolog プログラマーは肩をすくめて、発生チェックについてつぶやきます。しかし、これは発生チェックとはまったく関係ありません。彼らは一致します、はい、なぜなら

f(X){ X↦ g(X)} は と同じですf(g(X))。

この置換はすべてXを置換し、それらを に置換することに注意してくださいg(X)。これはどのように起こりますか？実際、メモリ内のグラフとしての Prolog の典型的な用語表現では起こりません。Prolog では、ノードXは何らかの形でメモリ内の実際のアドレスであり、そのような操作を行うことはまったくできません。しかし、論理では、物事は完全にテキストレベルにあります。まるで

sed 's/\<X\>/g(X)/g'

ただし、変数を同時に置換することもできます。考えてみてください{ X ↦ Y, Y ↦ X}。一度に置き換える必要があります。そうしないと、またはf(X,Y)に縮小されます。f(X,X)f(Y,Y)

したがって、この定義は形式的には完全ですが、Prolog システムでは直接対応していない概念に依存しています。

同様の問題は、マッチングではない一方的なユニフィケーションを考慮した場合にも発生しますが、ユニフィケーションとマッチングの間の一般的なケースです。

ISO/IEC 13211-1:1995 Cor.2:2012 (草案) によると:

8.2.4 subsumes_term/2

この組み込み述語は、構文の片側統一のテストを提供します。

8.2.4.1 説明

subsumes_term(General, Specific)は、次のような置換θがある場合に真です。

a) Generalθ とSpecificθは同一であり、
b) SpecificθとSpecific は同一です。

手続き的には、subsumes_term(General, Specific)それに応じて成功または失敗するだけです。副作用や統合はありません。

の定義ではvariant1/2、subsumes_term(f(X,Y),f(Y,X))すでに失敗しています。

于 2014-11-13T09:35:27.283 に答える