Luna Flow
简体中文

semantic 教程

本教程展示如何在不舍入的前提下跨表示比较值：把二进制浮点数、IEEE 十进制数或区间投影到精确有理数，检验相等性，用整数算术对有理数排序，检查区间是否包含某个十进制数，并把 checked 结果转换为一套通用的错误词汇。该投影适用于跨表示的测试、诊断和协议边界；算术仍由具体的包完成。数学原理见设计页面；所有条目都列在 API 参考中。

快速入门

moon add Luna-Flow/floating@0.8.0
import {
  "Luna-Flow/floating/semantic",
  "Luna-Flow/floating/bin_float",
  "Luna-Flow/floating/decimal",
}

三表示为 32 位二进制浮点数和表示为十进制数时，是同一个数：

///|
test "quick start: same value, different representations" {
  let binary = @bin_float.BinFloat::from_int(3, precision=32)
  let decimal = @decimal.Decimal::from_int(3, precision=32)
  inspect(
    @semantic.SemanticScalar::from_bin_float(binary) ==
    @semantic.SemanticScalar::from_decimal(decimal),
    content="true",
  )
}

日常任务

查看浮点数的精确值

下面的示例用这个辅助函数打印投影后的标量：

///|
fn exact(s : @semantic.SemanticScalar) -> String {
  match s {
    Rational(q) => q.numerator().to_string() + "/" + q.denominator().to_string()
    Infinity(@def.Sign::Negative) => "-inf"
    Infinity(_) => "+inf"
    NaN => "nan"
  }
}

///|
test "the double nearest to one tenth" {
  let tenth = @bin_float.BinFloat::from_double(0.1)
  inspect(
    exact(@semantic.SemanticScalar::from_bin_float(tenth)),
    content="3602879701896397/36028797018963968",
  )
  let decimal = @decimal.Decimal::from_string("0.1").unwrap()
  inspect(exact(@semantic.SemanticScalar::from_decimal(decimal)), content="1/10")
}

二进制值的分母是 2552^{55}；十进制值恰好是 1/101/10。两者的投影不同，因此 binary64 0.1 不是十分之一。

忽略同值类、精度和带符号零

十进制的 1.5、1.50 和 1.500 是同一个值的不同表示（一个同值类）；二进制值带有精度；零有两种符号。投影会忽略所有这些：

///|
test "the projection keeps only the value" {
  let a = @decimal.Decimal::from_string("1.500").unwrap()
  let b = @bin_float.BinFloat::from_double(1.5)
  inspect(
    @semantic.SemanticScalar::from_decimal(a) ==
    @semantic.SemanticScalar::from_bin_float(b),
    content="true",
  )
  let negative_zero = @bin_float.BinFloat::from_double(-0.0)
  let zero = @decimal.Decimal::zero()
  inspect(
    @semantic.SemanticScalar::from_bin_float(negative_zero) ==
    @semantic.SemanticScalar::from_decimal(zero),
    content="true",
  )
}

精确地比较两个值的大小

本包只提供相等性。由于投影得到的有理数暴露了约分后的分子和正的分母，你可以用交叉相乘规则 a/b<c/d  ⟺  ad<cba/b < c/d \iff ad < cb 对其中两个排序（因为 b,d>0b, d > 0，该规则成立）：

///|
fn rational_less(a : @semantic.ExactRational, b : @semantic.ExactRational) -> Bool {
  a.numerator() * b.denominator() < b.numerator() * a.denominator()
}

///|
test "binary 0.1 lies above one tenth" {
  let binary = match
    @semantic.SemanticScalar::from_bin_float(@bin_float.BinFloat::from_double(0.1)) {
    Rational(q) => q
    _ => fail("finite")
  }
  let tenth = @semantic.ExactRational::new(1N, 10N)
  inspect(rational_less(tenth, binary), content="true")
}

检查区间是否包络某个十进制数

SemanticInterval::from_ball_float 暴露了球的精确端点。结合上面的比较，你可以在不做任何舍入的情况下，用十进制参考值检查包络：

///|
fn encloses(x : @semantic.SemanticInterval, q : @semantic.ExactRational) -> Bool {
  let above_lower = match x.lower {
    Rational(l) => !rational_less(q, l)
    Infinity(@def.Sign::Negative) => true
    _ => false
  }
  let below_upper = match x.upper {
    Rational(u) => !rational_less(u, q)
    Infinity(@def.Sign::Positive) => true
    _ => false
  }
  above_lower && below_upper
}

///|
test "a ball for one tenth" {
  let ball = @ball_float.BallFloat::from_bounds(
    @bin_float.BinFloat::from_double(0.09375),
    @bin_float.BinFloat::from_double(0.125),
  )
  let projected = @semantic.SemanticInterval::from_ball_float(ball)
  inspect(encloses(projected, @semantic.ExactRational::new(1N, 10N)), content="true")
  inspect(encloses(projected, @semantic.ExactRational::new(1N, 5N)), content="false")
  let empty = @semantic.SemanticInterval::from_ball_float(@ball_float.BallFloat::empty())
  inspect(encloses(empty, @semantic.ExactRational::new(0N, 1N)), content="false")
}

空区间投影为反转的对 (+∞,−∞)(+\infty, -\infty)，因此辅助函数无需特殊处理即可拒绝每个值。

深入了解

跨包比较 checked 结果

semantic_scalar_result 把 Result[T, ArithmeticError] 映射为 SemanticResult，因此来自一个包的错误与来自另一个包的同一错误比较为相等，尽管它们的消息不同：

///|
test "errors compare by kind" {
  let binary = @semantic.semantic_scalar_result(
    @bin_float.BinFloat::from_int(1).div_checked(@bin_float.BinFloat::zero()),
    @semantic.SemanticScalar::from_bin_float,
  )
  let decimal = @semantic.semantic_scalar_result(
    @decimal.Decimal::from_int(1).div_checked(@decimal.Decimal::zero()),
    @semantic.SemanticScalar::from_decimal,
  )
  inspect(binary == decimal, content="true")
  inspect(
    binary == @semantic.SemanticResult::Error(@semantic.SemanticError::DivisionByZero),
    content="true",
  )
}

交叉检验两种实现

典型的一致性测试在两种表示下计算同一个结果，把两者都舍入为在各自表示中都能精确表示的值，然后比较投影。完全平方数的平方根在两种基数下都是精确的：

///|
test "binary and decimal agree on exact square roots" {
  for n in [1, 4, 9, 144, 1024] {
    let b = @semantic.semantic_scalar_result(
      @bin_float.BinFloat::from_int(n).sqrt(),
      @semantic.SemanticScalar::from_bin_float,
    )
    let d = @semantic.semantic_scalar_result(
      @decimal.Decimal::from_int(n).sqrt(),
      @semantic.SemanticScalar::from_decimal,
    )
    assert_true(b == d)
  }
}

常见陷阱

  • 对 SemanticScalar 而言 NaN == NaN 为 true。投影是一种值模型，而不是 IEEE 比较；IEEE 谓词请使用具体的包。
  • 投影丢弃了零的符号、NaN 载荷与信号状态、十进制同值类、精度、区间装饰和标志。不要用它来检验这些属性。
  • 本包没有提供序。请像上面那样自己写交叉相乘；切勿为了比较而转换为 Double。
  • 投影一个指数极大的十进制数（例如 1E+999999）会构造一个位数与指数相当的 BigInt。请只对指数适中的值进行投影。
  • 只有 @decimal.Decimal 有投影；如果需要投影 @decimal_gda.Decimal，请经由其字符串形式转换。
  • ExactRational::new 在分母为零时中止。

后续步骤