semantic API

semantic は floating の具体的な値を、表現に依存しない小さなモデルへ射影します。このモデルは、厳密な既約有理数、符号付き無限大、NaN、そのようなスカラーの閉区間、そして簡潔なエラー語彙からなります。異なる表現の 2 つの値(たとえば binary64 の BinFloat と IEEE の Decimal)は、同じ数を表すときに限り等しい意味値に射影されます。このパッケージは算術演算も丸めも行いません。チュートリアルでは典型的な比較を示し、設計ページでは射影が厳密である理由と、射影によって失われる情報を導いています。

例では、意味スカラーを numerator/denominator の形で表示する次のヘルパーを前提とします。

///|
fn show(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"
  }
}

厳密な有理数

ExactRational

ExactRational は、既約で分母が正の形に保たれる厳密な有理数です。

pub struct ExactRational {
  // private fields
} derive(Eq)

フィールドは非公開なので、すべての値は ExactRational::new または ExactRational::from_scaled_integer によって構築され、次の不変条件を満たします。

nd  with  d>0,gcd⁡(∣n∣,d)=1,n=0  ⟹  d=1.\frac{n}{d}\ \text{ with }\ d > 0,\quad \gcd(|n|, d) = 1,\quad n = 0 \implies d = 1.

この形はすべての有理数に対して一意なので、導出された == は有理数としての等価性になります。

ExactRational::new

new(numerator, denominator) は有理数 n/dn/d を構築し、約分します。

pub fn ExactRational::new(@bigint.BigInt, @bigint.BigInt) -> Self

負の分母はその符号が分子に移され、両者はその最大公約数(BigInt 上のユークリッドの互除法)で割られます。ゼロは 0/10/1 になります。denominator がゼロのときは中断します。

ExactRational::from_scaled_integer

from_scaled_integer(significand, radix, exponent) は厳密な値 m⋅rem \cdot r^{e} を構築します。

pub fn ExactRational::from_scaled_integer(@bigint.BigInt, Int, Int) -> Self

e≥0e \ge 0 のとき結果は (mre)/1(m r^{e})/1、e<0e < 0 のときは m/r−em / r^{-e} を約分したものです。radix ≤1\le 1 のときは中断します。冪は厳密に計算されるため、結果のサイズは ∣e∣|e| に比例して(約 ∣e∣log⁡2r|e| \log_2 r ビット)増加します。

ExactRational::numerator, ExactRational::denominator

これらのアクセサは、約分された分子(符号を持つ)と正の分母を返します。

pub fn ExactRational::numerator(Self) -> @bigint.BigInt
pub fn ExactRational::denominator(Self) -> @bigint.BigInt
///|
test "exact rationals are reduced" {
  let q = @semantic.ExactRational::new(6N, -8N)
  inspect(q.numerator().to_string() + "/" + q.denominator().to_string(), content="-3/4")
  let scaled = @semantic.ExactRational::from_scaled_integer(-12N, 10, -3)
  inspect(
    scaled.numerator().to_string() + "/" + scaled.denominator().to_string(),
    content="-3/250",
  )
  inspect(
    @semantic.ExactRational::from_scaled_integer(3N, 2, 4) ==
    @semantic.ExactRational::new(48N, 1N),
    content="true",
  )
}

スカラー

SemanticScalar

SemanticScalar は 1 つの浮動小数点データの意味です。

pub(all) enum SemanticScalar {
  Rational(ExactRational)
  Infinity(@def.Sign)
  NaN
} derive(Eq)

Rational はすべての有限値を保持し、符号付きゼロはどちらも 0/10/1 になります。Infinity は Negative または Positive を持ちます。NaN はすべての NaN(quiet でも signaling でも、任意のペイロード、任意の符号)を表します。等価性は構造的なので、IEEE の比較とは異なり、ここでは NaN == NaN は true です。

SemanticScalar::from_bin_float

from_bin_float(x) は BinFloat の厳密な意味を返します。

pub fn SemanticScalar::from_bin_float(@bin_float.BinFloat) -> Self

有限の x=(−1)sc 2ex = (-1)^{s} c\, 2^{e} は from_scaled_integer(±c, 2, e) の Rational に、無限大は Infinity(x.sign()) に、NaN は NaN に対応付けられます。精度は捨てられます。決して中断しません。

SemanticScalar::from_decimal

from_decimal(x) は IEEE の @decimal.Decimal の厳密な意味を返します。

pub fn SemanticScalar::from_decimal(@decimal.Decimal) -> Self

有限の x=(−1)sc 10qx = (-1)^{s} c\, 10^{q} は from_scaled_integer(±c, 10, q) の Rational に対応付けられるため、コホートのすべての要素(1.5、1.50、1.500)は同じ値 3/23/2 に対応付けられます。無限大と NaN は 2 進の場合と同様に対応付けられます。GDA 型 @decimal_gda.Decimal はこのパッケージでは射影を持ちません。

