Luna Flow
日本語

core 設計

設計目標

luna-generic は LunaFlow 全体に共有される代数語彙を与え、 arithmetic、luna-complex、linear-algebra、luna-poly などが同じ能力境界を再利用できるようにします。

主な設計判断

  • trait グラフを層化し、小さく保つ。
  • Ring、Field、Integral、Nat のような構造 traits と、 Zero、One、Inverse、Conjugate のような操作 traits を分離する。
  • 変換は、BigInt で表される ℤ で出会う二つの半分に分かれます。対象側は標準写像 ℤ -> R（FromInteger）で、一意であり常に準同型です。ソース側は Integral::normalize で、代表元を選びますが、準同型になるのは ℤ そのものの場合だけです。lift_to は両者を合成し、演算については何も約束しません。
  • どちらの半分も単一パラメータの trait です。すべての変換は始対象である環 ℤ を経由して分解されるため、二つの型を関係づける trait は必要ありません。
  • Integral は法則 from_integer(normalize(x)) == x によって FromInteger を拡張し、整数型を代表元の選ばれた ℤ の商にします。FromInteger は総称的な整数ソースではなく BigInt を受け取るので、trait 同士が互いを参照することはありません。
  • 符号なし型に加法逆元を主張させず、数学的整合性を保つ。
  • Field は可換体を意味します。その法則は、ほかの構造 trait と同じく実装者への契約であり、コンパイラが検査するものではありません。

数学的背景

各構造 trait は代数的構造のシグネチャで、その構造の公理がインスタンスの約束する法則です。x,y,zx, y, z はキャリア全体を動きます:

Trait構造スーパー trait に追加される法則
AddMonoidモノイド (A,+,0)(A, +, 0)(x+y)+z=x+(y+z)(x+y)+z = x+(y+z), 0+x=x+0=x0+x = x+0 = x
MulMonoidモノイド (A,⋅,1)(A, \cdot, 1)(xy)z=x(yz)(xy)z = x(yz), 1x=x1=x1x = x1 = x
AddGroup群 (A,+,0,−)(A, +, 0, -)x+(−x)=(−x)+x=0x + (-x) = (-x) + x = 0
MulGroup群 (A,⋅,1,−1)(A, \cdot, 1, {}^{-1})xx−1=x−1x=1x x^{-1} = x^{-1} x = 1
Semiring半環x+y=y+xx+y = y+x, x(y+z)=xy+xzx(y+z) = xy+xz, (x+y)z=xz+yz(x+y)z = xz+yz, 0x=x0=00x = x0 = 0
Ring環AddGroup の法則
Field体xy=yxxy = yx、x≠0x \neq 0 なら xx−1=1x x^{-1} = 1、x/y=xy−1x/y = x y^{-1}

スーパー trait のグラフは構造間の包含を反映しています。すべての環は半環であり、すべての半環は加法モノイドでも乗法モノイドでもある、という具合です。T : Ring で制約された関数はちょうど環の公理の帰結を使えるので、ジェネリックなコードはすべてのインスタンスで正しくなります。

このような構造の間の準同型 φ:A→B\varphi : A \to B はシグネチャのすべての演算を保存します:

φ(0)=0,φ(1)=1,φ(x+y)=φ(x)+φ(y),φ(xy)=φ(x)φ(y).\varphi(0) = 0, \quad \varphi(1) = 1, \quad \varphi(x + y) = \varphi(x) + \varphi(y), \quad \varphi(xy) = \varphi(x)\varphi(y).

ℤ の商としての整数

この節では FromNat、FromInteger、Integral、lift_to の背後にある数学を説明します。数学抜きでの使い方はcore チュートリアルにあります。

標準写像は一意である

