关于Prolog中catch/3作用域内选择点保留的技术问询

背景与测试代码 #

目标代码与元解释器 #

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

% 处理cut的元解释器
prove(true) :- !.
prove(!) :- !, ( true ; throw(cut) ).
prove((A,B)):- !, prove(A), prove(B).
prove(H) :- 
    catch((clause(H,B), prove(B)), cut, fail).

执行结果 #

原生Prolog执行查询：

?- fruit(X).
X = apple
X = orange

使用元解释器执行查询，结果与原生一致：

?- prove(fruit(X)).
X = apple
X = orange

核心疑问 #

针对catch(Goal, ExceptionTag, Handler)的选择点处理逻辑，存在两个核心疑问：

1. Q1：SWI-Prolog文档指出，异常抛出时Goal内的所有选择点会被丢弃，但实测结果与该描述不符。若选择点真的丢失，prove(!)的true分支不会被保留，无法得到X=orange的结果——对catch/3的行为存在哪些误解？
2. Q2：即便选择点被保留，Handler=fail会导致(clause(H,B), prove(B))作用域失败，按道理同样会丢弃Goal内的选择点，显然此处仍有理解偏差。

排查验证 #

为确认选择点行为，修改prove(!)分支添加日志输出：

prove(!) :- writeln("111"), true.
prove(!) :- writeln("222"), throw(cut), writeln("333").

输出结果证实prove(!)中writeln("111"), true的选择点被保留，这与文档描述矛盾。查阅其他Prolog实现的文档，相关表述也较为模糊。

补充：SWI-Prolog的catch/3文档明确说明：

all choice points generated by Goal are cut, the system backtracks to the start of catch/3
（翻译：由Goal生成的所有选择点都会被cut，系统回溯至catch/3的起始位置）

该描述意味着Goal的所有解决方案会被丢弃，仿佛从未执行过，但实测结果并非如此。

疑问解析 #

Q1：选择点丢弃的范围误解 #

文档中提到的“Goal内的选择点被丢弃”，指的是**catch包裹的Goal内部，从catch执行开始到throw抛出异常时，尚未被探索的选择点**，而非已经成功完成的分支的绑定结果。

具体到元解释器的执行流程：

• 当执行prove(fruit(orange))时，会匹配clause(fruit(orange), (!))，接着调用prove(!)。
• prove(!)的第一个子句中，!已经切断了prove(!)自身的其他子句选择点，随后进入(true ; throw(cut))的选择点。
• true分支成功执行后，整个(clause(H,B), prove(B))完成，catch/3的Goal成功，此时不会触发异常，X=orange的绑定结果被保留。
• 只有当用户请求回溯，系统回到(true ; throw(cut))的选择点时，才会执行throw(cut)触发异常，此时catch/3会丢弃Goal内部剩余的未探索选择点（比如clause(H,B)的后续子句），但不会丢弃已经成功的X=orange结果。

Q2：Handler=fail的作用范围误解 #

Handler=fail的作用是让当前触发异常的catch/3调用失败，而非丢弃所有已成功的结果。

执行流程细节：

• 当prove(fruit(orange))通过true分支成功后，prove(fruit(X))返回X=orange的结果。
• 用户请求下一个结果时，系统回溯到prove(fruit(X))的选择点，尝试匹配fruit(banana)的子句，此时执行prove(true)本应成功，但之前fruit(orange)子句中的!触发了throw(cut)，catch/3的failHandler会让当前的prove(fruit(banana))分支失败，最终不会返回X=banana的结果，这与原生Prolog中!切断后续子句的行为完全一致。

简单来说：catch的failHandler仅终止当前异常触发的分支，不会影响已经成功返回的结果；cut的效果正是通过“触发异常→终止后续分支”的逻辑实现的。

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