SLD解析树问题：求解swap([1,2], U)的谓词选择及合一过程

嘿，我来帮你一步步理清这个问题，把你困惑的合一过程、谓词选择和最终推导都讲明白～

首先先明确你提到的3条swap规则（这类问题的标准定义，我先列出来方便后续讲解）：

% 规则1：空列表的交换结果为空列表
swap([], []).
% 规则2：单元素列表交换后还是自身
swap([X], [X]).
% 规则3：交换前两个元素，递归处理剩余列表
swap([H,S|T], [S,H|U]) :- swap(T, U).

1. 首次选择的谓词：确实是第三条规则 #

当你查询swap([1,2], U)时，Prolog会按顺序尝试匹配每条规则：

• 规则1的第一个参数是空列表，和[1,2]完全不匹配，跳过；
• 规则2的第一个参数是单元素列表，[1,2]是双元素，不匹配，跳过；
• 规则3的第一个参数是[H,S|T]（表示至少有两个元素的列表，前两个是H、S，剩余部分是T），刚好能和[1,2]合一，所以首次匹配的就是第三条规则。

2. 详细的合一过程 #

我们把查询和规则3的头进行合一，这里要注意区分变量名（避免查询的U和规则里的U混淆，我把规则里的变量改成U_rule）：

• 规则3的头：swap([H,S|T], [S,H|U_rule])
• 查询：swap([1,2], U_query)

合一步骤：

1. 第一个参数合一：[H,S|T] = [1,2]
   • 列表[1,2]可以拆分为前两个元素1、2，剩余部分是空列表[]，所以得到：H=1，S=2，T=[]。
2. 第二个参数合一：[S,H|U_rule] = U_query
   • 代入H和S的值，得到：U_query = [2,1|U_rule]。

此时，查询的目标转化为规则3的体：swap(T, U_rule)，也就是swap([], U_rule)。

3. 递归推导得到最终结果 #

现在处理递归目标swap([], U_rule)：

• 这个目标会匹配规则1：swap([], [])，所以合一得到U_rule = []。
• 把U_rule = []回代到之前的U_query = [2,1|U_rule]，就得到：U_query = [2,1|[]] = [2,1]。

你之前疑惑的U = [2,1|U]其实是变量名混淆导致的——这里的两个U不是同一个变量！规则里的U是递归目标的变量，而查询的U是最终要绑定的变量，当递归到空列表时，规则1给递归变量绑定了空列表，回代后就得到了最终的确定值[2,1]。

简单的SLD树示意 #

• 根节点：swap([1,2], U)
  • 子节点（匹配规则3）：swap([], U_rule)
    • 子节点（匹配规则1）：成功，U_rule=[] → 回代得U=[2,1]

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