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

Posted 2023-05-08

【中文标题】存在的搜索和查询没有大惊小怪

【英文标题】：existential search and query without the fuss

【发布时间】：2011-12-10 10:50:32

【问题描述】：

有没有一种可扩展的、有效的方法来在 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 编写这样的代码？

【问题讨论】：

我怀疑hackage.haskell.org/package/logict 是你要找的。​​span>

【参考方案1】：

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

∃x ∈ xs : P

到

exists (\x -> P) xs

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

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

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

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

【讨论】：

是的，我认为 LogicT monad 是我正在寻找的。感谢您的回复。我对你提到的表示很熟悉，也觉得很麻烦。

【参考方案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（由于懒惰，它不会评估超出需要的值）。

【讨论】：

这个实现的问题是如果p1 x y z == p2 x y z 当x == xs !! 1 和xs 是无限的find 将永远不会终止。这就是为什么LogicT 实现msplit 和“公平分离”interleave