Why not simply fail on a query on ssu-consequences

Defining a clause

p(a) => true.

I got normal answer as I expected.

% ?- p(a). 
%@ true.

However I got errors for the following two queries.

% ?- p(b). 
%@ ERROR: No rule matches ptq:p(b)
%@ ERROR: In:
%@ ERROR:   [12] ptq:p(b)
%@ ERROR:   [11] toplevel_call(ptq:ptq: ...) at /Users/cantor/lib/swipl/boot/toplevel.pl:1317
%@ ^  Exception: (4) setup_call_cleanup('$toplevel':notrace(call_repl_loop_hook(begin, 0)), '$toplevel':'$query_loop'(0), '$toplevel':notrace(call_repl_loop_hook(end, 0))) ? creep

% ?- p(X). 
%@ ERROR: No rule matches ptq:p(_2458)
%@ ERROR: In:
%@ ERROR:   [12] ptq:p(_2508)
%@ ERROR:   [11] toplevel_call(ptq:ptq: ...) at /Users/cantor/lib/swipl/boot/toplevel.pl:1317
%@ ^  Exception: (4) setup_call_cleanup('$toplevel':notrace(call_repl_loop_hook(begin, 0)), '$toplevel':'$query_loop'(0), '$toplevel':notrace(call_repl_loop_hook(end, 0))) ? creep

By analogy to the standard use case , I expected simple fail to both of the queries.

So I have consulted to manual by ?- help('ssu-consequences'), and read the section: 5.6.2 Consequences of => single sided unification rules. Unfortunately still I can’t understand well the errors. What am I missing about
use of =>/2-clause ?

At SWI-Prolog -- Single Sided Unification rules

At a glance, I think the relevant bits on that page are:

  • The subsumes_term/2 guarantees the clause head is more generic than the goal term
  • Should silent failure be desired if no rule matches, this is easily…

I have two common problems when writing Prolog code:

  • a “should always succeed” predicate fails
  • a “should be deterministic” predicate leaves a choicepoint

Two tools help with this: the det/1 directive and SSU.

If you want a set of SSU rules to have a default fail, it’s easy enough to add one final rule:

p(_) => fail.

which is a lot easier than wrapping a non-SSU predicate with some kind of “throw error” if it fails.

There’s a discussion about this somewhere in this group’s archives.

1 Like

I thought => clauses could be used for as term rewriting
rules , but I noticed soon it does not work. So, now I
use explicitly subsumes_term/2 for one_sided head unification when applying rules without => rules, which works fine. (I am reviewing my old broken prolog codes for Montague’s PTQ, whose rule is complicated and tedious for me.)

I tested that the advice works. Thanks. I simply looked only one-sided unification aspect of => clauses as an elegant form of one-sided head unification to apply rewriting rules with non-ground terms in head arguments, which would suppress uses of ‘not willing to see use’ of nonvar/1 from codes, but
which is necessary to be sure that the rule is applicable to given terms without unexpected instantiation of the variables. I have to learn more about =>.