如何在 ISO Prolog 中定义(和命名)相应的安全术语比较谓词? [英] How to define (and name) the corresponding safe term comparison predicates in ISO Prolog?

问题描述

标准术语顺序(ISO/IEC 13211-1 7.2 术语顺序)定义在所有术语上——包括变量.虽然这个有很好的用途——想想 setof/3 的实现，这使得 8.4 术语比较中内置函数的许多其他干净和合乎逻辑的使用变成了与 imps(命令式构造的缩写形式)的声明性噩梦.8.4 词条比较特征:

Standard term order (ISO/IEC 13211-1 7.2 Term order) is defined over all terms — including variables. While there are good uses for this — think of the implementation of setof/3, this makes many otherwise clean and logical uses of the built-ins in 8.4 Term comparison a declarative nightmare with imps (short form for imperative constructs) all around. 8.4 Term comparison features:

8.4.1 (@=<)/2, (==)/2, (==)/2, (@<)/2, (@>)/2,(@>=)/2.
8.4.2 compare/3.
8.4.3 sort/2.
8.4.4 keysort/2.p>

8.4 Term comparison

8.4.1 (@=<)/2, (==)/2, (==)/2, (@<)/2, (@>)/2, (@>=)/2.
8.4.2 compare/3.
8.4.3 sort/2.
8.4.4 keysort/2.

举个例子，考虑一下:

?- X @< a.
true.

这成功了，因为

排序term_precedes (3.181) 定义是否
不是一个术语 X 术语 - 在一个术语 Y 之前.

7.2 Term order

An ordering term_precedes (3.181) defines whether or
not a term X term-precedes a term Y.

如果 X 和 Y 是相同的术语，那么 X term_precedes Y
和 Y term_precedes X 都是假的.

If X and Y are identical terms then X term_precedes Y
and Y term_precedes X are both false.

如果 X 和 Y 有不同的类型:X term_precedes Y iff
X 的类型按以下顺序在 Y 的类型之前:
变量在浮点数在整数之前
在 atom 之前在 compound 之前.

If X and Y have different types: X term_precedes Y iff the
type of X precedes the type of Y in the following order:
variable precedes floating point precedes integer
precedes atom precedes compound.

注意 —测试术语顺序的内置谓词
在 8.4 中定义.
...

NOTE — Built-in predicates which test the ordering of terms
are defined in 8.4.
...

因此所有变量都小于a.但是一旦 X 被实例化:

And thus all variables are smaller than a. But once X is instantiated:

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

结果无效.

这就是问题所在.为了克服这个问题，可以使用约束，或者只坚持核心行为，因此产生 instantiation_error.

So that is the problem. To overcome this, one might either use constraints, or stick to core behavior only and therefore produce an instantiation_error.

错误按照Error_term的形式分类:

a) 当一个
参数或其组成部分之一是一个变量，并且一个
需要实例化的参数或组件.它有
instantiation_error 的形式.

a) There shall be an Instantiation Error when an
argument or one of its components is a variable, and an
instantiated argument or component is required. It has
the form instantiation_error.

通过这种方式，只要不发生实例化错误，我们就可以确定结果是明确定义的.

In this manner we know for sure that a result is well defined as long as no instantiation error occurs.

对于 (==)/2，已经有 dif/2 使用约束或 iso_dif/2 产生清除实例化错误.

For (==)/2, there is already either dif/2 which uses constraints or iso_dif/2 which produces a clean instantiation error.

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

所以我的问题是关于:如何在 ISO 序言?理想情况下，没有任何明确的术语遍历.也许要澄清一下:上面的 iso_dif/2 没有使用任何显式的术语遍历.(==)/2 和 (=)/2 都在内部遍历该术语，但是与使用 的显式遍历相比，这样做的开销非常低(=..)/2 或 functor/3, arg/3.

