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

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 版本来处理 monadic 状态。为了提高效率，您可以尝试Control.Monad.Logic ，但这可能会让您对 Oleg 的论文感到头疼。

无论如何，经典编码是用 lambda 替换所有绑定(bind)结构，包括存在量词和通用量词，然后进行适当的函数调用。我的经验是，这种编码甚至适用于具有很多结构的复杂嵌套查询，但它总是让人觉得笨拙。