haskell - 使用 SBV 和 Haskell 证明符号理论

Question

我正在使用 SBV (使用 Z3 后端)在 Haskell 中创建一些理论证明。我想检查一下是否为 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具体 react ；其他求解器可以返回其他东西。它本质上是 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 接口(interface)使用的最简单的东西，但您可以通过这种方式获得一些好处。如果您在公理中大量使用量词，则求解器不太可能回答您的查询；并且可能会回复 unknown .这完全取决于您使用的求解器，以及要证明的属性有多难。