Prolog元解释器与单边统一

Question

我尝试了这个普通的解释器：

solve(true) :- !, true.
solve(X is E) :- !, X is E.
solve((A,B)) :- !, solve(A), solve(B).
solve(H) :- clause(H,B), solve(B).

我们可以用它来元解释一些代码吗？我试过这个代码，

需要SWI-Prolog 8.3.19，运行正常：

sumlist([X|Y], R) => sumlist(Y, H), R is X+H.
sumlist([], R) => R is 0.

?- sumlist([1,2,3],X).
X = 6.

?- sumlist(X,Y).
ERROR: No rule matches sumlist(_21604,_21606)

但是元解释出了问题。原因是第/2条

不知道使用单边统一的规则：

?- clause(sumlist(A,B),C).
A = [_22728|_22730],
C =  (sumlist(_22730, _22736), B is _22728+_22736) ;
A = [],
C =  (B is 0).

?- solve(sumlist([1,2,3],X)).
X = 6.

?- solve(sumlist(X,Y)).
SWI-Prolog wurde unerwartet beendet.

元解释器和单边统一有解决方案吗？

Answer 1

走出困境并保持在国际标准化组织核心标准中的一种方法是将单边统一转换为nonvar/1，(=)/2和(==)/2的组合，如下所示：

?- clause(sumlist(X,Y),Z), write((sumlist(X,Y):-Z)), nl, fail; true.
sumlist(_A, _B) :- nonvar(_A), _A = [_C|_D], sumlist(_D, _E), _B is _C+_E
sumlist(_A, _B) :- nonvar(_A), _A = [], _B is 0

当然，我们还需要将内置的nonvar/1、(=)/2和(==)/2添加到元解释器中：

solve(true) :- !.
solve(X is E) :- !, X is E.
solve(nonvar(X)) :- !, nonvar(X).
solve(X == Y) :- !, X == Y.
solve(X = Y) :- !, X = Y.
solve((A, B)) :- !, solve(A), solve(B).
solve(H) :- clause(H, B), solve(B).

元解释sumlist/2现在可以正常工作了：

?- solve(sumlist([1,2,3],X)).
X = 6

?- solve(sumlist(X,Y)).
No

但翻译者可能会挑战Prolog系统，涉及到子句索引。它将函数器从头部移动到身体。因此，Prolog系统需要一些身体前端索引，就像YAP首创的那样，并在Jekejeke Prolog中找到。

开源：

还有另一个模式匹配器

https://gist.github.com/jburse/a3517410a28b759ef44f72584f89aaf8#file-picat3-pl

Vanilla解释器，扩展解决方案

https://gist.github.com/jburse/a3517410a28b759ef44f72584f89aaf8#file-vanilla4-pl