So what my question is about: How to define (and name) the corresponding safe term comparison predicates in ISO Prolog? Ideally, without any explicit term traversal. Maybe to clarify: Above iso_dif/2 does not use any explicit term traversal. Both (==)/2 and (=)/2 traverse the term internally, but the overheads for this are extremely low compared to explicit traversal with (=..)/2 or functor/3, arg/3.

推荐答案

iso_dif/2 实现起来比比较简单得多:

iso_dif/2 is much simpler to implement than a comparison:

• 内置 = 运算符可用
• 您现在确切地向=
提供哪些参数

• The built-in = operator is available
• You now exactly what arguments to provide to=

根据您的评论，安全比较意味着如果两个子项中的变量都被实例化，则顺序不会改变.如果我们将比较命名为 lt，例如:

Based on your comments, the safe comparison means that the order won't change if variables in both subterms are instanciated. If we name the comparison lt, we have for example:

• lt(a(X), b(Y)) :始终适用于所有任何 X 和 Y，因为 a @<b
• lt(a(X), a(Y)) :我们不确定:intanciation_error
• lt(a(X), a(X)) :总是失败，因为 X @<X 失败

• lt(a(X), b(Y)) : always holds for all any X and Y, because a @< b
• lt(a(X), a(Y)) : we don't know for sure: intanciation_error
• lt(a(X), a(X)) : always fails, because X @< X fails

正如评论中所说，如果在并行遍历这两个术语时，第一个(可能)有区别的术语对包含:

As said in the comments, you want to throw an error if, when doing a side-by-side traversing of both terms, the first (potentially) discriminating pair of terms contains:

• 两个不相同的变量(lt(X,Y))
• 一个变量和一个非变量(lt(X,a)，或lt(10,Y))

但首先，让我们回顾一下您不想使用的可能方法:

But first, let's review the possible approaches that you don't want to use:

• 定义一个显式的术语遍历比较函数.出于性能原因，我知道您不希望这样做，但仍然是最直接的方法.我还是建议你这样做，这样你就有一个参考实现来与其他方法进行比较.

• Define an explicit term-traversal comparison function. I known you'd prefer not to, for performance reason, but still, this is the most straightforward approach. I'd recommend to do it anyway, so that you have a reference implementation to compare against other approaches.

使用约束进行延迟比较:我不知道如何使用 ISO Prolog 进行比较，但使用例如ECLiPSe，我将暂停对未实例化变量集的实际比较(使用 term_variables/2)，直到没有更多变量为止.以前，我也建议使用 coroutine/0 谓词，但是我忽略了它不影响 @< 运算符(仅 <)的事实.

Use constraints to have a delayed comparison: I don't know how to do it using ISO Prolog, but with e.g. ECLiPSe, I would suspend the actual comparison over the set of uninstanciated variables (using term_variables/2), until there is no more variables. Previously, I also suggested using the coroutine/0 predicate, but I overlooked the fact that it does not influence the @< operator (only <).

这种方法没有解决您描述的完全相同的问题，但它非常接近.一个优点是，如果赋予变量的最终值满足比较，它不会抛出异常，而 lt 在事先不知道时会抛出异常.

This approach does not address exactly the same issue as you describe, but it is very close. One advantage is that it does not throw an exception if the eventual values given to variables satisfy the comparison, whereas lt throws one when it doesn't know in advance.

这是 lt 的显式术语遍历方法的实现，@< 的安全版本.请查看它以检查这是否是您所期望的.我可能错过了一些案例.我不确定这是否符合 ISO Prolog，但如果您愿意，也可以修复.

Here is an implementation of the explicit term traversal approach for lt, the safe version of @<. Please review it to check if this is what you expect. I might have missed some cases. I am not sure if this is conform to ISO Prolog, but that can be fixed too, if you want.

lt(X,Y) :- X == Y,!,
    fail.

lt(X,Y) :- (var(X);var(Y)),!,
    throw(error(instanciation_error)).

lt(X,Y) :- atomic(X),atomic(Y),!,
    X @< Y.

