存在的搜索和查询没有大惊小怪

Question

有没有一种可扩展的、有效的方法来在 Haskell 中编写存在性语句而无需实现嵌入式逻辑编程语言？通常，当我在实现算法时，我想表达存在量化的一阶陈述，例如

∃x.∃y.x,y ∈ xs ∧ x ≠ y ∧ p x y

∈ 在列表中被重载。如果我赶时间，我可能会写出看起来像这样的明显代码

find p []     = False
find p (x:xs) = any (\y -> x /= y && (p x y || p y x)) xs || find p xs

或

find p xs = or [ x /= y && (p x y || p y x) | x <- xs, y <- xs]

但是这种方法不能很好地推广到返回值或谓词或多个参数的函数的查询。例如，即使是像

这样的简单语句

∃x.∃y.x,y,z ∈ xs ∧ x ≠ y ≠ z ∧ f x y z = g x y z

需要编写另一个搜索过程。这意味着大量的样板代码。当然，像 Curry 或 Prolog 这样实现缩小或解析引擎的语言允许程序员编写如下语句：

find(p,xs,z) = x ∈ xs & y ∈ xs & x =/= y & f x y =:= g x y =:= z

大量滥用该表示法，它执行搜索并返回一个值。这个问题在实现正式指定的算法时经常出现，通常通过fmap、foldr和mapAccum等函数的组合来解决，但主要是显式递归。有没有更通用、更高效，或者只是通用和表达性更强的方法来用 Haskell 编写这样的代码？

Answer 1

有一个标准的转换可以让你转换

∃x ∈ xs : P

到

exists (\x -> P) xs

如果您需要出示见证人，您可以使用find 而不是exists。

与逻辑语言相比，在 Haskell 中进行这种抽象的真正麻烦在于，您确实必须将“宇宙”集 xs 作为参数传递。我相信这就是你在标题中提到的“大惊小怪”的原因。

当然，如果您愿意，您可以将通用集（您正在搜索的）填充到一个 monad 中。然后，您可以定义自己的 exists 或 find 版本来处理单子状态。为了提高效率，您可以尝试Control.Monad.Logic，但它可能会导致您对 Oleg 的论文感到头疼。

无论如何，经典编码是将所有绑定构造（包括存在量词和通用量词）替换为 lambda，并继续进行适当的函数调用。我的经验是，这种编码甚至适用于具有大量结构的复杂嵌套查询，但总感觉很笨重。

Answer 2

也许我不明白，但列表推导有什么问题？您的第二个示例变为：

[(x,y,z) | x <- xs, y <- xs, z <- xs
, x /= y && y /= z && x /= z 
, (p1 x y z) == (p2 x y z)]

这允许您返回值；要检查公式是否满足，只需使用null（由于懒惰，它不会评估超出需要的值）。