任意の環 R に対して、環準同型 ℤ -> R はちょうど一つ存在します。環準同型 φ は 1 を 1 に送らなければならず、加法性から n > 0 では φ(n) = 1 + ... + 1（n 個）、さらに φ(-n) = -φ(n) が強制されます。逆に、分配法則により n ↦ n·1 は + と * を保存します。同じ議論により、任意の半環 R に対して半環準同型 ℕ -> R もちょうど一つ存在します。圏論の言葉では、ℕ と ℤ は始対象です。

完全な導出を、まず ℕ について示します。RR を半環とし、φ:N→R\varphi : \mathbb{N} \to R を再帰的に定義します:

φ(0)=0,φ(n+1)=φ(n)+1.\varphi(0) = 0, \qquad \varphi(n + 1) = \varphi(n) + 1 .

加法性。nn に関する帰納法（RR における ++ の結合法則を使用）:

φ(m+0)=φ(m)=φ(m)+φ(0),φ(m+(n+1))=φ((m+n)+1)=φ(m+n)+1=(φ(m)+φ(n))+1=φ(m)+φ(n+1).\begin{aligned} \varphi(m + 0) &= \varphi(m) = \varphi(m) + \varphi(0), \\ \varphi(m + (n+1)) &= \varphi((m + n) + 1) = \varphi(m + n) + 1 \\ &= (\varphi(m) + \varphi(n)) + 1 = \varphi(m) + \varphi(n + 1). \end{aligned}

乗法性。nn に関する帰納法（吸収則 x⋅0=0x \cdot 0 = 0、加法性、分配法則を使用）:

φ(m⋅0)=0=φ(m)⋅0=φ(m)φ(0),φ(m(n+1))=φ(mn+m)=φ(m)φ(n)+φ(m)=φ(m)(φ(n)+1)=φ(m)φ(n+1).\begin{aligned} \varphi(m \cdot 0) &= 0 = \varphi(m) \cdot 0 = \varphi(m)\varphi(0), \\ \varphi(m(n+1)) &= \varphi(mn + m) = \varphi(m)\varphi(n) + \varphi(m) \\ &= \varphi(m)(\varphi(n) + 1) = \varphi(m)\varphi(n + 1). \end{aligned}

一意性: 任意の半環準同型 ψ\psi は ψ(0)=0\psi(0) = 0 と ψ(n+1)=ψ(n)+ψ(1)=ψ(n)+1\psi(n + 1) = \psi(n) + \psi(1) = \psi(n) + 1 を満たし、これは同じ漸化式なので、帰納法により ψ=φ\psi = \varphi です。

ℤ については、RR を環とします。すべての整数は自然数の差 a−ba - b として書けるので、φ^(a−b)=φ(a)−φ(b)\hat\varphi(a - b) = \varphi(a) - \varphi(b) と置きます。これは well-defined です。a−b=c−da - b = c - d は ℕ で a+d=b+ca + d = b + c を意味し、したがって RR で φ(a)+φ(d)=φ(b)+φ(c)\varphi(a) + \varphi(d) = \varphi(b) + \varphi(c) となり、両辺に −φ(b)−φ(d)-\varphi(b) - \varphi(d) を加えると（++ は可換）φ(a)−φ(b)=φ(c)−φ(d)\varphi(a) - \varphi(b) = \varphi(c) - \varphi(d) を得ます。項ごとに加法的で、分配法則により乗法的です:

φ^((a−b)(c−d))=φ^((ac+bd)−(ad+bc))=φ(a)φ(c)+φ(b)φ(d)−φ(a)φ(d)−φ(b)φ(c)=(φ(a)−φ(b))(φ(c)−φ(d)).\begin{aligned} \hat\varphi((a - b)(c - d)) &= \hat\varphi((ac + bd) - (ad + bc)) \\ &= \varphi(a)\varphi(c) + \varphi(b)\varphi(d) - \varphi(a)\varphi(d) - \varphi(b)\varphi(c) \\ &= (\varphi(a) - \varphi(b))(\varphi(c) - \varphi(d)). \end{aligned}

