Prolog (swi-pl) 中长度/2 的逻辑推理次数

Question

我预计内置 length/2 谓词与逻辑推理的数量呈线性关系。然而，它似乎是恒定的：

?- length(L,10),time(length(L,X)).
% 2 inferences, 0.000 CPU in 0.000 seconds (63% CPU, 142857 Lips)

?- length(L,20),time(length(L,X)).
% 2 inferences, 0.000 CPU in 0.000 seconds (62% CPU, 153846 Lips)

?- length(L,30),time(length(L,X)).
% 2 inferences, 0.000 CPU in 0.000 seconds (65% CPU, 111111 Lips)

这是因为程序被委托给C了吗？我在 SWIPL 代码库中找不到相关代码。

Answer 1

length/2 在 init.pl 的第 3230 行附近有一个浅但功能强大的接口。从这里开始'$skip_list'(Length0, List, Tail)，它被称为C 接口的“瑞士刀”。

您可以在 src/pl-prims.c 第 2377 行及以下位置找到它：

/** '$skip_list'(-Length, +Xs0, -Xs) is det.

Xs0, Xs is a pair of list differences. Xs0   is the input list and Xs is
the minimal remaining list. Examination of   Xs  permits to classify the
list Xs0:

        Xs        | list type of Xs0   | Length
        []    ... | well formed        | length
        Var   ... | partial            | elements skipped
        [_|_] ... | infinite           | upper bound for cycle
        Term  ... | malformed          | elements skipped
*/
PRED_IMPL("$skip_list", 3, skip_list, 0)
...