如果查询在 Prolog 中无效，SLD 树是否存在? [英] Does SLD tree exist if the query is invalid in Prolog?

问题描述

考虑以下 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 树吗?

解决方案

这是一个使用 sldnfdraw 包的最小示例.首先，使用

使用==时的输出(术语等价)

当使用

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

Considering the following Prolog 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).

What's the SLD tree for the question above ?

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

It's not valid so does it even exist a SLD tree ?

解决方案

Here is a minimal example using the sldnfdraw package. First, generate a program and query using the syntax specified in the library documentation:

% 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.

Next, generate a .tex file for the relevant resolution tree:

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

You can run this goal from the command line. Finally, include this file in a .tex document

% estamos-tree-draw.tex

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

and compile with

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

There should be a .pdf file in your source folder containing the resolution tree.

Code improvement

For what it's worth I would suggest writing your program as:

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

for simplicity and to avoid using == in place of unification, as false noted in the comments.

Output when using = (unification)

Here we use = unification in the "guard part" testing H.

Output when using == (term equivalence)

When using term equivalence == we are done really quickly because there is failure at the first call:

Because the only clause that matches is reverse_bits([H|T], [1|R]) :- H==0, reverse_bits(T, R). and at that point, H is a fresh variable and in no way equivalent to 0.

这篇关于如果查询在 Prolog 中无效，SLD 树是否存在?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！