///|
test "project binary and decimal values" {
  let binary = @semantic.SemanticScalar::from_bin_float(
    @bin_float.BinFloat::from_double(0.1),
  )
  inspect(show(binary), content="3602879701896397/36028797018963968")
  let decimal = @semantic.SemanticScalar::from_decimal(
    @decimal.Decimal::from_string("0.1").unwrap(),
  )
  inspect(show(decimal), content="1/10")
  inspect(binary == decimal, content="false")
  let half = @semantic.SemanticScalar::from_bin_float(
    @bin_float.BinFloat::from_double(0.5),
  )
  let half_decimal = @semantic.SemanticScalar::from_decimal(
    @decimal.Decimal::from_string("0.500").unwrap(),
  )
  inspect(half == half_decimal, content="true")
  inspect(
    show(@semantic.SemanticScalar::from_bin_float(@bin_float.BinFloat::from_double(-0.0))),
    content="0/1",
  )
  inspect(
    @semantic.SemanticScalar::from_bin_float(@bin_float.BinFloat::nan()) ==
    @semantic.SemanticScalar::NaN,
    content="true",
  )
}

区間

SemanticInterval

SemanticInterval は 2 つの意味端点で与えられる閉区間です。

pub struct SemanticInterval {
  lower : SemanticScalar
  upper : SemanticScalar
} derive(Eq)

フィールドは公開されており、パッケージ外からは読み取り専用です。この型は lower が upper を超えないことを検査しません。以下の射影では、空集合に対して逆転した組 (+∞,−∞)(+\infty, -\infty) を用います。

SemanticInterval::from_ball_float

from_ball_float(x) は BallFloat の 2 つの端点を射影します。

pub fn SemanticInterval::from_ball_float(@ball_float.BallFloat) -> Self

lower は from_bin_float(x.lower_bound())、upper は from_bin_float(x.upper_bound()) です。有界な区間は 2 つの Rational 端点を、非有界な側は Infinity を与え、実数直線全体は (−∞,+∞)(-\infty, +\infty) を、空区間は (Infinity(Positive),Infinity(Negative))(\texttt{Infinity(Positive)}, \texttt{Infinity(Negative)}) を与えます。装飾、精度、フラグは捨てられます。

///|
test "project intervals" {
  let x = @semantic.SemanticInterval::from_ball_float(
    @ball_float.BallFloat::from_bounds(
      @bin_float.BinFloat::from_int(1),
      @bin_float.BinFloat::from_double(2.5),
    ),
  )
  inspect(show(x.lower) + " .. " + show(x.upper), content="1/1 .. 5/2")
  let whole = @semantic.SemanticInterval::from_ball_float(
    @ball_float.BallFloat::whole(),
  )
  inspect(show(whole.lower) + " .. " + show(whole.upper), content="-inf .. +inf")
  let empty = @semantic.SemanticInterval::from_ball_float(
    @ball_float.BallFloat::empty(),
  )
  inspect(show(empty.lower) + " .. " + show(empty.upper), content="+inf .. -inf")
}

エラーと checked 結果

SemanticError

SemanticError は表現に依存しないエラー語彙です。

pub(all) enum SemanticError {
  DivisionByZero
  ParseError
  DomainError
  FormatError
  UnsupportedOperation
  UnorderedComparison
  CertificationFailure
} derive(Eq)

これは Luna-Flow/arithmetic の ArithmeticErrorKind を、メッセージと認証の詳細を除いて写したものです。

SemanticError::from_arithmetic

from_arithmetic(err) は ArithmeticError を分類します。

pub fn SemanticError::from_arithmetic(@arithmetic.ArithmeticError) -> Self

種類は、ゼロ除算、パース、定義域、書式、順序付けられない比較、認証失敗の順に判定されます。それ以外(UnsupportedOperation の種類)は UnsupportedOperation に対応付けられます。メッセージと CertificationFailureDetail は捨てられます。

SemanticResult

SemanticResult[T] は意味値または意味エラーです。

pub(all) enum SemanticResult[T] {
  Value(T)
  Error(SemanticError)
} derive(Eq)

semantic_scalar_result, semantic_interval_result

これらの関数は、具体的なパッケージの checked 結果を意味結果に変換します。成功時には呼び出し側が与える射影を用います。

pub fn[T] semantic_scalar_result(Result[T, @arithmetic.ArithmeticError], (T) -> SemanticScalar) -> SemanticResult[SemanticScalar]
pub fn[T] semantic_interval_result(Result[T, @arithmetic.ArithmeticError], (T) -> SemanticInterval) -> SemanticResult[SemanticInterval]
semantic_scalar_result(Ok(v),f)=Value(f(v)),semantic_scalar_result(Err(e),f)=Error(from_arithmetic(e)),\begin{aligned} \texttt{semantic\_scalar\_result}(\texttt{Ok}(v), f) &= \texttt{Value}(f(v)),\\ \texttt{semantic\_scalar\_result}(\texttt{Err}(e), f) &= \texttt{Error}(\texttt{from\_arithmetic}(e)), \end{aligned}

