12

我在 Haskell 中使用SBV（带有 Z3 后端）来创建一些理论证明。我想检查 forallx和y给定的约束（例如x + y = y + x，+“加号运算符”在哪里，而不是加法）其他一些术语是否有效。我想定义关于+表达式的公理（如关联性、身份等），然后检查进一步的等式，如检查是否是a + (b + c) == (a + c) + b有效的形式a和.bc

我试图使用类似的东西来完成它：

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

但似乎我们不能.==在符号值上使用运算符。这是缺少的功能还是错误的用法？我们能以某种方式使用 SBV 做到这一点吗？

4

2 回答 2

12

通过使用未解释的排序和函数，这种推理确实是可能的。但是请注意，对此类结构的推理通常需要量化的公理，而 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。让我们声明plusand 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 编写的公理。还要注意我们在这里切换到使用Symbolicmonad：

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。这完全取决于您使用的求解器，以及要证明的属性有多难。

于 2015-07-08T23:40:48.340 回答
4

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

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

如果您需要一个更加程序化的界面（有时您会这样做），那么您可以使用Symbolicmonad，因此：

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

于 2015-07-08T17:25:37.567 回答