Tego rodzaju rozumowanie jest rzeczywiście możliwe dzięki zastosowaniu nieinterpretowanych rodzajów i funkcji. Ostrzegamy jednak, że rozumowanie dotyczące takich struktur zwykle wymaga kwantyfikacji aksjomatów, a rozwiązania do rozwiązywania SMT zwykle nie są zbyt dobre w rozumowaniu za pomocą kwantyfikatorów.
Powiedziawszy to, oto, jak to zrobić, używając SBV.
Po pierwsze, niektóre kod kotła płyta uzyskać zinterpretowane typ 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
Gdy to zrobisz, będziesz miał dostęp do zinterpretowane typu T
i jej symbolicznym odpowiednikiem ST
. Załóżmy zadeklarować plus
i zero
, znowu tylko zinterpretowane stałe z odpowiednich typów:
-- Uninterpreted addition
plus :: ST -> ST -> ST
plus = uninterpret "plus"
-- Uninterpreted zero
zero :: ST
zero = uninterpret "zero"
Jak dotąd, wszystko powiedzieliśmy SBV jest to, że istnieje rodzaj T
oraz funkcję plus
i stałą zero
; wyraźnie niezinterpretowane. Oznacza to, że solver SMT nie przyjmuje żadnych założeń poza faktem, że mają one podane typy.
Niech najpierw starają się udowodnić, że 0+x = x
:
bad = prove $ \x -> zero `plus` x .== x
Jeśli spróbujesz tego otrzymasz następującą odpowiedź:
*Main> bad
Falsifiable. Counter-example:
s0 = T!val!0 :: T
Co solver SMT jest informacją jest to, że nieruchomości nie trzyma się, a tutaj jest wartość, której nie ma.Wartość T!val!0
jest specyficzną odpowiedzią; inni twórcy mogą zwracać inne rzeczy. Zasadniczo jest to wewnętrzny identyfikator mieszkańca typu T
; i poza tym nic o tym nie wiemy. Nie jest to oczywiście zbyt użyteczne, ponieważ nie wiesz, jakie skojarzenia tworzyły dla plus
i zero
, ale można się tego spodziewać.
Aby dowieść własności, powiedzmy rozwiązaniu SMT jeszcze dwie rzeczy. Po pierwsze, że plus
jest przemienny. Po drugie, dodany po prawej stronie zero
nic nie robi. Są one wykonywane za pośrednictwem wywołań addAxiom
. Niestety, musisz zapisać swoje aksjomaty w składni SMTLib, ponieważ SBV nie obsługuje (przynajmniej jeszcze) obsługi aksjomatów napisanych przy użyciu Haskella. Należy również zauważyć możemy przełączyć się za pomocą Symbolic
monady tutaj:
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
uwaga jak powiedzieliśmy solver x+y = y+x
i x+0 = x
, i poprosił go, aby udowodnić 0+x = x
. Pisanie aksjomatów w ten sposób wygląda naprawdę paskudnie, ponieważ musisz używać składni SMTLib, ale to jest obecny stan rzeczy. Teraz mamy:
*Main> good
Q.E.D.
Skwantyfikowane aksjomaty i zinterpretowane-typy/funkcje nie są najłatwiejsze rzeczy do używania przez interfejs SBV, ale można dostać jakiś przebieg z nim w ten sposób. Jeśli masz duże ilości kwantyfikatorów w swoich aksjomatach, jest mało prawdopodobne, że solver będzie w stanie odpowiedzieć na twoje pytania; i prawdopodobnie odpowiedzieć unknown
. Wszystko zależy od tego, z jakiego solver korzystasz i jak trudne są właściwości do udowodnienia.
Twoja linia 'prove' jest równoważna' prove (forall "x". == forall "x") '. Nigdy nie korzystałem z SBV, ale wygląda mi to źle. – chi
Masz rację. W każdym razie nie mogłem go skompilować, ponieważ nie możemy użyć '. ==' na symbolice (bez formalnego "x" powinno być także wartością symboliczną) –