ada - 单独指定 'Small and ' Delta 是否有意义？

Question

编译器选择的“小”的演示者
作为 Ada 中定点类型的新手，听到 'Small 的默认值是 2 的幂，小于或等于指定的 delta 时，我感到很惊讶。这是介绍问题的简短片段:

with Ada.Text_IO; use Ada.Text_IO;

procedure Main is
   type foo is delta 0.1 range 0.0..1.0;
   x : foo := foo'delta;
begin
   Put (x'Image);
   while true loop
      x := x + foo'delta;
      Put (x'Image);
   end loop;
end Main;

输出显示 'Small 确实是小于 0.1 的 2 的最大幂，因为某些打印值出现了两次:

 0.1 0.1 0.2 0.3 0.3 0.4 0.4 0.5 0.6 0.6 0.7 0.8 0.8 0.9 0.9 1.0

raised CONSTRAINT_ERROR : main.adb:9 range check failed

解决方案:将它们指定为相同的值
如果我们真的想要 0.1 作为增量，我们可以这样说:

   real_delta : constant := 0.1;
   type foo is delta real_delta range 0.0..1.0
      with Small => real_delta;

题;将两者指定为不同的值是否有用？
如果优化是这种差异的唯一用例，它可能是一个 bool 属性，或者甚至只是一个警告“选定的增量不是 2 的幂(建议使用 2**-4)”。是否有任何理由将两者指定为单独的值，例如:

   type foo is delta 0.1 range 0.0..1.0
      with Small => 0.07;
   x : foo := 0.4 + 0.4;  -- equals 0.7 rather than 0.8

这似乎只会让后来遇到这个问题的可怜的读者感到困惑。以下示例取自 John Barnes 的 Programming in Ada 2012，第 434 页的第 17.5 节。他没有解释为什么 delta 是一个更大的值，而不是实际使用的“小”的倍数。

π : constant := Ada.numerics.π;
type angle is delta 0.1 range -4*π .. 4 *π;
for Angle'Small use π * 2.0**(-13);

我看到的唯一区别是“图像现在只打印一位数的精度。这是唯一的区别吗？
另外，为什么我的编译器拒绝 for foo'Small use foo'Delta ?
我遇到了直接执行上述操作的代码，没有常量:

type foo is delta 0.1 range 0.0..1.0;
for foo'Small use foo'Delta;

但 GNAT 提示 foo 在声明后立即被卡住:

main.adb:6:04: representation item appears too late

这在某些版本的 Ada 中有所改变吗？它应该是有效的 Ada2012 吗？

Answer 1

免责声明 : 所以定点算术是一个比较特殊的话题。这就是我对这个主题的理解，但我必须在这里发出警告:我在下面写的内容可能不正确。所以对于所有阅读它的人:如果我错了，请纠正我。
在 Ada 中，真实类型由其准确性定义。这与通过实现(即硬件表示)定义真实类型的大多数其他语言相反。在实际类型的定义中选择使用准确性属性而不是表示方面符合语言哲学:准确性作为一个概念，与正确性密切相关；语言的目标。根据准确性定义真实类型也更自然，因为您让编译器根据您对准确性的要求选择最佳类型(在计算机上，无论如何，所有值都是近似值，您必须一次性处理该事实-方式或其他)。Delta属性定义了对与基础定点类型相关的绝对误差界限(准确度)的要求(另见 Ada 83 Rationale, section 5.1.3)。优点有两方面:

程序员使用需求指定数字类型，并将硬件上的最佳表示选择委托(delegate)给编译器。

类型定义中直接说明了绝对误差界限，通常用于数值分析以分析和预测算术运算对精度的影响。数值分析(精度和范围分析)是实现计算算法的一个重要方面，尤其是在使用定点类型时。

Update 24-10-2020: These former paragraphs should be read in the context of the original language specification, Ada 83. Moreover the Ada 83 language had a second important objective that seemed to have influenced the choice for defining numeric real types using accuracy: the separation principle. See, the Ada 83 Rationale, chapter 15 for a clear statement on what this meant. When Ada 95 was developed, however, the separation between logical type properties (like accuracy) and machine representation was (at least for fixed-point types) reviewed and found to be not as useful in practice as what was hoped for (see the Ada 95 Rationale, section G.4.2). Hence, as of Ada 95, the role of the Delta attribute has been diminished and the Small attribute has been used instead in the formulation of how fixed-point types and operations should work (see, for example, RM G.2.3).

例如，考虑下面的示例程序。该程序定义了数字类型并指定“真”值与底层表示之间的绝对差异不得超过 0.07:

type Fix is delta 0.07 range 0.0 .. 10.0;     --  0.07 is just a random value here

换句话说，当给定的“真”值被强制转换为类型 Fix 时，那么它将获得 +/- 0.07 的不确定性。因此，三个命名常量 X , Y和 Z在下面的程序中，当转换为类型 Fix 时， 变得:

X : constant := 5.6;       --  Becomes 5.6 +/- 0.07 when casted to type Fix.
Y : constant := 0.3;       --  Becomes 0.3 +/- 0.07 when casted to type Fix.
Z : constant := 2.5;       --  Becomes 2.5 +/- 0.07 when casted to type Fix.

鉴于这些不确定性，我们可以计算一些算术运算序列的结果的不确定性(另请参阅 this 关于 SO 的优秀答案)。这实际上在程序中得到了演示。

Update 24-10-2020: In retrospect, this doesn't seem to be correct and there are complications. The computations of uncertainty in the program do not take into account the intermediate and final casting (quantization) of numbers that may occur during the computation and final assignment. Hence, the computed uncertainties are not correct and too optimistic (i.e. they should be larger). I will not delete the example program though as it does provide an intuition for the original intend of the Delta attribute.

进行了三个计算，均使用 Long_Float ( Flt ) 和自定义定点类型 Fix .使用 Long_Float 的计算结果当然，也是一个近似值，但为了演示起见，我们可以假设它是精确的。然而，定点计算的结果具有(非常)有限的精度，因为我们为类型 Fix 指定了相当大的误差界限。 .另一方面，定点值需要更少的空间(这里:每个值只有 8 位)并且算术运算不需要专门的浮点硬件。
您可以调整 Small 的事实属性只是为了让程序员可以控制定点类型定义的集合中可用的型号。总是制作 Small 可能很诱人表示方面等于 Delta属性，但使它们相等(通常)不会改变在使用定点数和算术运算时需要执行一些数值(错误)分析的要求。

Update 24-10-2020: This statement is only partly correct I think. The Small attribute does allow programmers to control the model numbers (i.e. number that can be represented exactly by the data type), but it's not just that. As of Ada 95, the Small attribute plays a major role in how fixed-point arithmetic is supposed to work (RM G.2.3) and, moreover, most documentation on fixed-point arithmetic and software to analyze fixed-point algorithms (see, for example here) assume that actual representation of the type in hardware is known; their treatment of the subject does not depart from an absolute error bound, but always depart from the representation of a fixed-point value.

归根结底，这一切都与以数值精度交易资源(内存、浮点硬件)有关。

Update 24-10-2020: Also this statement requires a remark: not requiring floating-point operations for executing fixed-point operations in Ada depends on a context. Fixed-point operations, in particular multiplication and division, can be done using only integer operations if the type of the operands and result of the operation have particular values for Small. It's too much detail to put here, but some interesting information can actually be found in the well documented source code of GNAT itself, see, for example, exp_fixd.adb.

Update 24-10-2020: So in conclusion, given the changes in Ada 95 and given the current state-of-art in tools for performing fixed-point analysis, there seems no strong argument to choose the values for Delta and Small differently. The Delta attribute still represents the absolute error bound, but it's value is not as useful as thought originally. It's only major use seems, as you already mentioned, be in the I/O of fixed-point data-types (RM 3.5.10 (5) and Ada.Text_IO.Fixed_IO).

main.adb

pragma Warnings (Off, "static fixed-point value is not a multiple of Small");
pragma Warnings (Off, "high bound adjusted down by delta (RM 3.5.9(13))");


with Ada.Text_IO; use Ada.Text_IO;

procedure Main is

   type Flt is new Long_Float;
   type Fix is delta 0.07 range 0.0 .. 10.0;

   ---------
   -- Put --
   ---------

   procedure Put (Nominal, Uncertainty : Flt; Result : Fix) is

      package Fix_IO is new Fixed_IO (Fix);
      use Fix_IO;

      package Flt_IO is new Float_IO (Flt);
      use Flt_IO;

   begin
      Put ("   Result will be within     : ");
      Put (Nominal, Fore => 2, Aft => 4, Exp => 0);
      Put (" +/-");
      Put (Uncertainty, Fore => 2, Aft => 4, Exp => 0);
      New_Line;

      Put ("   Actual fixed-point result : ");
      Put (Result, Fore => 2);
      New_Line (2);

   end Put;

   X : constant := 5.6;
   Y : constant := 0.3;
   Z : constant := 2.5;

   D : constant Flt := Fix'Delta;

begin

   Put_Line ("Size  of fixed-point type : " & Fix'Size'Image);
   Put_Line ("Small of fixed-point type : " & Fix'Small'Image);
   New_Line;

   --  Update 24-10-2020: Uncertainty computation is too optimistic. It omits
   --                     the effect of quantization in intermediate and final
   --                     variable assignments.

   Put_Line ("X + Y = ");
   Put (Nominal     => Flt (X) + Flt (Y),
        Uncertainty => D + D,
        Result      => Fix (X) + Fix (Y));

   Put_Line ("X * Y = ");
   Put (Nominal     => Flt (X) * Flt (Y),
        Uncertainty => (D / X + D / Y) * X * Y,
        Result      => Fix (X) * Fix (Y));

   Put_Line ("X * Y + Z = ");
   Put (Nominal     => Flt (X) * Flt (Y) + Flt (Z),
        Uncertainty => (D / X + D / Y) * X * Y + D,
        Result      => Fix (X) * Fix (Y) + Fix (Z));

end Main;

输出

Size  of fixed-point type :  8
Small of fixed-point type :  6.25000000000000000E-02

X + Y = 
   Result will be within     :  5.9000 +/- 0.1400
   Actual fixed-point result :  5.81

X * Y = 
   Result will be within     :  1.6800 +/- 0.4130
   Actual fixed-point result :  1.38

X * Y + Z = 
   Result will be within     :  4.1800 +/- 0.4830
   Actual fixed-point result :  3.88