Как получить символические функции квадратного корня и логарифма в SBV?

Question

Единственное решение, которое я могу найти - это приближение квадратного корня, но это не работает символически, поэтому я не могу использовать его для доказательства.

Answer 1

SBV уже поддерживает квадратный корень для типов с плавающей точкой:

Одинарная точность:

Prelude Data.SBV> sat $ \x -> x .== fpSqrt sRNE (4.2::SFloat)
Satisfiable. Model:
  s0 = 2.04939 :: Float

Двойная точность:

Prelude Data.SBV> sat $ \x -> x .== fpSqrt sRNE (4.2::SDouble)
Satisfiable. Model:
  s0 = 2.04939015319192 :: Double

Обратите внимание, что вы должны предоставить режим округления, в приведенном выше sRNE который обозначает round-nearest-towards-even который является режимом округления по умолчанию, используемым в Haskell. SBV поддерживает все 5 режимов округления IEEE, если это необходимо.

Вы также можете использовать вещественные числа (алгебраические действительные числа произвольной точности):

Prelude Data.SBV> sat $ \x -> x * x .==  (4.2::SReal)
Satisfiable. Model:
  s0 = root(1, 5x^2 = 21) = -2.0493901531919196... :: Real

В этом случае вы получите алгебраическое уравнение и аппроксимацию реального результата. (Обратите внимание, что выше x*x == 4.2 такой же как 5*x^2 = 21). Обе формы доступны из программного API.

Там нет единой функции для целочисленных квадратных корней; ни для логарифмов. Эти последние могут быть выражены с помощью квантификаторов, но решатели SMT вряд ли дадут хорошие результаты для них, так как они будут включать в себя как нелинейную арифметику, так и количественную оценку.

В общем, обратите внимание, что ни SBV, ни SMT решатели не подходят для "упрощения" символьных выражений. Вы всегда получите конкретный ответ на свой запрос: если вы попросите sqrt 50, ты получишь 7.07106 (в правильном типе / точности), вместо таких вещей, как 5 * sqrt 2, например.