如何在Python中实现带回溯的Prolog合一算法？开发遇困求助

嘿，我完全懂你查了一堆资料反而越看越懵的感觉——合一算法的示例要么太简化要么太学术，确实容易绕晕。咱们一步步拆解，从核心逻辑到落地实现，把它捋得明明白白。

简单说，合一就是找到一个置换（Substitution）——本质是变量到表达式的映射——让两个输入的逻辑表达式（比如谓词项、原子公式）变得完全一致。如果找不到这样的置换，就返回失败。

这些是合一的底层逻辑，别搞混：

• 如果两个表达式是相同的常量：直接成功，置换为空（不需要替换任何东西）。
• 如果其中一个是变量：
  • 先检查这个变量有没有已经被置换过，要是有，就用置换后的值继续匹配；
  • 如果变量和另一个表达式完全相同（比如X和X），直接成功；
  • 要是另一个表达式里包含这个变量（比如X和f(X)），这会导致无限循环（置换后X变成f(X)，再替换又会变成f(f(X))...），必须返回失败——这一步叫发生检查，是很多新手容易漏掉的关键点；
  • 其他情况，把这个变量映射到另一个表达式，加入置换集合。
• 如果两个都是复合项（比如f(a,X)和f(Y,b)）：
  • 先检查函数/谓词的名字、参数数量是否一致，不一致直接失败；
  • 然后递归地合一每一对对应的参数，把所有得到的置换合并起来。
• 剩下的情况（比如常量和复合项、不同函数名的复合项）：合一失败。

把上面的规则转化成可落地的逻辑，伪代码如下：

# 主合一函数，substitution是当前已有的置换集合（初始为空字典）
function unify(expr1, expr2, substitution):
    # 第一步：先把现有置换应用到两个表达式上，确保处理的是最新状态
    expr1 = apply_substitution(expr1, substitution)
    expr2 = apply_substitution(expr2, substitution)

    # 情况1：两个表达式完全相同
    if expr1 == expr2:
        return substitution
    # 情况2：第一个是变量
    elif is_variable(expr1):
        # 发生检查：变量不能出现在目标表达式里
        if occurs_check(expr1, expr2):
            return failure
        # 把变量映射到表达式，加入置换
        substitution[expr1] = expr2
        return substitution
    # 情况3：第二个是变量（和情况2对称）
    elif is_variable(expr2):
        if occurs_check(expr2, expr1):
            return failure
        substitution[expr2] = expr1
        return substitution
    # 情况4：都是复合项
    elif is_compound(expr1) and is_compound(expr2):
        # 函数名或参数数量不一致，直接失败
        if expr1.name != expr2.name or len(expr1.args) != len(expr2.args):
            return failure
        # 递归合一每个参数
        for arg1, arg2 in zip(expr1.args, expr2.args):
            substitution = unify(arg1, arg2, substitution)
            # 只要有一个参数合一失败，整体失败
            if substitution is failure:
                return failure
        return substitution
    # 情况5：不匹配的常量或其他情况
    else:
        return failure

# 辅助函数：把置换应用到表达式上
function apply_substitution(expr, substitution):
    if is_variable(expr):
        # 如果变量在置换里，返回替换后的值，否则返回原变量
        return substitution.get(expr, expr)
    elif is_compound(expr):
        # 递归替换复合项的每个参数
        new_args = [apply_substitution(arg, substitution) for arg in expr.args]
        return Compound(expr.name, new_args)
    else:
        # 常量直接返回
        return expr

# 辅助函数：检查变量是否出现在表达式中（发生检查）
function occurs_check(var, expr):
    if var == expr:
        return True
    elif is_compound(expr):
        # 只要有一个参数包含变量，就返回True
        return any(occurs_check(var, arg) for arg in expr.args)
    else:
        # 常量不包含变量，返回False
        return False

• 漏掉发生检查：这是最常见的错误，会导致无限递归或无效置换（比如X → f(X)），一定要记得加；
• 没先应用现有置换：比如已经有X → Y的置换，现在合一X和a，得先把X替换成Y，再合一Y和a，不能直接用原始的X处理；
• 复合项匹配不严谨：必须先校验函数名和参数数量，比如f(a)和g(a)、f(a,b)和f(a)都不可能合一；
• 置换合并错误：递归处理参数时，要把每一步得到的置换累积起来，不能覆盖之前的结果。

比如我们要合一f(X, g(Y))和f(a, g(Z))：

1. 两个都是复合项，函数名都是f，参数数量都是2，进入递归；
2. 合一第一个参数X和a：X是变量，无发生检查问题，置换变成{X: a}；
3. 合一第二个参数g(Y)和g(Z)：都是复合项，函数名g，参数数量1，继续递归；
4. 合一Y和Z：Y是变量，无发生检查，置换更新为{X: a, Y: Z}；
5. 所有参数都合一成功，最终置换就是这个集合，应用后两个表达式都变成f(a, g(Z))，合一成功。

再试一个失败的例子：合一X和f(X)，发生检查会发现X出现在f(X)中，直接返回失败，避免了无限循环。

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