区間についても同様です。f は高々 1 回しか呼ばれません。

///|
test "checked results become semantic results" {
  let failed = @semantic.semantic_scalar_result(
    @bin_float.BinFloat::from_int(1).div_checked(@bin_float.BinFloat::zero()),
    @semantic.SemanticScalar::from_bin_float,
  )
  inspect(
    failed == @semantic.SemanticResult::Error(@semantic.SemanticError::DivisionByZero),
    content="true",
  )
  let root = @semantic.semantic_scalar_result(
    @bin_float.BinFloat::from_int(4).sqrt(),
    @semantic.SemanticScalar::from_bin_float,
  )
  let two = @semantic.SemanticScalar::from_decimal(@decimal.Decimal::from_int(2))
  inspect(root == @semantic.SemanticResult::Value(two), content="true")
}

トレイト実装

等価性

このパッケージのすべての型は Eq を導出しており、equal と not_equal のメソッドは明示的に昇格されています。== と != の使用を推奨します。

pub fn ExactRational::equal(Self, Self) -> Bool
pub fn ExactRational::not_equal(Self, Self) -> Bool
pub fn SemanticScalar::equal(Self, Self) -> Bool
pub fn SemanticScalar::not_equal(Self, Self) -> Bool
pub fn SemanticInterval::equal(Self, Self) -> Bool
pub fn SemanticInterval::not_equal(Self, Self) -> Bool
pub fn SemanticError::equal(Self, Self) -> Bool
pub fn SemanticError::not_equal(Self, Self) -> Bool
pub fn[T : Eq] SemanticResult::equal(Self[T], Self[T]) -> Bool
pub fn[T : Eq] SemanticResult::not_equal(Self[T], Self[T]) -> Bool

ExactRational の等価性は、既約形であるため数値としての等価性になります。SemanticScalar の等価性はそれに加えて NaN == NaN を真とし、2 つの無限大を区別します。順序は提供されません。

公開インターフェース全体

以下のスナップショットは、パッケージの生成された完全なインターフェースです。

// Generated using `moon info`, DON'T EDIT IT
package "Luna-Flow/floating/semantic"

import {
  "Luna-Flow/arithmetic",
  "Luna-Flow/floating/ball_float",
  "Luna-Flow/floating/bin_float",
  "Luna-Flow/floating/decimal",
  "Luna-Flow/floating/def",
  "moonbitlang/core/bigint",
}

// Values
pub fn[T] semantic_interval_result(Result[T, @arithmetic.ArithmeticError], (T) -> SemanticInterval) -> SemanticResult[SemanticInterval]

pub fn[T] semantic_scalar_result(Result[T, @arithmetic.ArithmeticError], (T) -> SemanticScalar) -> SemanticResult[SemanticScalar]

// Errors

// Types and methods
pub struct ExactRational {
  // private fields
} derive(Eq)
pub fn ExactRational::denominator(Self) -> @bigint.BigInt
pub fn ExactRational::equal(Self, Self) -> Bool
pub fn ExactRational::from_scaled_integer(@bigint.BigInt, Int, Int) -> Self
pub fn ExactRational::new(@bigint.BigInt, @bigint.BigInt) -> Self
pub fn ExactRational::not_equal(Self, Self) -> Bool
pub fn ExactRational::numerator(Self) -> @bigint.BigInt

pub(all) enum SemanticError {
  DivisionByZero
  ParseError
  DomainError
  FormatError
  UnsupportedOperation
  UnorderedComparison
  CertificationFailure
} derive(Eq)
pub fn SemanticError::equal(Self, Self) -> Bool
pub fn SemanticError::from_arithmetic(@arithmetic.ArithmeticError) -> Self
pub fn SemanticError::not_equal(Self, Self) -> Bool

pub struct SemanticInterval {
  lower : SemanticScalar
  upper : SemanticScalar
} derive(Eq)
pub fn SemanticInterval::equal(Self, Self) -> Bool
pub fn SemanticInterval::from_ball_float(@ball_float.BallFloat) -> Self
pub fn SemanticInterval::not_equal(Self, Self) -> Bool

pub(all) enum SemanticResult[T] {
  Value(T)
  Error(SemanticError)
} derive(Eq)
pub fn[T : Eq] SemanticResult::equal(Self[T], Self[T]) -> Bool
pub fn[T : Eq] SemanticResult::not_equal(Self[T], Self[T]) -> Bool

pub(all) enum SemanticScalar {
  Rational(ExactRational)
  Infinity(@def.Sign)
  NaN
} derive(Eq)
pub fn SemanticScalar::equal(Self, Self) -> Bool
pub fn SemanticScalar::from_bin_float(@bin_float.BinFloat) -> Self
pub fn SemanticScalar::from_decimal(@decimal.Decimal) -> Self
pub fn SemanticScalar::not_equal(Self, Self) -> Bool

// Type aliases

// Traits