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

Я использую SBV (с бэкэндом Z3) в Haskell для создания некоторых теоритических предсказателей. Я хочу проверить, если 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?

Ответ 1

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

Ответ 2

Ваше использование 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