【问题标题】:Are there any value-level logical quantifers in Haskell?Haskell 中是否有任何价值级别的逻辑量词?
【发布时间】: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/…)?
  • 最终它应该产生一个布尔值,并且短期评估将是理想的。它还应该能够链接通用和存在运算符,以便它们像数学一样工作,我不知道allany 是否像那样工作。所有和任何都使用一元谓词,但我希望能够为 allany 指定两个单独的变量,然后将它们链接在一起以生成一个采用二元谓词的函数,并且通常链接 n 个不同的量词产生一个接受 n 元谓词的函数。
  • 您要量化的领域是什么?如果您在列表中有您的值,那么 allany 将可以正常工作(也可以嵌套)。
  • 我不确定您要寻找什么功能,但如果域(实际上)是有限的,constraintprogramming 库可能适合您的需求。

标签: haskell quantifiers


【解决方案1】:

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

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

【讨论】:

    猜你喜欢
    • 1970-01-01
    • 1970-01-01
    • 2010-10-25
    • 1970-01-01
    • 1970-01-01
    • 2016-10-09
    • 1970-01-01
    • 2018-04-23
    • 2021-12-17
    相关资源
    最近更新 更多