使用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]

但您会问调用bfilter时的数字10是什么？这个想法是，假设所有列表的长度都有某种上限，并且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，它将获取一个项目列表、一个默认值、一个计算结果为索引的表达式，并尝试从该列表中获取第index个项目。

您可以将f重写为

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

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

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

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