Prolog 解绑绑定变量 [英] Prolog unbind bound variable

问题描述

我有这个跟踪元解释器.它是为 swi-prolog 编写的.

I have this tracing meta interpreter. It is written for swi-prolog.

trace(Goal):-
        trace(Goal, 0).

trace(true, _Depth):-!, true.
trace(fail, _Depth):-!, fail.
trace(A > B, _Depth):-!, A > B.
trace(A < B, _Depth):-!, A < B.
trace(A <= B, _Depth):-!, A <= B.
trace(A >= B, _Depth):-!, A >= B.
trace(A = B, _Depth):-!, A = B.
trace(A is B, _Depth):-!, A is B.
trace(!, _Depth):-!, fail.
trace(not(A), _Depth):-!, not(A).
trace((Goal1, Goal2), Depth):-!,
        trace(Goal1, Depth),
        trace(Goal2, Depth).
trace(Goal, Depth):-
        display('Call: ', Goal, Depth),
        clause(Goal, Body),
        Depth1 is Depth + 1,
        trace(Body, Depth1),
        display('Exit: ', Goal, Depth),
        display_redo(Goal, Depth).
trace(Goal, Depth):-
        display('Fail: ', Goal, Depth),
        fail.

display(Message, Goal, Depth):-
        tab(Depth), write(Depth), write(': '), write(Message),
        write(Goal), nl.

display_redo(Goal, Depth):-
        true
        ;
        display('Redo: ', Goal, Depth),
        fail.

just_do_it(In, Out, Query):-
        consult(In),
        tell(Out),
        call_with_depth_limit(findall(Query, trace(Query), _Solutions), 30, _XMessage),
        writeln(_XMessage),
        writeln(_Solutions),
        told,
        unload_file(In),
        true.

它工作正常，除了一件事之外应该如何.当我在函数 just_do_it(In, Out, Query) 的 Query 中有变量时，输出带有绑定变量.是否有某种方法可以在进一步的跟踪步骤中取消绑定变量，以便我可以看到它何时绑定，何时未绑定?

It is working fine and how it should except one thing. When I have variable in Query in function just_do_it(In, Out, Query), the output is with binded variable. Is there some way to unbind the variable in further steps of tracing so I could see when it is binded and when not?

示例输出:

0: Call: a(_G1085,_G1085,_G1087)
0: Exit: a(3,3,7)
0: Redo: a(3,3,7)
  1: Call: b(_G1087,_G1085)
  1: Exit: b(7,3)
  1: Redo: b(7,3)
  1: Exit: b(5,1)
  1: Redo: b(5,1)
  1: Fail: b(_G1087,_G1085)
0: Fail: a(_G1085,_G1085,_G1087)

我想要的输出示例:

0: Call: a(_G1085,_G1085,_G1087)
0: Exit: a(3,3,7)
0: Redo: a(_G1085,_G1085,_G1087)
 1: Call: b(_G1087,_G1085)
 1: Exit: b(7,3)
 1: Redo: b(_G1087,_G1085)
 1: Exit: b(5,1)
 1: Redo: b(_G1087,_G1085)
 1: Fail: b(_G1087,_G1085)
0: Fail: a(_G1085,_G1085,_G1087)

推荐答案

你的解释器有几个问题:

There are several issues with your interpreter:

您正在使用不存在的运算符 <=.所以你必须得到一个语法错误.在 Prolog 中，less-then-or-equal 是 =< 以避免与箭头 ⇐/<= 混淆.

You are using an operator <= which does not exist. So you must get a syntax error on this. In Prolog less-then-or-equal is =< to avoid confusion with an arrow ⇐ / <= .

您正在定义一个谓词 trace/1，但是 SWI 和许多其他 Prolog 一样已经预定义了这个谓词.所以最好换个名字.

You are defining a predicate trace/1, but SWI as many other Prologs have this predicate already predefined. So better use another name.

切割没有正确实施.

not/1 的规则应该定义 (\+)/1，并且可以读作:

The rule for not/1 should rather define (\+)/1, and could read:

trace(\+A, Depth):-!, \+trace(A, Depth).

证明变量应该导致instantiation_error.就像在 call(_) 中一样.所以你需要作为第一条规则

Proving variables should result in an instantiation_error. Like in call(_). So you need as first rule

trace(V, _) :- var(V), !, throw(error(instantiation_error, _)).

<小时>

要正确显示重做，您需要以更明确的方式替换目标clause(Goal, Body),.毕竟，除了通过回溯之外，没有办法解除变量的绑定.也就是说，我们必须找到变量仍未实例化的正确时刻.将 clause/2 替换为 redo_clause/3.

---

To display redo correctly, you need to replace the goal clause(Goal, Body), by a more explicit way. After all, there is no way to unbind variables, except via backtracking. That is, we have to find the right moment where the variables are still uninstantiated. Replace clause/2 by redo_clause/3.

redo_clause(Depth, Goal, Body) :-
   findall(Goal-Body, clause(Goal, Body), [First|Rest]),
   ( Goal-Body = First
   ; length(Rest, RL), length(RestC, RL),
     member(Goal-Body,RestC),
     display('Redo: ', Goal, Depth),
     Rest = RestC
   ).

这篇关于Prolog 解绑绑定变量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！