Why does SWI-Prolog invent f/2 given only f/1?

3
votes

SWI-Prolog 7.6.4:

?- dif(X, f(Y)), X=f(a).
X = f(a),
dif(f(f(a), Y), f(f(Y), a)).

Note that I use f/1 in the query, but the constraint is on f/2. It's not wrong, but seems rather circuitous. Why doesn't Prolog return

?- dif(X, f(Y)), X=f(a).
X = f(a),
dif(Y, a).
1
prologswi-prologprolog-dif
seems a bug... sorry I haven't a constructive answer, most probably you should post on SWI-Prolog discourse. Jan W. always provides fast and accurate analysis and patches – CapelliC

1 Answers

3
votes

That f in the printed constraint has nothing to do with your f. It's just a placeholder to keep subterms together:

?- dif(X, incal(Y)), X=incal(a).

X = incal(a),

dif(f(incal(a), Y), f(incal(Y), a)).    <--- residual constraints, not yet resolved

The above meaning just that:

  • incal(a) must stay different from incal(Y); and
  • Y must stay different from a

Yes, you could simplify that but ... when does one know whether optimization will cost less than one will gain?