用SBV和Haskell证明符号理论

Question

我在Haskell中使用SBV (带有Z3后端)来创建一些理论证明。我想检查对于具有给定约束的所有x和y (比如x + y = y + x，其中+是一个“加号运算符”，而不是加法)，其他一些条件是否有效。我想定义关于+表达式的公理(比如结合性、恒等)。然后检查进一步的等式，比如检查a + (b + c) == (a + c) + b是否是有效的形式a、b和c。

我试着用这样的方法来完成它：

main = do
    let x = forall "x"
    let y = forall "y"
    out <- prove $ (x .== x)
    print "end"

但是，我们似乎不能对符号值使用.==运算符。这是缺少的功能还是错误的用法？我们能用SBV做这件事吗？

Answer 1

通过使用未解释的分类和功能，这种推理是可能的。但是，请注意，关于这种结构的推理通常需要量化的公理，而SMT-求解器通常不太擅长用量词进行推理。

话虽如此，我还是这样做的，使用SBV。

首先，使用一些锅炉板代码来获得未解释的T类型。

{-# LANGUAGE DeriveDataTypeable #-}

import Data.Generics
import Data.SBV

-- Uninterpreted type T
data T = TBase () deriving (Eq, Ord, Data, Typeable, Read, Show)
instance SymWord T
instance HasKind T
type ST = SBV T

一旦这样做，您就可以访问未解释的类型T及其符号对应的ST。让我们声明plus和zero，同样地，使用正确类型的未解释常量：

-- Uninterpreted addition
plus :: ST -> ST -> ST
plus = uninterpret "plus"

-- Uninterpreted zero
zero :: ST
zero = uninterpret "zero"

到目前为止，我们告诉SBV存在一个类型T、一个函数plus和一个常量zero；显然没有被解释。也就是说，SMT求解者除了假设它们有给定的类型之外，没有其他的假设。

我们先来证明一下0+x = x

bad = prove $ \x -> zero `plus` x .== x

如果您尝试这样做，您将得到以下响应：

*Main> bad
Falsifiable. Counter-example:
  s0 = T!val!0 :: T

SMT求解程序告诉您的是，该属性不保存，这里有一个不保存的值。值T!val!0是一个特定于Z3的响应；其他求解器可以返回其他内容。它本质上是T类型的居住者的内部标识符；除此之外，我们对它一无所知。当然，这并不是非常有用，因为您并不知道它为plus和zero创建了哪些关联，但这是意料之中的。

为了证明这个属性，让我们再告诉SMT的求解者两件事。首先，plus是可交换的。第二，右边的zero并没有做任何事情。这些都是通过addAxiom调用完成的。不幸的是，您必须用SMTLib语法编写您的公理，因为SBV不支持(至少目前)支持使用Haskell编写的公理。注意，我们在这里切换到使用Symbolic monad：

good = prove $ do
         addAxiom "plus-zero-axioms"
                  [ "(assert (forall ((x T) (y T)) (= (plus x y) (plus y x))))"
                  , "(assert (forall ((x T)) (= (plus x zero) x)))"
                  ]
         x <- free "x"
         return $ zero `plus` x .== x

注意我们是如何告诉求解器x+y = y+x和x+0 = x，并要求它证明0+x = x。以这种方式编写公理看起来很难看，因为您必须使用SMTLib语法，但这就是当前的状况。现在我们有：

*Main> good
Q.E.D.

量化的公理和未解释的类型/函数并不是通过SBV接口使用的最容易的东西，但是这样您可以从中获得一些里程。如果您在公理中大量使用量词，那么求解器不太可能回答您的查询，并且很可能会响应unknown。这一切都取决于你使用的求解者，以及证明这些属性的难度。

Answer 2

您对API的使用并不完全正确。证明数学等式的最简单的方法是使用简单的函数。例如，无界整数上的结合性可以这样表示：

prove $ \x y z -> x + (y + z) .== (x + y) + (z :: SInteger)

如果您需要更多的编程接口(有时也需要)，那么您可以使用Symbolic monad，这样：

plusAssoc = prove $ do x <- sInteger "x"
                       y <- sInteger "y"
                       z <- sInteger "z"
                       return $ x + (y + z) .== (x + y) + z

我建议浏览hackage站点中提供的许多示例，以熟悉API：https://hackage.haskell.org/package/sbv