1

我在 Isabelle 中使用 Decision_Procs 文件中的 Approximation.thy 进行区间算术。该文件为您提供了一种证明实数不等式的策略，例如：

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

现在，我有兴趣尝试似乎是 approx 函数的实现的核心功能。这在 Isabelle/HOL 中通过计算证明实值不等式的第 4.5.2 节中进行了描述。以下是我所做的一些陈述：

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 ab，也许有一种函数real_to_float r）。然后，您会看到该函数在给定一些精度（我将其理解为正确小数位数）的情况下计算作为第二个参数给出的操作的上限和下限。

现在，主要问题如下：

  • 最后一个参数的目的是什么？我猜它们是第二个参数中变量的置信区间？

  • 文中声称该函数还实现了区间算术。你能举一个例子，我可以看到这个函数是如何执行间隔加法的吗？([a,b]+[c,d]=[a+c,b+d])

4

1 回答 1

2

这些东西都不是直接使用的。这就是 Approximation 方法在它们之上提供便利层的原因。

有一个类似的功能real_to_float。它的名字是float_of，但它没有任何代码方程，所以你不能真正使用它。可以证明它的代码方程，但这有点乏味。

至于您的其他问题：是的，最后一个参数是一个列表，其中第 i 个元素是已知第 i 个变量的值所在的区间。

是的，approx执行区间算术；事实上，这正是它所做工作的核心。它完全按间隔运行。可以观察到您提到的示例，例如在执行x + ywhere xis in[1;2]和yis in 时[-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)
于 2018-10-28T17:40:02.400 回答