Hi guys,

I cannot interpret the output of the query below. In fact I no not understand why this does not fail.
Can someone enlighten me?


?- clause(\+ p(X),B).
B = (\+call(p(X)))

You don’t need to define any p/1 to get the exactly same result:

$ swipl -q
?- clause(\+ p(X), B).
B = (\+call(p(X))).

Does that give you an idea what you might be seeing?

But what are you trying to achieve?

The meta predicate (\+)/1 with a stable argument is usually
compiled away. Namely \+ X can be compiled along (X->fail;true):

test :- \+ foo.

?- vm_list(test).
       0 i_enter
       1 c_not(0,'L1')
       4 i_call(user:foo/0)
       6 c_cut(0)
       8 c_fail
L1:    9 i_exi

But it has a stub definition. So that it can be dynamically called.
The stub defintion becomes visible when doing listing:

?- listing((\+)/1).
:- meta_predicate\+0.

system:\+Goal :-
    \+ call(Goal).

Via clause/2, since clause/2 works also for static predicates in
SWI-Prolog, the clause/2 call simply retrieves the above clause.


Thank you guys for your answer. I definitely lack some knowledge on how Prolog is implemented to fully understand your answers. But I understand that there is a system clause defining + Goal explaining why clause(\+ p(X), B) did not fail, but still I find it difficult to interpret it. @Boris, I was trying to write a small meta interpreter. I had a bug in my program and the reason was that I assumed that clause(\+ p(X), B) would fail.

You should still explain what exactly you think this query means. What you are really doing here:

?- clause(\+ p(X), B).

Is that you are posing the query:

Could you please unify B with the body of the clause that has a head that unifies with \+ p(X).

And since (\+/1) is a meta-predicate, yes, you can unify \+ Foo for any Foo whatsoever:

$ swipl -q
?- clause(\+ Foo, Body).
Body = (\+call(Foo)).

Now that I think about it, did you mean to ask,

?- \+ clause(p(X), B).


Most Prolog systems do not allow for clause/2 to work on static code. SWI-Prolog does. ISO demands a permission error though, so that won’t fix your meta interpreter either. You typically need predicate_property/2 for deciding when you want to use clause/2.

As of \+/1, if you want your meta interpreter to handle that, you can’t just call it as that would stop meta-interpreting the argument goal. So, you end up with something like

solve(Var) :- var(Var), !, instantiation_error(Var).
solve(true) :- !.
solve((A,B)) :- !, solve(A), solve(B).
solve(\+A) :- !, \+ solve(A).
solve(A) :- predicate_property(A, foreign), !, call(A).
solve(A) :- clause(A, Body), solve(Body).

The … are for some more things you may wire into the meta-interpreter or may want to call rather than meta-interpreting. Note that handling modules, cuts and meta-predicates complicate the whole story further.

Thank you Jan. You meta-interpreter is basically what I wrote. But because I did not insert the cut in the body of the fourth rule, it backtracked on the last rule and this is not what I wanted.