環準同型は ψ(−n)=−ψ(n)\psi(-n) = -\psi(n) も満たさなければならないので、負の数でも φ^\hat\varphi と一致し、φ^\hat\varphi は一意です。11 圏論の言葉では、ℕ は半環の圏の始対象、ℤ は環の圏の始対象です。ℤ は加法モノイド ℕ のグロタンディーク群であり、上で使ったのはこの構成です。

この写像は R だけで決まるので、対象側の性質として単一パラメータの trait で表せます: FromNat::from_natural と FromInteger::from_integer。

固定幅の整数

Int は 2^32 を法として加算・乗算するので、環としては ℤ/2^32 です。その from_integer は全射である簡約 ℤ -> ℤ/2^32 です。normalize は逆向きで、各剰余類から整数を一つ、[-2^31, 2^31) にあるものを選びます。法則 from_integer(normalize(x)) == x は、normalize が簡約の切断であることをちょうど表しています:

  • normalize は左逆を持つので単射です。
  • その像は各類のちょうど一つの元を含みます。単射なので高々一つ、法則により少なくとも一つです。
  • 準同型ではありません: normalize(2147483647 + 1) = -2^31 ですが、normalize(2147483647) + normalize(1) = 2^31 です。

記号で書くと、m=2km = 2^k、π:Z→Z/m\pi : \mathbb{Z} \to \mathbb{Z}/m を核が mZm\mathbb{Z} の簡約写像として、同梱のインスタンスは次を使います

ssigned(π(n))=((n+2k−1) mod 2k)−2k−1,sunsigned(π(n))=n mod 2k,s_{\text{signed}}(\pi(n)) = \bigl((n + 2^{k-1}) \bmod 2^k\bigr) - 2^{k-1}, \qquad s_{\text{unsigned}}(\pi(n)) = n \bmod 2^k,

ここで  mod \bmod は [0,2k)[0, 2^k) の値をとります。nn と n+jmn + jm が同じ値を与えるのでどちらも well-defined で、それぞれ nn との差が mm の倍数なのでどちらも π(s(x))=x\pi(s(x)) = x を満たします。上の単射性の二つの段階を書き下すと次のとおりです:

s(x)=s(y)  ⟹  x=π(s(x))=π(s(y))=y.s(x) = s(y) \;\Longrightarrow\; x = \pi(s(x)) = \pi(s(y)) = y .

加法性のずれは法の倍数です:

s(x)+s(y)−s(x+y)∈mZ,becauseπ(s(x)+s(y))=x+y=π(s(x+y)).s(x) + s(y) - s(x + y) \in m\mathbb{Z}, \qquad\text{because}\qquad \pi\bigl(s(x) + s(y)\bigr) = x + y = \pi\bigl(s(x + y)\bigr).

Int で x=231−1x = 2^{31} - 1、y=1y = 1 とするとずれは 2322^{32} なので、どのように代表元を選んでも修正できません。ss が準同型になるのは m=0m = 0 のとき、つまり BigInt の場合だけです。

切断が何を保存するかはhom 設計で説明します。

変換が準同型になるとき

lift_to : S -> R は R::from_integer と S::normalize の合成です。S が ℤ/m（BigInt では m = 0）のとき、環準同型 ℤ/m -> R が存在するのは R で m·1 = 0 となるとき、かつそのときに限ります:

  • ψ がそのような準同型なら、R において 0 = ψ(0) = ψ(m·1) = m·1 です。
  • m·1 = 0 なら、標準写像 ℤ -> R は mℤ を 0 に送るので ℤ/m を経由して分解します。ℤ -> ℤ/m は全射なので、この分解は一意です。

このとき lift_to はこの準同型そのものです。標準写像 ℤ -> R を π : ℤ -> ℤ/m を用いて ψ ∘ π と書くと、lift_to = ψ ∘ π ∘ normalize = ψ です。したがって:

  • Int64 -> Int は準同型です。2^64 ≡ 0 (mod 2^32) だからです。
  • Int -> Int64 は準同型ではありません。2^32 ≢ 0 (mod 2^64) だからです。
  • 固定幅の整数から BigInt、Float、Double への準同型は存在しません。これらではすべての m > 0 について m·1 ≠ 0 だからです。

