如何在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术语比较中的内建函数的许多其他干净而合理的用法到处都是带有imp(声明式构造的简写形式)的声明性噩梦. 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术语比较

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

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.

这成功了，因为

7.2学期顺序

排序 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如果
X的类型按以下顺序先于Y的类型:
variable之前floating point之前integer
在atom之前.

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.

7.12.2错误分类

错误根据Error_term的形式分类:

7.12.2 Error classification

Errors are classified according to the form of 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 或

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))
   ).

那么我的问题是什么:如何在

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比比较容易实现:

• 内置的\=运算符可用
• 您现在可以确切地提供给\=
的参数

• 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))

• two non-identical variables (lt(X,Y))
• a variable and a non-variable (lt(X,a), or 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)，直到没有更多变量为止.以前，我还建议使用协程/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)首先按人为顺序排序；此外，修复(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的评论)

• 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屋！