Плавающая и интервальная арифметика в Изабель - PullRequest
Новая
       18

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

0 голосов
/ 27 октября 2018

Я использую 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 a b, возможно, есть функция вида real_to_float r). Затем вы видите, что функция вычисляет, учитывая некоторую точность (которую я понимаю как число правильных десятичных знаков), верхнюю и нижнюю границы для операций, заданных в качестве второго параметра.

Теперь главный вопрос следующий:

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

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

1 Ответ

0 голосов
/ 28 октября 2018

Ни одна из этих вещей не предназначена для непосредственного использования; вот почему метод 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)
...