为何基于throw(cut)/catch实现的Prolog元解释器cut未生效？

问题描述 #

尝试通过throw(cut)/catch组合在简易Prolog元解释器中实现cut语义，编写了如下代码：

fruit(apple).
fruit(orange) :- !.
fruit(banana).

% meta-interpreter
prove(true) :- !.
prove(!) :- !, ( true ; throw(cut) ).
prove((A,B)):- !, prove(A), prove(B).
prove(H) :- clause(H,B),
    catch(prove(B), cut, fail),
    write(H), write(" <- "), writeln(B).

预期查询prove(fruit(X))仅返回X = apple和X = orange，但实际还返回了X = banana。追踪发现prove(!)从未抛出cut异常。

核心原因 #

prove(!)子句中错误使用了宿主Prolog的cut（!），导致throw(cut)分支永远无法执行：

• 子句prove(!) :- !, ( true ; throw(cut) )中的第一个!是宿主Prolog的原生cut，它会截断该子句内部的所有回溯分支。
• 当调用prove(!)时，true分支先成功，宿主cut直接终止了该子句的后续回溯可能，throw(cut)分支完全被跳过，永远不会触发异常。

这种情况下，处理fruit(orange) :- !.时，prove(!)仅返回成功，不会向外层catch传递任何cut信号；当用户请求下一个解时，元解释器会正常回溯到clause(fruit(X), B)，匹配到fruit(banana)子句，从而返回不符合预期的结果。

修正方案 #

移除prove(!)中的宿主cut，修改为：

prove(!) :- true ; throw(cut).

修正后的逻辑：

1. 首次调用prove(!)时，true分支成功，符合原cut的"执行成功"语义。
2. 当回溯到该prove(!)调用时，会进入throw(cut)分支，抛出异常。
3. 外层catch(prove(B), cut, fail)捕获异常后执行fail，阻止clause(H,B)继续枚举当前谓词的其他子句，完美模拟cut截断后续回溯的效果。

验证：执行prove(fruit(X))时，会依次返回X = apple和X = orange，请求下一个解时无结果返回，符合预期。

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