验证SICStus Prolog中copy_term/3处理attribute_goal/2目标的结论是否正确

我正在使用SICStus Prolog的属性变量（attributed variables）接口编写求解器，初始代码如下：

:- module(attach2, [attach2/2]).
:- use_module(library(atts)).
:- attribute att/2.

attach2(X,Y) :- put_atts(X,att(X,Y)),
                put_atts(Y,att(Y,X)).

verify_attribute(_,_,[]).

attribute_goal(V,(true,G,true,G,true)) :- get_atts(V,att(X,Y)), G = attach2(X,Y).

对应的示例查询结果：

| ?- attach2(X,Y), copy_term(X,Xc,Xcc), copy_term(Y,Yc,Ycc), copy_term(X+Y,XYc,XYcc).
Xcc = attach2:(true,attach2(Xc,_A),true,attach2(Xc,_A),true),
Ycc = attach2:(true,attach2(Yc,_B),true,attach2(Yc,_B),true),
XYc = _C+_D,
XYcc = (attach2:attach2(_C,_D),attach2:attach2(_D,_C)),
attach2(X,Y),
attach2(Y,X) ? ;
no

若将attach2/2修改为：

attach2(X,Y) :- put_atts(X,att(X,Y)),
                put_atts(Y,att(X,Y)).

查询结果得到优化：

| ?- attach2(X,Y), copy_term(X,Xc,Xcc), copy_term(Y,Yc,Ycc), copy_term(X+Y,XYc,XYcc).
Xcc = attach2:(true,attach2(Xc,_A),true,attach2(Xc,_A),true),
Ycc = attach2:(true,attach2(_B,Yc),true,attach2(_B,Yc),true),
XYc = _C+_D,
XYcc = attach2:attach2(_C,_D),
attach2(X,Y) ? ;
no

我由此得出结论：

copy_term/3会收集attribute_goal/2返回的目标，当遇到多个属性变量时，会移除无意义的true和重复目标。

请问该结论是否本质正确？

回答 #

你的结论本质上是正确的，补充细节后可以更精准地描述其行为：

• 目标收集与合并逻辑：copy_term/3会遍历被复制项中的所有属性变量，调用每个变量的attribute_goal/2生成约束目标。收集过程中会自动过滤等价于true的冗余目标，同时合并语义重复的约束目标——这里的“重复”指语义等价，而非字面完全一致。
• 修改代码后的差异原因：修改attach2/2后，X和Y的属性存储的是同一个att(X,Y)，而非初始版本中各自独立的att(X,Y)和att(Y,X)。复制X+Y时，两个变量对应的attribute_goal/2生成的目标都是attach2(_C,_D)，属于语义重复，因此被合并为一个；而初始版本中生成的attach2(_C,_D)和attach2(_D,_C)语义不等价（除非attach2/2被定义为对称），所以会被保留为两个独立目标。
• true的处理：attribute_goal/2返回序列中的true会被直接忽略，因为它是恒成立的约束，对求解状态无影响，属于无意义冗余。

内容的提问来源于stack exchange，提问作者repeat