单面统一可以改善错误处理吗？

Posted 2023-05-08

【中文标题】单面统一可以改善错误处理吗？

【英文标题】：Can single sided unification improve error handling?

【发布时间】：2021-05-20 22:14:49

【问题描述】：

受question 的启发，我正在努力强化错误 处理反向/2。所以我尝试了这个实现：

reverse(X, Y) :- reverse(X, [], Y).

reverse(X, _, _) :- var(X), throw(error(instantiation_error,_)).
reverse([], X, R) :- !, R = X.
reverse([X|Y], Z, R) :- !, reverse(Y, [X|Z], R).
reverse(X, _, _) :- throw(error(type_error(list,X),_)).

一切正常，直到我尝试将 reverse/2 作为生成器：

?- reverse([1,2,3],X).
X = [3, 2, 1].

?- reverse(2,X).
ERROR: Type error: `list' expected, found `2' (an integer)

?- reverse(X,Y).
ERROR: Arguments are not sufficiently instantiated

单面统一可以改变这种情况，一些基于单面统一的典型解决方案，以便生成器reverse(X,Y) 仍然可以工作吗？ SWI-Prolog 8.3.19 中提供单面统一。

【参考方案1】：

恐怕我无法提出单面统一的解决方案。而是(\=)/2 形式的正常统一可能有用。我几乎不使用(\=)/2。该解决方案的灵感来自 Dijkstra 守卫 if-fi，本文末尾的论文链接：

if
Cond1 -> ActionList1
..
Condn -> ActionList2
fi

如果条件 Cond1,..,Condn 都不满足，则 if-fi 中止。所以我们 只需使用条件否定的连词即可：

reverse(X, Y) :- reverse(X, [], Y).

reverse(X, _, _) :- X \= [], X \= [_|_], throw(error(type_error(list,X),_)).
reverse([], X, R) :- R = X.
reverse([X|Y], Z, R) :- reverse(Y, [X|Z], R). 

似乎有效：

?- reverse([1,2,3],X).
X = [3, 2, 1].

?- reverse(2,X).
ERROR: Type error: `list' expected, found `2' (an integer)

?- reverse(X,Y).
X = Y, Y = [] ;
X = Y, Y = [_1778] ;
X = [_1778, _2648],
Y = [_2648, _1778] ;
Etc..

所以单边统一可能是错误的做法？我不知道。上述解决方案会产生开销，除非某些索引可能会优化掉(\=)/2。甚至可以与属性变量一起使用。

程序的不确定性和形式派生 Edsger W. Dijkstra - Burroughs Corporationhttp://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.90.97&rep=rep1&type=pdf

【参考方案2】：

这似乎有效（在 library(lists) 中使用 reverse/2 的 => 的简单翻译）：

reverse(List, Reversed) =>
    reverse(List, [], Reversed, Reversed).

reverse([], Ys, Reversed, Tail) =>
    Reversed = Ys,
    Tail = [].
reverse([X|Xs], Rs, Reversed, Tail) =>
    Tail = [_|Bound],
    reverse(Xs, [X|Rs], Reversed, Bound).

【讨论】：

查看我的问题，它说“生成器反向（X，Y）仍然可以工作吗？”在我这边不起作用。仍然给出 ?- reverse(X,Y)。错误：没有规则匹配 reverse(_2624,[],_2628,_2628)。