我在Haskell中使用SBV(带有Z3后端)来创建一些理论证明.我想检查forall 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吗？
ali*_*ias 11
通过使用未经解释的排序和功能,这种推理确实是可能的.然而,需要注意的是,对这种结构的推理通常需要量化的公理,而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.这一切都取决于你使用的求解器,以及要证明的属性有多难.