为什么 SWI-Prolog 只给出 f/1 就发明了 f/2？

问题描述

SWI-Prolog 7.6.4：

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

请注意，我在查询中使用了 f/1，但约束在 f/2 上。这没有错，但似乎相当迂回。为什么Prolog不返回

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

解决方法

打印约束中的 f 与您的 f 无关。这只是将子术语保持在一起的占位符：

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

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

上面的意思就是：

• incal(a) 必须与 incal(Y) 不同；和
• Y 必须与 a 保持不同

是的，您可以简化它，但是……何时才能知道优化的成本是否会低于收益？