3

关于这个主题的维基百科部分是一团糟。它指出：

Pure Prolog基于一阶谓词逻辑的子集 Horn 子句，它是图灵完备的。Prolog的图灵完备性可以通过使用它来模拟图灵机来展示：

（重点补充）

然后它继续显示使用非 Horn 子句（!和once）的代码：

turing(Tape0, Tape) :-
    perform(q0, [], Ls, Tape0, Rs),
    reverse(Ls, Ls1),
    append(Ls1, Rs, Tape).
 
perform(qf, Ls, Ls, Rs, Rs) :- !.
perform(Q0, Ls0, Ls, Rs0, Rs) :-
    symbol(Rs0, Sym, RsRest),
    once(rule(Q0, Sym, Q1, NewSym, Action)),
    action(Action, Ls0, Ls1, [NewSym|RsRest], Rs1),
    perform(Q1, Ls1, Ls, Rs1, Rs).
 
symbol([], b, []).
symbol([Sym|Rs], Sym, Rs).
 
action(left, Ls0, Ls, Rs0, Rs) :- left(Ls0, Ls, Rs0, Rs).
action(stay, Ls, Ls, Rs, Rs).
action(right, Ls0, [Sym|Ls0], [Sym|Rs], Rs).
 
left([], [], Rs0, [b|Rs0]).
left([L|Ls], Ls, Rs, [L|Rs]).

rule(q0, 1, q0, 1, right).
rule(q0, b, qf, 1, stay).

好的，所以 Prolog 是图灵完备的。没有人怀疑这一点。纯Prolog 呢？

如果纯 Prolog 实际上是图灵完备的，为什么我们似乎无法在其中实现列表交集（第一个列表按第二个列表中的成员资格过滤）？所有实现都至少使用以下之一：!, \+, findall,call直接或间接。

4

3 回答 3

4

为什么我们似乎无法在其中实现列表交集（第一个列表由第二个列表中的成员资格过滤）？所有实现都至少使用以下之一：!, \+, findall,call直接或间接。

请注意，使用的答案if_/3根本不需要任何剪切​​。剪切（或 if-then-else）仅出于性能和稳健性的原因（即捕获确定的情况并在意外使用的情况下发出错误信号）。您可以将其全部扩展为没有任何此类结构的版本。它将以相同的方式终止，但在当前实现中效率较低。

以下是和的纯化if_/3版本(=)/3：

if_(If_1, Then_0, Else_0) :-
   call(If_1, T),
   (  T = true, call(Then_0)
   ;  T = false, call(Else_0)
   %;  nonvar(T) -> throw(error(type_error(boolean,T),_))
   %;  /* var(T) */ throw(error(instantiation_error,_))
   ).

=(X, X, true).
=(X, Y, false) :-
   dif(X,Y).

而且，如果您不接受call/2and call/1（毕竟两者都不是一阶逻辑的一部分），您将不得不相应地扩展每个用途。换句话说，所有的使用if_/3都使得这样的扩展是可能的。

至于图灵完备性，这已经使用单一规则建立。请参阅此问题以及其中包含的参考资料，这是如何可能的（实际上并不那么直观）。

于 2020-12-18T19:56:57.197 回答
2

您可以使用您的语言构建图灵机，从而将当前磁带和内部状态表示为“累加器项”。只是你不能使用“！” 承诺选择一个基本确定性“证明”的子句，因此除了不断增长的术语之外，真正的实现将充满不断增长的堆栈（将永远不会再次访问）。但是在图灵宇宙中，空间是自由的，时间是无限的，热力学上可用的能量是丰富的（而且周围有一个很大的散热器）。不用担心！

实际上，在纯 Prolog 中构建 Marvin Minsky 的最小通用图灵机是一个很好的练习。

编辑：这个“相交”的实现怎么样。少了什么东西？

% horn_intersect(++List1,++List2,?List3)
% List3 is the intersection of List1 and List2
% Assumptions: 
% 1) All the members of List1, List2, List3 are grounded
%    No unbound variables (a non-logical concept)
% 2) We don't care about determinism. The same solution
%    may be generated several times (as long as it's right)
%    Choicepoints are not removed.
% 3) There is a dataflow direction: (List1,List2) --> List3.
%    This also ensures that this is a function (only one solution,
%    though represented by a set of equivalent solutions)
%    These are not foreseen:
%    Going the other ways (List1,List3) --> "an infinite set of List2 templates"
%    Going the other ways (List2,Listd) --> "an infinite set of List1 templates"
%    Going the other ways List3         --> "an infinite set of (List1,List2) templates tuples"
%    However, accepting a (List1,List2,List3) is ok.

horn_intersect([],_,[]).
horn_intersect(_,[],[]).

horn_intersect([X|Xs],List2,[X|Ms]) :- in(X,List2),horn_intersect(Xs,List2,Ms).
horn_intersect([X|Xs],List2,Ms)     :- not_in(X,List2),horn_intersect(Xs,List2,Ms).

in(X,[X|_]).
in(X,[K|Ms]) :- X\=K,in(X,Ms).

not_in(_,[]).
not_in(X,[K|Ms]) :- X\=K,not_in(X,Ms).

:- begin_tests(horn_horn_intersect).

test(1,[true,nondet])           :- horn_intersect([a,b,c],[a,b,c],[a,b,c]).
test(2,[true,nondet])           :- horn_intersect([b],[a,b,c],[b]).
test(3,[true,nondet])           :- horn_intersect([a,b,c],[b],[b]).
test(4,[true,nondet])           :- horn_intersect([a,b,c],[],[]).
test(5,[true,nondet])           :- horn_intersect([],[a,b,c],[]).
test(6,[true,nondet])           :- horn_intersect([x,y],[a,b],[]).
test(7,fail)                    :- horn_intersect([x,y],[a,b],[u,v]).
test(8,[Out == [], nondet])     :- horn_intersect([x,y],[a,b],Out).
test(9,[Out == [a,b], nondet])  :- horn_intersect([a,b,c],[a,b],Out).
test(10,[Out == [a,b], nondet]) :- horn_intersect([a,b],[a,b,c],Out).
test(11,[Out == [], nondet])    :- horn_intersect([x,y],[a,b],Out).
   
:- end_tests(horn_horn_intersect).
于 2020-12-18T09:56:54.217 回答
1

如果您将状态编码为Peano 数字，则使用 0 表示停止。
和 s(X) 用于所有非暂停状态。然后你不需要削减：

perform(0, Ls, Ls, Rs, Rs).
perform(s(Q0), Ls0, Ls, Rs0, Rs) :-
    symbol(Rs0, Sym, RsRest),
    rule(s(Q0), Sym, Q1, NewSym, Action),
    action(Action, Ls0, Ls1, [NewSym|RsRest], Rs1),
    perform(Q1, Ls1, Ls, Rs1, Rs).


但是您也可以通过证明纯 Prolog 可以在 Peano 数内进行µ 递归来展示“计算完整性” 。

于 2020-12-18T15:03:35.543 回答