使用 Haskell 和 SBV 进行列表理解的条件

Question

我想编写一个带有符号表达式 (SBV) 条件的 Haskell 列表推导式。我用下面的小例子重现了这个问题。

import Data.SBV

allUs :: [SInteger] 
allUs = [0,1,2]  

f :: SInteger -> SBool 
f 0 = sTrue
f 1 = sFalse
f 2 = sTrue

someUs :: [SInteger] 
someUs = [u | u <- allUs, f u == sTrue]

使用show someUs，会出现以下错误

*** Data.SBV: Comparing symbolic values using Haskell's Eq class!
***
*** Received:    0 :: SInteger  == 0 :: SInteger
*** Instead use: 0 :: SInteger .== 0 :: SInteger
***
*** The Eq instance for symbolic values are necessiated only because
*** of the Bits class requirement. You must use symbolic equality
*** operators instead. (And complain to Haskell folks that they
*** remove the 'Eq' superclass from 'Bits'!.)

CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/Symbolic.hs:1009:23 in sbv-8.8.5-IR852OLMhURGkbvysaJG5x:Data.SBV.Core.Symbolic

将条件更改为f u .== sTrue 也会报错

<interactive>:8:27: error:
    • Couldn't match type ‘SBV Bool’ with ‘Bool’
      Expected type: Bool
        Actual type: SBool
    • In the expression: f u .== sTrue
      In a stmt of a list comprehension: f u .== sTrue
      In the expression: [u | u <- allUs, f u .== sTrue]

如何解决这个问题？

Answer 1

您的f 和someUs 都不能按书面形式进行符号计算。理想情况下，这些应该是类型错误，被立即拒绝。这是因为符号值不能是Eq 类的实例：为什么？因为确定符号值的相等性需要调用底层求解器；所以结果不能是Bool；它真的应该是SBool。但是 Haskell 不允许在模式匹配中使用广义保护来允许这种可能性。 （这也是有充分理由的，所以这并不是 Haskell 的错。只是这两种编程风格不能很好地结合在一起。）

您可以问为什么 SBV 将符号值作为 Eq 类的实例。它是Eq 实例的唯一原因是错误消息告诉您：因为我们希望它们成为Bits 类的实例；其中有Eq 作为超类要求。但那完全是另一回事了。

基于此，如何在 SBV 中编写函数？以下是您如何以符号样式编写 f：

f :: SInteger -> SBool
f i = ite (i .== 0) sTrue
    $ ite (i .== 1) sFalse
    $ ite (i .== 2) sTrue
    $               sFalse   -- arbitrarily filled to make the function total

很难看，但这是唯一的写法，除非你想玩一些准引用的把戏。

关于someUs：这也不是你可以直接象征性地写的东西：这被称为脊椎混凝土列表。如果不对单个元素实际运行求解器，SBV 就无法知道结果列表的长度。一般来说，您不能在带有符号元素的脊椎混凝土列表上执行 filter 之类的函数。

解决方案是使用所谓的符号列表和有界列表抽象。这不是很令人满意，但您可以尽最大努力避免终止问题：

{-# LANGUAGE OverloadedLists #-}

import Data.SBV
import Data.SBV.List
import Data.SBV.Tools.BoundedList

f :: SInteger -> SBool
f i = ite (i .== 0) sTrue
    $ ite (i .== 1) sFalse
    $ ite (i .== 2) sTrue
    $               sFalse   -- arbitrarily filled to make the function total

allUs :: SList Integer
allUs = [0,1,2]

someUs :: SList Integer
someUs = bfilter 10 f allUs

当我运行它时，我得到：

*Main> someUs
[0,2] :: [SInteger]

但你会问10 拨打bfilter 时的那个号码是什么？好吧，这个想法是假设所有列表的长度都有某种上限，Data.SBV.Tools.BoundedList 导出了一堆方法来轻松处理它们；都采用绑定参数。只要输入最多这个长度，它们就可以正常工作。如果您的列表长于给定的范围，则无法保证会发生什么。 （一般来说，它会在绑定时切断你的列表，但你不应该依赖这种行为。）

https://hackage.haskell.org/package/sbv-8.12/docs/Documentation-SBV-Examples-Lists-BoundedMutex.html 有一个与 BMC（有界模型检查）协调使用此类列表的示例

总而言之，由于 Haskell 中的限制（Bool 是固定类型而不是类）和底层求解器的限制，在符号上下文中处理列表会带来一些建模成本以及您可以做多少，它不能很好地处理递归定义的函数。后者主要是因为这样的证明需要归纳，而 SMT 求解器不能开箱即用地进行归纳。但是，如果您使用类似 BMC 的想法遵循游戏规则，您可以在合理范围内处理问题的实际实例。

Answer 2

(.==) 接受两个EqSymbolic 实例，返回一个SBool。在列表推导中，条件是使用 guard 函数实现的。

它是这样的：

guard :: Alternative f => Bool -> f ()
guard False = empty
guard True = pure ()

对于列表，empty 是 []，pure () 返回一个单例列表 [()]。计算结果为 False 的列表中的任何成员都将返回一个空列表而不是一个单元项，将其排除在链下的计算之外。

[True, False, True] >>= guard
= concatMap guard [True, False, True]
= concat $ map guard [True, False, True]
= concat $ [[()], [], [()]]
= [(), ()]

当上下文被展平时，第二个分支被排除，因此它从计算中“修剪”。

您在这里似乎有两个问题 - 当您在 f 中进行模式匹配时，您正在使用 Eq 类进行比较。这就是 SBV 错误的来源。由于您的值非常接近，您可以使用select，它采用项目列表、默认值、计算结果为索引的表达式，并尝试从该列表中获取indexth 项目。

您可以将f 重写为

f :: SInteger -> SBool
f = select [sTrue, sFalse, sTrue] sFalse

第二个问题是守卫显式查找Bool，但(.==) 仍然返回SBool。查看Data.SBV，您应该能够使用unliteral 将其强制转换为常规Bool，它会尝试将SBV 值解包为等效的Haskell 值。

fromSBool :: SBool -> Bool
fromSBool = fromMaybe False . unliteral

someUs :: [SInteger]
someUs = [u | u <- allUs, fromSBool (f u)]
-- [0 :: SInteger, 2 :: SInteger]