Testimonianza della teoria simbolica tramite SBV e Haskell

Question

Sto usando SBV (con backend Z3) in Haskell per creare alcuni dimostratori di teoria. Voglio verificare se forall x e con determinati vincoli (come x + y = y + x, dove + è un "operatore più", non aggiunta) altri termini sono validi. Voglio definire gli assiomi sull'espressione + (come associatività, identità ecc.) E quindi controllare ulteriori uguaglianze, come controllare se a + (b + c) == (a + c) + b è valido formale a, b e c.

stavo cercando di realizzarlo utilizzando qualcosa di simile:

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

Ma sembra che non possiamo usare l'operatore .== sui valori simbolici. Questa è una caratteristica mancante o un uso errato? Siamo in grado di farlo in qualche modo usando SBV?

Answer 1

Questo tipo di ragionamento è infatti possibile, attraverso l'utilizzo di tipi e funzioni non interpretati. Si avverta, tuttavia, che ragionare su tali strutture richiede in genere assiomi quantificati e che i solutori di SMT di solito non sono molto bravi a ragionare con i quantificatori.

Detto questo, ecco come farei, usando SBV.

In primo luogo, del codice della caldaia-piastra per ottenere un tipo non interpretato 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 

Una volta fatto questo, avrete accesso a un tipo non interpretato T e la sua controparte simbolica ST. Facciamo dichiarare plus e zero, ancora una volta le costanti solo non interpretati con i tipi giusti:

-- Uninterpreted addition 
plus :: ST -> ST -> ST 
plus = uninterpret "plus" 

-- Uninterpreted zero 
zero :: ST 
zero = uninterpret "zero" 

Finora, tutti abbiamo detto SBV è che esiste un tipo T, e una funzione plus, e una costante zero; essere espressamente non interpretato. Cioè, il solutore SMT non fa supposizioni se non il fatto che hanno i tipi dati.

si deve prima cercare di dimostrare che 0+x = x:

bad = prove $ \x -> zero `plus` x .== x 

Se si tenta questo, si otterrà la seguente risposta:

*Main> bad 
Falsifiable. Counter-example: 
    s0 = T!val!0 :: T 

Quello che il solutore SMT sta dicendo è che la proprietà non regge, ed ecco un valore dove non regge.Il valore T!val!0 è una risposta specifica Z3; altri solutori possono restituire altre cose. È essenzialmente un identificatore interno per un abitante del tipo T; e a parte questo non ne sappiamo nulla. Ovviamente questo non è molto utile, in quanto non si sa veramente quali associazioni ha fatto per plus e zero, ma è normale.

Per provare la proprietà, diciamo al risolutore SMT altre due cose. Innanzitutto, che plus è commutativo. E secondo, che zero aggiunto a destra non fa nulla. Questi sono fatti tramite chiamate addAxiom. Sfortunatamente, devi scrivere i tuoi assiomi nella sintassi SMTLib, dato che SBV non (almeno ancora) supporta gli assiomi scritti usando Haskell. Si noti anche che passare ad usare il Symbolic monade qui:

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 

noti come abbiamo detto al risolutore x+y = y+x e x+0 = x, e ha chiesto di dimostrare 0+x = x. Scrivere assiomi in questo modo sembra davvero brutto dato che devi usare la sintassi SMTLib, ma questo è lo stato attuale delle cose. Ora abbiamo:

*Main> good 
Q.E.D. 

assiomi quantificati e-tipi non interpretati/funzioni non sono le cose più facili da utilizzare tramite l'interfaccia SBV, ma è possibile ottenere alcuni chilometraggio in questo modo. Se hai un uso massiccio dei quantificatori nei tuoi assiomi, è improbabile che il risolutore sia in grado di rispondere alle tue domande; e probabilmente risponderà allo unknown. Tutto dipende dal solutore che si usa e dalla rigidità delle proprietà da dimostrare.

Answer 2

L'utilizzo dell'API non è corretto. Il modo più semplice per dimostrare le uguaglianze matematiche sarebbe utilizzare funzioni semplici. Per esempio, l'associatività sopra interi illimitati può essere espresso in questo modo:

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

Se avete bisogno di un'interfaccia più programmatica (e, a volte si vuole), quindi è possibile utilizzare il Symbolic Monade, questa convenzione:

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

mi consiglia la navigazione attraverso molti degli esempi forniti nel sito hackage per acquisire familiarità con l'API: https://hackage.haskell.org/package/sbv