Teoria symboli dowodzących za pomocą SBV i Haskell

Question

Używam SBV (z backendem Z3) w Haskell, aby utworzyć teorię teorii. Chcę sprawdzić, czy dla wszystkich x i y z podanymi ograniczeniami (jak x + y = y + x, gdzie + jest "operatorem dodatkowym", a nie dodatkiem), niektóre inne warunki są poprawne. Chcę zdefiniować aksjomaty dotyczące wyrażenia + (takie jak asocjatywność, tożsamość itp.), A następnie sprawdzić dalsze równości, np. Sprawdzić, czy a + (b + c) == (a + c) + b jest prawidłowe formalne a, b i .

starałem się wykonać go za pomocą czegoś takiego:

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

Wydaje się jednak, że nie możemy użyć operatora .== na wartościach symbolicznych. Czy jest to brakująca funkcja lub niewłaściwe użycie? Czy jesteśmy w stanie to zrobić w jakiś sposób przy użyciu SBV?

Answer 1

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.

Answer 2

Korzystanie z interfejsu API nie jest poprawne. Najprostszym sposobem udowodnienia matematycznych równości byłoby użycie prostych funkcji. Na przykład, asocjatywność nad nieograniczonych liczb całkowitych można wyrazić w następujący sposób:

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

Jeśli potrzebujesz więcej interfejs programistyczny (a czasem trzeba będzie), a następnie można użyć Symbolic monady, wygląda następująco:

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

Polecam przeglądanie wielu przykładów z witryny hackage, aby zapoznać się z interfejsem API: https://hackage.haskell.org/package/sbv