如何消除Unification库中的统一循环解？

我使用unification库时遇到了不符合预期的循环解，示例代码如下：

from unification import *

x1 = var('x1')

unify((x1, 1), x1) # 返回 {~x1: (~x1, 1)}

这种自引用的循环解不符合需求，我希望unify返回False——因为代入后((x1, 1), 1)不等于(x1, 1)。

另一个需要拒绝的循环解示例：

{~x1: (~s1_1, (~s1_2, ~s1_3)),
 ~x2: (~s1_1, ~s1_2),
 ~x3: (~s1_1, ~s1_3),
 ~s1_1: ~i1,
 ~i1: (~x3, ~s1_3),
 ~i2: (~s1_2, ~s1_3),
 ~s1_2: (~x3, ~s1_3)}

它的循环引用链是：~x3: (~s1_1, ~s1_3) -> ~x3: (~i1, ~s1_3) -> ~x3: ((~x3, ~s1_3), ~s1_3)。

如果库本身无法实现这种约束，请提供检测此类循环引用的算法。

1. 库内置功能限制 #

unification库默认允许递归（循环）合一解，目前没有内置配置直接禁用该行为。要实现需求，需在合一结果返回后手动检测并过滤循环引用的情况。

2. 循环引用检测算法 #

核心逻辑是追踪每个变量的绑定展开链，若链中再次出现当前变量，则判定为循环引用。

算法步骤 #

• 遍历替换字典中的每个变量及其绑定值
• 对每个变量维护一个已访问集合，记录当前追踪路径上的变量
• 递归展开绑定值：
  1. 若当前值是变量：
     • 若该变量在已访问集合中，说明存在循环，返回True
     • 否则将其加入集合，继续展开它的绑定值
  2. 若当前值是复合结构（如元组、列表），遍历每个元素并递归检查
• 所有变量展开路径无循环则合法，否则判定为循环引用

代码实现 #

from unification import var

def has_cyclic_reference(substitution):
    def check(current_var, visited):
        # 当前变量没有绑定值，无循环
        if current_var not in substitution:
            return False
        bound_value = substitution[current_var]
        
        # 绑定值是变量，继续追踪
        if isinstance(bound_value, var):
            if bound_value in visited:
                return True
            # 递归检查，更新已访问集合
            return check(bound_value, visited | {bound_value})
        
        # 绑定值是复合结构，遍历每个元素检查
        elif isinstance(bound_value, (tuple, list)):
            for elem in bound_value:
                if isinstance(elem, var):
                    if check(elem, visited | {current_var}):
                        return True
        return False

    # 检查每个变量的绑定链
    for var_key in substitution:
        if check(var_key, {var_key}):
            return True
    return False

# 测试示例
sub1 = {var('x1'): (var('x1'), 1)}
print(has_cyclic_reference(sub1))  # 输出 True，存在循环

sub2 = {var('x1'): var('x2'), var('x2'): var('x3'), var('x3'): 1}
print(has_cyclic_reference(sub2))  # 输出 False，无循环

使用方式 #

调用unify后，若返回替换字典，用上述函数检测：

result = unify((x1, 1), x1)
if result is not False and has_cyclic_reference(result):
    # 存在循环引用，视为合一失败
    final_result = False
else:
    final_result = result

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