什么类型的系统可以防止逻辑语言中的目标暂停？

Question

从咖喱教程的 3.13.3节:

---

剩余的操作称为刚性操作,而缩小的操作称为灵活操作.所有已定义的操作都是灵活的,而大多数基本操作(如算术运算)都是严格的,因为猜测对它们来说不是一个合理的选择.例如,prelude定义了一个列表连接操作,如下所示:

infixr 5 ++
...
(++)             :: [a] -> [a] -> [a]
[]       ++ ys   = ys
(x:xs) ++ ys     = x : xs ++ ys

由于操作"++"是灵活的,我们可以使用它来搜索满足特定属性的列表:

Prelude> x ++ [3,4] =:= [1,2,3,4]       where x free
Free variables in goal: x
Result: success
Bindings:
x=[1,2] ?

另一方面,诸如加"+"之类的预定义算术运算是刚性的.因此,使用逻辑变量作为参数的"+"调用flounders:

Prelude> x + 2 =:= 4 where x free
Free variables in goal: x
*** Goal suspended!

---

库里似乎没有防止写入将被暂停的目标.什么类型的系统可以提前检测到目标是否会被暂停？

Answer 1

您所描述的听起来像是模式检查，它通常检查哪些输出可用于特定的输入集。您可能需要检查 Mercury 语言，它非常重视模式检查。