前言: McCarthy 91

Question

我正在学习关于递归的知识，并遇到了McCarthy 91 function。

我已经找到了几种语言的示例(C++、Java、Python、Scheme等等)。我正在试着找出它是如何用Prolog编写的。

我在网上找不到任何例子，我也不知道如何自己写(用Prolog)。有没有人可以在网上发布一个代码示例，或者给我指出合适的源代码？非常感谢你的帮助。

Answer 1

下面是一个使用lifter的SWI-Prolog测试(为了更容易理解，我保留了上面注释的非left子句)。

:- [lifter].

%m(N, M) :- N > 100 -> M is N-10 ; T1 is N+11, m(T1, T2), m(T2, M).
 m(N, M) :- N > 100 -> M is N-10 ; m(m(° is N+11, °), M).

下面是纯Prolog的翻译(当然与Sergey one相同，在重命名变量之后)

6 ?- listing(m).
m(A, B) :-
    (   A>100
    ->  B is A-10
    ;   C is A+11,
        m(C, D),
        m(D, B)
    ).

true.

7 ?- writeln(m(88,°)).
91
true.

Answer 2

m91(N, M) :-
    ( N > 100 ->
        M is N - 10
    ;
        Np11 is N + 11,
        m91(Np11, M1),
        m91(M1, M)
    ).

它不是一个真正的函数，而是一个谓词。结果在第二个参数中被“返回”：

?- m91(99, M).
M = 91.

?- m91(87, M).
M = 91.

?- m91(187, M).
M = 177.

一些Prolog实现允许使用这样的谓词作为算术函数。使用ECLiPSe

[eclipse]: M is m91(99).
M = 91
Yes (0.00s cpu)

Answer 3

这里有几个值得注意的方面。毕竟，这个功能的初衷是在正式验证的背景下考虑它。

只要你用(is)/2对这个函数进行编码，你就会得到与其他语言中基本相同的结果--这是一个你需要推理的函数。您需要从(is)/2的模算法切换到library(clpfd)提供的(基本)代数，以便直接将Prolog转换为关于关系的推理：

:- use_module(library(clpfd)).

m(N0,N):-
   N0#>100,
   N #= N0-10.
m(N0,N):-
   N0#=<100,
   N1 #=N0+11,
   m(N1,N2),
   m(N2,N).

现在，我们不仅可以要求一个具体的结果，我们还可以要求：

?- m(N0,N).
N0 in 101..sup,
N+10#=N0,
N in 91..sup ;
N0 = 100,
N = 91 ;
N0 = 99,
N = 91 ;
N0 = 98,
N = 91 ;
N0 = 97,
N = 91 ...

或者，更具体地说，我们可能会问这个“函数”何时不等于91：

?- N#\=91, m(N0,N).
N in 92..sup,
N+10#=N0,
N0 in 102..sup ; LOOPS

第一个答案告诉我们，对于值N0 in 102..sup，结果不会是91。然后，系统试图找到下一个答案，但需要太多时间(也就是说，对于我们有限的生命来说，太多时间)。

理想情况下，我们应该像这样实现m/2：

m2(N0,N) :-
   N0#>100,
   N #= N0-10.
m2(N0,N):-
   N0#=<100,
   N #= 91.

而事实上，这将是一个对程序转换系统的挑战。m2/2允许Prolog使用两个答案来描述整个关系：

?- m2(N0,N).
N0 in 101..sup,
N+10#=N0,
N in 91..sup ;
N = 91,
N0 in inf..100.

所以我们在这里用有限的方法描述了无限多的解！