haskell - Haskell 中是否有任何值(value)级别的逻辑量词？

Question

我正在为 Python 开发一个抽象代数库，当我意识到很多肮脏的工作只是构造循环以对应于带有量词的逻辑表达式时。然后我意识到，虽然在 Python 中实现逻辑量化的函数可能很困难，但在 Haskell 或其他语言中会更容易。

现在我有量词，只要属性只涉及一个被量化的变量，并且只有当你量化的关系有三个变量时，克服这些障碍似乎是困难的部分。

例如，语句 ∀x ∃y (x < y)导致问题，但 ∀x (x = 2) ∃y (y < 3)很好。

是否有任何现有的 Haskell 库可以实现这样的值级逻辑量词？搜索起来很困难，因为每当我按照“逻辑量词 Haskell”的方式搜索一些东西时，我都会得到很多关于类型量词的东西，这不是我想要的。

我唯一能找到的是 forAll在 Test.QuickCheck ，而这并不带有“存在”。

Answer 1

您可以使用 SMT 编写此类表达式并生成反例。求解器。 Haskell 与 smt 求解器(例如 https://hackage.haskell.org/package/sbv)有很好的自然绑定(bind)，让您可以编写正常外观的表达式并在这个特殊规则下评估它们。

这是获得所需内容的一种好方法。