同じ議論を一つの連鎖で書きます。ιR:Z→R\iota_R : \mathbb{Z} \to R を標準写像とし、m⋅1R=0m \cdot 1_R = 0 のとき ιR=ψ∘π\iota_R = \psi \circ \pi です:

lift_to=ιR∘s=ψ∘π∘s=ψ∘idZ/m=ψ.\texttt{lift\_to} = \iota_R \circ s = \psi \circ \pi \circ s = \psi \circ \mathrm{id}_{\mathbb{Z}/m} = \psi .

二つの法の例では、ℤ/2^32 で 264⋅1=232⋅(232⋅1)=232⋅0=02^{64} \cdot 1 = 2^{32} \cdot (2^{32} \cdot 1) = 2^{32} \cdot 0 = 0 ですが、ℤ/2^64 では 0<232<2640 < 2^{32} < 2^{64} なので 232⋅1≠02^{32} \cdot 1 \neq 0 です。

符号なし型が Semiring で止まる理由

UInt、UInt16、UInt64 は回り込む自然数として読まれます。Nat は非負の代表元を約束し、それらを使うコードは値を個数やサイズとして扱います。ℕ には加法逆元がないので、環ではなく半環です:

1+x=0 in N  ⟹  0=1+x≥1,1 + x = 0 \text{ in } \mathbb{N} \;\Longrightarrow\; 0 = 1 + x \geq 1,

これは矛盾です。抽象的な環としては符号なし型は ℤ/2^k で、負元 −x=2k−x-x = 2^k - x を持ちます。それを公開すると、環向けに書かれたジェネリックなコードで -1 が黙って 2k−12^k - 1 を意味することになり、Nat という読み方はまさにこの混乱を避けています。また標準ライブラリは符号なし型に Neg を提供しておらず、MoonBit ではこのパッケージが外部の型に外部の trait のインスタンスを追加できないため、ラッパー型なしにはそもそも AddGroup を実装できません。標準写像は全域のままです。UInt での from_integer(-1) は 232−12^{32} - 1、つまり ℤ/2^32 における −1-1 の像です。

trait が互いを参照しない理由

すべての変換は ℤ を経由して分解されます: S -> ℤ -> R。前半は S（Integral）だけに、後半は R（FromInteger）だけに依存するので、二つの型を関係づける trait は必要ありません。FromInteger は総称的な整数ソースではなく BigInt を受け取るため、Integral は循環なしにそれを拡張できます。

体と斜体

Field は乗法が可換な Ring + Inverse + Div です。可換性を述べるメソッドはありませんが、契約の一部です。

定義

斜体（可除環）とは、1≠01 \neq 0 で、すべての a≠0a \neq 0 が両側逆元 aa−1=a−1a=1a a^{-1} = a^{-1} a = 1 を持つ環です。体 とは乗法が可換、ab=baab = ba である斜体です。両者の違いはこの法則だけで、Ring + Inverse + Div のメソッドシグネチャでは区別できません。

体でない斜体の標準的な例は、基底 1,i,j,k1, i, j, k と i2=j2=k2=ijk=−1i^2 = j^2 = k^2 = ijk = -1 を持つハミルトンの四元数 ℍ です。ijk=−1ijk = -1 の右から kk を掛けると ij⋅k2=−kij \cdot k^2 = -k となるので ij=kij = k、同様に ji=−kji = -k です:

ij=k,ji=−k,ij≠ji.ij = k, \qquad ji = -k, \qquad ij \neq ji .

可換性がないと何が壊れるか

どの斜体でも、積の逆元は順序が逆になります:

