Prolog中两个整数的递归定义函数（分区函数）

Question

我发誓这不是作业题。我已经几十年没参加类了。曾几何时，我想出了一个可爱的分区函数递归公式：

         / 0 (k > n)
f(k, n) {  1 (k = n)
         \ p(k, n-k)+p(k+1, n) (k < n)

我想尝试在序言中表示这一点。这是我所能得到的：

partition(N, N, 1) :- !. %% 

partition(K, N, 0) :- K > N.

partition(K, N, A+B) :-
 X is K+1,
 Y is N-K,
 partition(X, N, A),
 partition(K, Y, B).

?- partition(1, 10, X). 给我这个：

X = 1+0+0+0+0+1+(1+0+0)+(1+0+0+0+(1+0))+(1+0+0+0+1+(1+0+0)+(1+0+0+1+(1+0+1)))+(1+0+0+0+0+(1+0)+(1+0+0+1)+(1+0+0+0+(1+0)+(1+0+0+(1+0)))+(1+0+0+0+1+(1+0+0)+(1+0+0+1+(1+0+1))+(1+0+0+0+(1+0)+(1+0+0+(1+0))+(1+0+0+1+(1+0+1)+(1+0+0+(1+0)+(1+0+1+(1+0+(1+1)))))))) ?

令人欣慰的是，上面的表达式中确实有 42 个（？）。我希望 X=42. 注意问号。是的，有更多的比赛（显然无限多）。第二个是：

X = 1+0+0+0+0+1+(1+0+0)+(1+0+0+0+(1+0))+(1+0+0+0+1+(1+0+0)+(1+0+0+1+(1+0+1)))+(1+0+0+0+0+(1+0)+(1+0+0+1)+(1+0+0+0+(1+0)+(1+0+0+(1+0)))+(1+0+0+0+1+(1+0+0)+(1+0+0+1+(1+0+1))+(1+0+0+0+(1+0)+(1+0+0+(1+0))+(1+0+0+1+(1+0+1)+(1+0+0+(1+0)+(1+0+1+(1+(0+0)+(1+1)))))))) ?

Answer 1

I swear this isn't a homework problem. I haven't attended classes in decades.

冷静点，就算是作业，只要你做了合理的努力，寻求帮助就没有问题（合理当然是主观的，但我认为是好的问题）你自己，更多的是你的实施有一个特定的问题:)。

您的方法的问题在于您（在许多人中）认为 Prolog 将语义附加到仿函数。 对于Prolog +不是加法，也不是把东西加起来，+只是一个符号，不求值.

然而，有一个谓词评估表达式树并使用 "semantics" 大多数人都同意的。那就是 is/2 谓词。所以现在你可以简单地将它修改为：

partition(K, N, C) :-
    X is K+1,
    Y is N-K,
    partition(X, N, A),
    partition(K, Y, B),
    C is A+B.

Yes, there are more matches (apparently infinitely more).

那是因为你的最后一个子句没有 guard 表示 K < N，换句话说，Prolog 将 backtrack 而不管K 和 N 如何相互关联，它总是可以选择最后的子句（K == N 除外，因为你在那里放置了一个剪切（!））。

您最好在最后一个子句中使用“guard”，否则在回溯时可以调用 if K < N。所以完整的代码序列应该是这样的：

partition(N, N, 1) :- !. %% 

partition(K, N, 0) :- K > N.

partition(K, N, C) :-
    K < N,
    X is K+1,
    Y is N-K,
    partition(X, N, A),
    partition(K, Y, B),
    C is A+B.

请注意 is/2 没有什么特别之处：它只是一个谓词：您也可以用 is(C,A+B) 调用它。它只是以这样一种方式定义的，它也可以用作中缀运算符。

使用给定的子句，查询给出：

?- partition(1, 10, X).
X = 42 ;
false.

Prolog中两个整数的递归定义函数（分区函数）

Recursively defined function of two integers in Prolog (partition function)

recursion

prolog

number-theory