Символическая теория, доказывающая использование SBV и Haskell

Я использую 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?

Источник

2 ответа

Решение

Такое рассуждение действительно возможно благодаря использованию неинтерпретированных видов и функций. Имейте в виду, однако, что для рассуждения о таких структурах обычно требуются количественные аксиомы, а решатели 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 Монада здесь:

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, Все зависит от решателя, который вы используете, и от того, насколько сложны свойства для доказательства.

Источник

Ваше использование API не совсем правильно. Самый простой способ доказать математические равенства - использовать простые функции. Например, ассоциативность по неограниченным целым числам может быть выражена следующим образом:

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

Если вам нужен более программный интерфейс (а иногда и вам), то вы можете использовать Symbolic монада, таким образом:

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

Я бы порекомендовал просмотреть многие примеры, представленные на сайте взлома, чтобы ознакомиться с API: https://hackage.haskell.org/package/sbv

Источник
Другие вопросы по тегам