performance - 将谓词应用于 Prolog : requesting advice on implementation choices 中列表的子集

Question

编辑:在我提到列出的第二个是首先我尝试实现，所以我改写了相关段落。抱歉造成混淆。

一些动机背景:我正在 SWI Prolog 中构建一个约束求解器，为了极大地优化空间和时间，我在主要约束数据结构中构建了一个反向索引。每当我的系统中的“变量”(不是 Prolog 变量)被赋值时，我想确保这个赋值不会使任何其他约束无法满足。我有一个从变量到约束的索引，可以快速选择要检查的约束。从某种意义上说，这归结为将 try_check/2 谓词应用于给定的左侧 (LHS) 和右侧列表 (RHS_L) 的所有元素，这些元素的索引出现在列表 (IdxL) 中.这是我当前的实现:

%% FORALL Implementation
try_check_filtered(LHS, IdxL, RHS_L) :-
    forall((member(Idx, IdxL), nth0(Idx, RHS_L, RHS)), 
           try_check(LHS, RHS)).

我还有一个较早的实现，它做同样的事情，但在第二个位置使用一个额外的参数来跟踪当前列表索引(索引列表按升序排序):

%% Tail-Recursive Implementation
%%try_check_filtered(+LHS, +Idx, +IdxL, +RHS_L)
try_check_filtered(_LHS, _Idx, [], _RHS_L) :- !.    % Stop when index list is empty
try_check_filtered(LHS, Idx, [Idx|Ti], [H|T]) :- !, % If at next index -> check
    try_check(LHS, H),
    Inext is Idx+1,
    try_check_filtered(LHS, Inext, Ti, T).
try_check_filtered(LHS, Idx, IdxL, [_H|T]) :-       % If not at next index -> skip
    Inext is Idx+1,
    try_check_filtered(LHS, Inext, IdxL, T).
try_check_filtered(_LHS, _Idx, _IdxL, []).           % Done when at the end of RHS_L

我有两个问题:

1. 有没有我想不到的更好的实现方法？
2. 我惊讶地发现 forall 实现比尾递归执行得更好。在我看来，尾递归具有线性时间分派(dispatch)(沿着列表走一次以“调​​用”所有必要的 try_check)，而 forall 实现具有二次分派(dispatch)(对成员的线性调用次数，每次调用都会导致另一个线性调用第 n 个)。 (如果您对我看到的性能改进感到好奇，在大约 44 秒的执行过程中，在尾递归上使用 forall 实现可以节省大约 4 秒)。

我的一个想法是尾递归优化没有应用到我的尾递归实现中，迫使列表的多个副本进入堆栈帧，从而使它变慢。为了(希望)为我的尾递归实现启用尾递归优化，我试图通过在规则末尾添加一个 cut (!) 来使我的 try_check/2 谓词具有确定性。够了吗？ try_check/2 规则有暂时的副作用是否重要:它断言了一些事实，它在完成之前撤回了这些事实，从而使事实集合保持不变。我上面报告的性能是在 try_check/2 谓词中的削减。

我希望我提供了足够的信息来进行建设性的讨论。预先感谢您的回复!

编辑:这是 try_check 的(高级)实现。整个代码2600行，其中很多(大概一半)是被这个检查间接用到的，所以这里无法贴出。

%% try_check_eni(+E1:effect, +E2:effect)
try_check_eni(E1, E2) :-
    push_trying,
    check_no_try,
    ( is_non_interfering(E1, E2)
    -> (clear_try, pop_trying)
    ; (clear_try, pop_trying, fail))
    , !.

push_trying/0 和 pop_trying/0 断言和收回一个 trying/0 谓词，它稍微修改了一些其他谓词的操作方式，这样我就不必为 try_check 谓词复制检查谓词所使用的代码。 is_non_interfering/2 是不确定的。在trying 模式下，is_non_interfering 将实例化变量标记为try/1 以便实例化可以通过clear_try/0 收回> 检查约束后。

Answer 1

nth0/3 具有线性成本。因此，与 member/2 和 forall/2 的组合具有二次成本。事实上，第二个代码变体没有利用索引列表按升序排列的事实，而第一个变体做到了。

在这个开发阶段尽量不要过度优化:首先正确执行，然后(并且只有这样)快速执行。

专注于清晰可读的代码，选择合适的数据结构，做出正确的库选择...如果情况需要，您可以将列表中的随机读取访问替换为，比如说，一些复合结构加上 arg/3.

此外，您的代码可能会受益于第一个参数索引。使用 cut 和/或 assert/retract 时要小心，这两者很容易降低正确性和性能。