(ab)(b−1a−1)=a(bb−1)a−1=aa−1=1,so(ab)−1=b−1a−1.(ab)(b^{-1}a^{-1}) = a(bb^{-1})a^{-1} = a a^{-1} = 1, \qquad\text{so}\qquad (ab)^{-1} = b^{-1}a^{-1}.

逆の順序はもう一方の積の逆元 a−1b−1=(ba)−1a^{-1}b^{-1} = (ba)^{-1} であり、逆元をとる操作は単射なので

(ab)−1=a−1b−1  ⟺  (ab)−1=(ba)−1  ⟺  ab=ba.(ab)^{-1} = a^{-1}b^{-1} \iff (ab)^{-1} = (ba)^{-1} \iff ab = ba .

ℍ では (ij)−1=k−1=−k(ij)^{-1} = k^{-1} = -k ですが、i−1j−1=(−i)(−j)=ij=ki^{-1} j^{-1} = (-i)(-j) = ij = k です。除算も同じように曖昧です。ab−1a b^{-1} と b−1ab^{-1} a は一般に異なる元で、Div はそのうち一つしか提供しません。

F : Field で制約されたジェネリックなコードは ab=baab = ba に依存してかまいません。(ab)−1(ab)^{-1} を a−1b−1a^{-1}b^{-1} に書き換える、a/b⋅ca/b \cdot c を ac/bac/b として計算する、計算を減らすために積を並べ替える、などです。Field を実装した非可換な型はコンパイルを通り、そのようなコードから誤った答えを受け取ります。これが trait が可換性を述べる理由であり、体でない斜体がこれを実装してはならない理由です。斜体でも動くジェネリックなコードは Ring + Inverse + Div を要求し、因子の順序を保ちます。

有限の斜体はすべて可換なので、22 ウェダーバーンの小定理（1905）: 有限の斜体は体である。実数上では、フロベニウスの定理（1877）により、有限次元の結合的な可除代数は ℝ、ℂ、ℍ だけです。 この区別が問題になるのは無限の型だけです。

浮動小数点のインスタンス

Float と Double は丸めの範囲で Field を実装します。乗法は厳密に可換で fl(ab)=fl(ba)\mathrm{fl}(ab) = \mathrm{fl}(ba) です。IEEE 754 は正確な積を丸め、正確な積は順序に依存しないからです。結合法則と分配法則は近似的にしか成り立たず、0 には逆元がありません。inv はそこで中断します。

採用しなかった代替案

  • 二引数の変換 trait Into[S, R]: MoonBit の trait には Self しかなく、ℤ を経由する分解があるので不要です。
  • 広い「数」trait: ℤ、ℤ/2^k、近似的な実数、体の違いを隠してしまいますが、それこそジェネリックなコードが尊重すべき違いです。
  • NatHomomorphism と IntegralHomomorphism を変換インターフェースにすること: 固定幅のソースには与えられない準同型を約束していました。非推奨の trait としてのみ残っています。
  • 斜体専用の trait: 同梱の型には不要で、可換性なしで動く必要のあるコードは Ring + Inverse + Div を要求できます。

境界

  • このパッケージは行列、複素数、多項式、解析関数、数値アルゴリズムを定義しません。
  • 正確系と近似系の意味論差を無理に隠しません。
  • コンパイル時に法則を検査しません。Field の可換性を含め、すべての構造 trait の法則は実装者への契約で、hom API の道具でテストします。
  • 任意精度の ℕ はモデル化しません。そのような型は ℤ の商ではないので Integral になれません。

Footnotes

  1. 圏論の言葉では、ℕ は半環の圏の始対象、ℤ は環の圏の始対象です。ℤ は加法モノイド ℕ のグロタンディーク群であり、上で使ったのはこの構成です。 ↩

  2. ウェダーバーンの小定理（1905）: 有限の斜体は体である。実数上では、フロベニウスの定理（1877）により、有限次元の結合的な可除代数は ℝ、ℂ、ℍ だけです。 ↩