我不知道如何阅读这个例子
?- lijstSom(L, 45)
L = [1,2,3,4,5,6,7,8,9],
False
...但是想想谓词lijstSom(List, Sum)
将某些整数列表与其总和相关联,而不是计算整数列表的总和。为什么要“某些清单”?因为我们有这样的约束:整数列表中的整数必须从 1 开始以 1 为增量单调递增。
因此,您可以向 Prolog 处理器询问以下问题:
“说一下第一个参数之间的关系lijstSom/2
和第二个参数lijstSom/2
(假设第一个是单调递增整数的列表,第二个是整数):
lijstSom([1,2,3], Sum)
... 应该返回真(因为是的,至少有一个解决方案)并且give Sum
= 6(因为它也构建了解决方案......我们是某个角落建构主义 here.
lijstSom(L, 6)
... 应该返回真(因为是的,至少有一个解决方案)并且给出解决方案 [1,2,3]
.
lijstSom([1,2,3], 6)
... 应该返回真(因为就是这样,[1,2,3]
总和为 6);不需要更多信息。
lijstSom(L, S)
...应该是无限级数true和成对的解决方案(“生成解决方案”)。
L = [1], S = 1;
L = [1,2], S = 3;
L = [1,2,3], S = 6;
...
lijstSom([1,2,3], 7)
...应该返回错误(“失败”)因为 7 不存在关系lijstSom
with [1,2,3]
如 7 =/= 1+2+3。
人们甚至可能希望 Prolog 处理器说一些有趣的事情:
lijstSom([1,2,X], 6)
X = 3
or even
lijstSom([1,2,X], S)
X = 3
S = 6
实际上,lijstSom/2
尽可能接近数学上的神奇,也就是说:
- 可以不受限制地访问漂浮在柏拉图数学空间中某处的列表求和关系的完整表格。
- 能够以少于无限的步骤找到正确的条目。
- 并输出它。
当然,出于显着的实际原因,我们仅限于低指数和有限数量的可区分符号的多项式算法。糟透了!
所以,首先定义lijstSom(L,S)
使用归纳定义:
-
lijstSom([a list with final value N],S)
... 为真,如果 ...lijstSom([a list],S-N
and
-
lijstSom([],0)
因为空列表的总和为 0。
这很好,因为它给出了最终将任意长度的列表减少到大小为 0 的列表的方法,同时保持完整的知识其总和!
Prolog 不擅长处理列表的尾部,但擅长处理头部,所以我们作弊并更改我们的定义lijstSom/2
说明列表是按相反顺序给出的:
lijstSom([3,2,1], 6)
现在一些代码。
#=
是“包含等于”运算符图书馆(clpfd)。要使用它,我们需要发出use_module(library(clpfd)).
先指挥。
lijstSom([],0).
lijstSom([K|Rest],N) :- lijstSom([Rest],T), T+K #= N.
以上遵循数学要求lijstSom
并允许 Prolog 处理器执行其计算:在第二个子句中,它可以根据大小为 A-1 的列表的值计算大小为 A 的列表的值,“落下”列表长度始终减小的楼梯,直到它达到了终止情况lijstSom([],0).
.
但我们还没有提到单调递减 1 列表。
让我们更准确地说:
lijstSom([],0) :- !.
lijstSom([1],1) :- ! .
lijstSom([K,V|Rest],N) :- K #= V+1, T+K #= N, lijstSom([V|Rest],T).
Better!
(我们还添加了“!”来告诉 Prolog 处理器不要寻找超过这一点的替代解决方案,因为我们对算法的了解比以往任何时候都多。此外,第三行有效,但只是因为我做对了运行下面的测试并让它们通过后。)
如果检查失败,Prolog 处理器将显示“false”——对于您的输入没有解决方案。这正是我们想要的。
但这有效吗?我们在这台卓越的物理机器的“数学性”方面能走多远?
Load library(clpfd)
用于约束和使用library(plunit)对于单元测试:
将其放入文件中x.pl
你可以加载[x]
alias consult('x')
或重新加载make
在 Prolog REPL 上:
:- use_module(library(clpfd)).
lijstSom([],0) :-
format("Hit case ([],0)\n"),!.
lijstSom([1],1) :-
format("Hit case ([1],1)\n"),!.
lijstSom([K,V|Rest],N) :-
format("Called with K=~w, V=~w, Rest=~w, N=~w\n", [K,V,Rest,N]),
K #= V+1,
T+K #= N,
T #> 0, V #> 0, % needed to avoid infinite descent
lijstSom([V|Rest],T).
:- begin_tests(listsom).
test("0 verify") :- lijstSom([],0).
test("1 verify") :- lijstSom([1],1).
test("3 verify") :- lijstSom([2,1],3).
test("6 verify") :- lijstSom([3,2,1],6).
test("0 construct") :- lijstSom(L,0) , L = [].
test("1 construct") :- lijstSom(L,1) , L = [1].
test("3 construct") :- lijstSom(L,3) , L = [2,1].
test("6 construct") :- lijstSom(L,6) , L = [3,2,1].
test("0 sum") :- lijstSom([],S) , S = 0.
test("1 sum") :- lijstSom([1],S) , S = 1.
test("3 sum") :- lijstSom([2,1],S) , S = 3.
test("6 sum") :- lijstSom([3,2,1],S) , S = 6.
test("1 partial") :- lijstSom([X],1) , X = 1.
test("3 partial") :- lijstSom([X,1],3) , X = 2.
test("6 partial") :- lijstSom([X,2,1],6) , X = 3.
test("1 extreme partial") :- lijstSom([X],S) , X = 1, S = 1.
test("3 extreme partial") :- lijstSom([X,1],S) , X = 2, S = 3.
test("6 extreme partial") :- lijstSom([X,2,1],S) , X = 3, S = 6.
test("6 partial list") :- lijstSom([X|L],6) , X = 3, L = [2,1].
% Important to test the NOPES
test("bad list", fail) :- lijstSom([3,1],_).
test("bad sum", fail) :- lijstSom([3,2,1],5).
test("reversed list", fail) :- lijstSom([1,2,3],6).
test("infinite descent from 2", fail) :- lijstSom(_,2).
test("infinite descent from 9", fail) :- lijstSom(_,9).
:- end_tests(listsom).
Then
?- run_tests(listsom).
% PL-Unit: listsom ...................... done
% All 22 tests passed
什么会Dijkstra说?是的,他可能会抱怨一些事情。