【发布时间】:2014-10-10 01:15:02
【问题描述】:
我正在为 Python 开发一个抽象代数库,当我意识到很多繁琐的工作只是构造循环以对应带有量词的逻辑表达式。然后我意识到,虽然在 Python 中实现逻辑量化的函数可能很难,但在 Haskell 或其他语言中会更容易。
现在我有量词,只要属性只涉及一个被量化的变量,并且只有当你量化的关系包含三个变量时,克服这些障碍似乎是困难的部分。
例如,∀x ∃y (x < y) 语句会导致问题,但 ∀x (x = 2) ∃y (y < 3) 没问题。
是否有任何现有的 Haskell 库可以实现这样的值级逻辑量词?搜索起来很困难,因为每当我按照“逻辑量词 Haskell”的方式搜索一些东西时,我都会得到很多关于类型量词的东西,这不是我想要的。
我唯一能找到的是Test.QuickCheck 中的forAll,而这并不带有“存在”。
【问题讨论】:
-
有趣。你能补充一点关于你想用这些结构做什么的细节吗?我不清楚你是想证明它们、操纵它们、断言它们、测试它们还是其他什么。
-
你到底想做什么?您想在某个值范围内循环并搜索示例还是检查所有值? (比如 Foldables all and any:hackage.haskell.org/package/base-4.7.0.1/docs/…)?
-
最终它应该产生一个布尔值,并且短期评估将是理想的。它还应该能够链接通用和存在运算符,以便它们像数学一样工作,我不知道
all和any是否像那样工作。所有和任何都使用一元谓词,但我希望能够为all和any指定两个单独的变量,然后将它们链接在一起以生成一个采用二元谓词的函数,并且通常链接 n 个不同的量词产生一个接受 n 元谓词的函数。 -
您要量化的领域是什么?如果您在列表中有您的值,那么
all和any将可以正常工作(也可以嵌套)。 -
我不确定您要寻找什么功能,但如果域(实际上)是有限的,constraintprogramming 库可能适合您的需求。
标签: haskell quantifiers