Prolog中带cut的分组析取目标与拆分规则的等价性验证

众所周知，以下两条Prolog规则：

fruit(X) :- yellow(X).
fruit(X) :- red(X).

可以通过析取符;简写为：

fruit(X) :- ( yellow(X); red(X) ).

现在来看这条在分组析取目标前引入cut的规则：

test(specific) :- !, ( goal1 ; goal2 ).
test(General) :- goal3.

它的设计意图很明确：只要test(specific)匹配成功，test(General)就不会被执行。

问题：上述规则是否与以下规则等价？ #

test(specific) :- goal1.
test(specific) :- !, goal2.
test(General) :- goal3.

疑问点在于第一种写法里cut在整个析取分组之前，而第二种写法只在goal2前加了cut，这种不对称性让人需要验证对cut作用的理解是否准确。这个问题的背景是为了搞清楚Prolog追踪元解释器中cut的实现逻辑。

等价性结论与分析 #

这两组规则并不等价，核心差异在于cut的触发时机和作用范围：

• 第一组规则中，!在进入test(specific)子句后立即执行：
  只要test(specific)的头部匹配成功，cut就会直接切断所有test/1的后续备选分支（也就是test(General)这条规则），之后才会执行goal1 ; goal2。哪怕goal1和goal2都失败，test(General)也不会被尝试。
• 第二组规则中，!只在第二个test(specific)子句中：
  调用test(specific)时会先尝试第一个子句的goal1：
  1. 如果goal1成功，test(specific)直接成功；若后续因为其他目标失败触发回溯，会继续尝试第二个test(specific)子句，此时才会触发cut，切断test(General)，再执行goal2。
  2. 如果goal1失败，才会进入第二个子句，触发cut后执行goal2；若goal2也失败，整个test(specific)失败，且test(General)不会被尝试。

简单来说，第一组规则里cut的作用是阻止test(General)被执行的同时，也固定了test(specific)只有这一个子句分支；而第二组规则中，test(specific)有两个独立子句，cut只在第二个子句生效，第一个子句成功后仍有回溯到第二个子句的可能，且只有此时才会切断test(General)。

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