如果Prolog中查询无效，SLD树是否存在？

Question

考虑以下 Prolog 程序：

reverse_bits([1], [0]).
reverse_bits([0], [1]).
reverse_bits([H|T], [0|R]) :- H==1, reverse_bits(T, R).
reverse_bits([H|T], [1|R]) :- H==0, reverse_bits(T, R).

上述问题的 SLD 树是什么？

reverse_bits(Input, [1, 0, 0]).?

它无效，那么它是否存在 SLD 树？

Answer 1

这是使用该sldnfdraw包的最小示例。首先，使用库文档中指定的语法生成程序和查询：

% estamos.pl

:- use_module(library(sldnfdraw)).
:- sldnf.

:- begin_program.

reverse_bits([1], [0]).
reverse_bits([0], [1]).
reverse_bits([H|T], [0|R]) :- H==1, reverse_bits(T, R).
reverse_bits([H|T], [1|R]) :- H==0, reverse_bits(T, R).

:- end_program.

:- begin_query.

reverse_bits(Input,[1,0,0]).

:- end_query.

接下来，.tex为相关解析树生成一个文件：

?- draw_goal('estamos-tree.tex').

您可以从命令行运行此目标。最后，将此文件包含在.tex文档中

% estamos-tree-draw.tex

\documentclass{article}
\usepackage{epic,eepic}
\usepackage{ecltree}
\begin{document}
\input{estamos-tree}
\end{document}

并编译

$ latex estamos-tree-draw.tex
$ dvipdf estamos-tree-draw.dvi

.pdf您的源文件夹中应该有一个包含解析树的文件。

代码改进

对于它的价值，我建议将您的程序编写为：

reverse_bits([],[]).
reverse_bits([0|T],[1|R]) :- reverse_bits(T,R).
reverse_bits([1|T],[0|R]) :- reverse_bits(T,R).

为简单起见并避免使用==代替统一，如评论中指出的错误。

使用时的输出=（统一）

这里我们=在“保护部分”测试中使用统一H。

使用时的输出==（术语等价）

使用术语等价时， ==我们很快就完成了，因为第一次调用就失败了：

因为唯一匹配的子句是reverse_bits([H|T], [1|R]) :- H==0, reverse_bits(T, R).and 在那个时候，H是一个新变量，绝不等同于0.