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 ビットの二進浮動小数点数として表した 3 と十進数として表した 3 は、同じ数です。

///|
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 のペイロードと signaling 状態、十進のコホート、精度、区間の装飾、フラグを捨てます。それらの判定には使わないでください。
  • パッケージには順序付けがありません。上のようにたすき掛けを自分で書いてください。比較のために Double に変換してはいけません。
  • 巨大な指数を持つ十進数（例えば 1E+999999）を射影すると、指数と同じだけの桁を持つ BigInt が構築されます。射影は適度な指数の値にとどめてください。
  • 射影を持つのは @decimal.Decimal だけです。必要な場合は @decimal_gda.Decimal を文字列形式経由で変換してください。
  • ExactRational::new は分母がゼロのとき異常終了します。

次のステップ