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

问题描述

我想用符号表达式 (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]

如何解决这个问题？

解决方法

无论是您的 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 的电话号码是多少？嗯，这个想法是假设所有列表的长度都有某种上限，Data.SBV.Tools.BoundedList 导出一堆方法来轻松处理它们；都采用绑定参数。只要输入最多是这个长度，它们就会正常工作。如果您的列表长于给定的界限，则无法保证会发生什么。（一般来说，它会在一定范围内砍掉你的列表，但你不应该依赖这种行为。）

https://hackage.haskell.org/package/sbv-8.12/docs/Documentation-SBV-Examples-Lists-BoundedMutex.html

中有一个与 BMC（有界模型检查）协调使用此类列表的经过验证的示例

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

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

这是它的样子：

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

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

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

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

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

您可以将 f 重写为

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

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

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

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

haskell haskell sbv