Плавающая и интервальная арифметика в Изабель

Question

Я использую Approximation.thy из файла Descision_Procs для интервальной арифметики в Изабель. Файл дает вам тактику для доказательства неравенства по реалам, например:

theorem "3 ≤ x ∧ x ≤ 6 ⟹ sin ( pi / x) > 0.4" by (approximation 10)

Теперь я заинтересован в том, чтобы опробовать основную функцию реализации, которая выглядит как функция приближения. Это описано в разделе 4.5.2 "Проверка вещественных неравенств путем вычислений в Изабель /HOL". Вот некоторые из заявлений, которые я делаю:

value "Float 3 (-1)"
value "approx 1 (Num (Float 3 (-2))) [Some (Float 1 0,Float 4 0)]"
value "approx 1 (Add (Num (Float 3 (-2))) (Num (Float 4 (-8)))) [Some (Float 1 0,Float 4 0)]"
value "approx 1 (Add (Var 1) (Num (Float 4 (-8)))) [Some (Float 1 0,Float 4 0)]"

Во-первых, я хотел бы спросить, знаете ли вы более удобный способ написания float (вместо Float a b, может быть, есть такая функция real_to_float r). Затем вы видите, что функция вычисляет, учитывая некоторую точность (которую я понимаю как число правильных десятичных знаков), верхнюю и нижнюю границы для операций, заданных в качестве второго параметра.

Теперь главный вопрос заключается в следующем:

• Какова цель последнего параметра? Я предполагаю, что они являются доверительными интервалами для переменных во втором параметре?

• В тексте утверждается, что эта функция также реализует интервальную арифметику. Можете ли вы показать пример, где я могу видеть, как эта функция выполняет, например, добавление интервала? ([А, Ь]+[с,d]=[а + с, B + D])

Answer 1

Ни одна из этих вещей не предназначена для непосредственного использования; Вот почему метод Approximation предлагает удобный слой над ними.

Есть такая функция real_to_float, Его имя float_of, но у него нет кодовых уравнений, поэтому вы не можете его использовать. Можно было доказать кодовое уравнение для этого, но это было бы немного утомительно.

Что касается других ваших вопросов: Да, последний параметр - это список, где i-й элемент - это интервал, в котором, как известно, лежит значение i-й переменной.

И да, approx выполняет интервальную арифметику; на самом деле, это является основой того, что он делает. Он работает исключительно на интервалах. Приведенный вами пример можно наблюдать, например, при выполнении x + y где x в [1;2] а также y в [-1;2]:

value "approx 10 (Add (Var 0) (Var 1))
         [Some (Float 1 0, Float 1 1), Some (Float (-1) 0, Float 1 1)]"

который возвращает интервал [0;4]:

"Some (Float 0 0, Float 2 1)"
  :: "(float × float) option"

или, более прямо:

lemma "(x :: real) ∈ {1..2} ⟹ y ∈ {-1..2} ⟹ x + y ∈ {0..4}"
  by (approximation 10)