lt([XH|XT],[YH|YT]) :- !,
    (XH == YH ->
         lt(XT,YT)
     ;   lt(XH,YH)).

lt(X,Y) :-
    functor(X,_,XA),
    functor(Y,_,YA),
    (XA == YA ->
       X =.. XL,
       Y =.. YL,
       lt(XL,YL)
    ;  XA < YA).

(考虑到 Tudor Berariu 的评论:(i)缺少 var/var 错误案例，(ii)首先按 arity 排序；此外，修复(i)允许我删除 subsumes_term 为列表.谢谢.)

( taking into account Tudor Berariu's remarks: (i) missing var/var error case, (ii) order by arity first; moreover, fixing (i) allows me to remove subsumes_term for lists. Thanks.)

这是我在不解构术语的情况下达到相同效果的尝试.

Here is my attempt to achieve the same effect without destructuring terms.

every([],_).
every([X|L],X) :-
    every(L,X).

lt(X,Y) :-
    copy_term(X,X2),
    copy_term(Y,Y2),
    term_variables(X2,VX),
    term_variables(Y2,VY),
    every(VX,1),
    every(VY,0),
    (X @< Y ->
         (X2 @< Y2 ->
              true
          ;   throw(error(instanciation_error)))
     ;   (X2 @< Y2 ->
              throw(error(instanciation_error))
          ;   false)).

基本原理

假设 X @<Y 成功.我们要检查关系是否不依赖于一些未初始化的变量.因此，我生成了 X 和 Y 的相应副本 X2 和 Y2，其中所有变量都被实例化:

Rationale

Suppose that X @< Y succeeds. We want to check that the relation does not depend on some uninitialized variables. So, I produce respective copies X2 and Y2 of X and Y, where all variables are instanciated:

• X2中，变量统一为1.
• Y2中，变量统一为0.

• In X2, variables are unified with 1.
• In Y2, variables are unified with 0.

所以，如果关系 X2 @<Y2 仍然成立，我们知道我们不依赖于变量之间的标准术语排序.否则，我们抛出一个异常，因为这意味着一个 1 @<0 关系，以前没有发生，导致关系失败.

So, if the relation X2 @< Y2 still holds, we know that we don't rely on the standard term ordering between variables. Otherwise, we throw an exception, because it means that a 1 @< 0 relation, that previously was not occuring, made the relation fail.

(基于 OP 的评论)

(based on OP's comments)

• lt(X+a,X+b) 应该成功但会产生错误.

• lt(X+a,X+b) should succeed but produce an error.

乍一看，人们可能会认为统一出现在两个术语中且具有相同值的变量，例如 val，可能会解决这种情况.但是，在比较项中可能会出现其他的X，从而导致判断错误.

At first sight, one may think that unifying variables that occur in both terms with the same value, say val, may fix the situation. However, there might be other occurences of X in the compared terms where this lead to an errorneous judgment.

lt(X,3) 应该会产生错误但会成功.

lt(X,3) should produce an error but succeeds.

为了解决这种情况，应该将 X 与大于 3 的值统一起来.在一般情况下，X 应该采用 的值大于其他任何可能的术语¹.除了实际限制之外，@< 关系没有最大值:复合项大于非复合项，根据定义，复合项可以任意大.

In order to fix that case, one should unify X with something that is greater than 3. In the general case, X should take a value that is greater than other any possible term¹. Practical limitations aside, the @< relation has no maximum: compound terms are greater than non-compound ones, and by definition, compound terms can be made arbitrarly great.

所以，这种方法不是决定性的，我认为它不容易纠正.

So, that approach is not conclusive and I don't think it can be corrected easily.

1:请注意，对于任何给定的术语，我们可以找到局部最大和最小术语，这对于问题的目的来说已经足够了.

1: Note that for any given term, however, we could find the locally maximal and minimal terms, which would be sufficient for the purpose of the question.

这篇关于如何在 ISO Prolog 中定义(和命名)相应的安全术语比较谓词?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！