4

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

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

例如,该语句∀x ∃y (x < y)会导致问题,但没问题∀x (x = 2) ∃y (y < 3)

是否有任何现有的 Haskell 库可以实现这样的值级逻辑量词?很难搜索,因为每当我按照“逻辑量词 Haskell”进行搜索时,我都会得到很多关于类型量词的东西,这不是我想要的。

我唯一能找到的是一个forAllin Test.QuickCheck,这并不带有“存在”。

4

1 回答 1

0

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

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

于 2015-02-23T06:00:26.250 回答