hom 設計

目標

MoonBit の現在の型システムの中で構造を保つ写像を表現し、型システムが証明できない法則を開発者に委ねつつ、その義務を監査可能かつ検査可能に保つこと。

制約

MoonBit の trait は Self しか引数を持たず、多引数 trait も関連型もないため、準同型 A -> B を trait として書けません。
ℕ と ℤ からの準同型は一意（始対象）なので、FromNat と FromInteger は対象側の trait として置けます。それ以外の準同型は一般に一意ではなく、値として扱う必要があります。

中核となる設計判断

LCF 流の証明書: Hom[S, A, B] のフィールドは非公開で、このパッケージの中でのみ構築されます。
公開された信頼の入口は Hom::postulate だけです。カーネルの規則はパッケージ内部の trust を使うため、postulate を検索すると利用者側の義務だけが正確に列挙されます。（assume は MoonBit の予約語のため使いません。）Section::postulate は切断の信頼の入口であり、標準の Hom::from_integer と Section::of_integral はもう一方の葉で、その義務は trait インスタンスにあります。
商から被覆代数へ戻る持ち上げは Hom ではなく Section です。射影を Hom として持ち、proj(lift(q)) == q だけを約束します。代表元上で演算と一致することはこの法則から従います。両者を分けることで、Int -> BigInt のような代表元の持ち上げが準同型であるかのように合成されるのを防ぎます。
シグネチャは証明書の幽霊型 S として現れ、代数は辞書値 Algebra[S, A] として渡されます。証明書は何を保つかを述べ、辞書は検査に使われます。
シグネチャ間の包含は、このパッケージだけが作れる Reduct[S, T] の証人で表します。
保存の強さは検査時に選ぶ関係 rel で決まり、厳密・lax・近似の準同型が一つの API を共有します。

切断

hom チュートリアルでは、この数学に触れずに Section を使います。

定義

π : A -> Q を全射準同型とします（例: 簡約 BigInt -> Int）。切断とは、すべての q について π(s(q)) = q を満たす写像 s : Q -> A で、各類 π⁻¹(q) から元を一つ選びます。第一同型定理により Q は商 A / ker π なので、切断とは商代数の代表元の選び方のことです。

切断が保存するもの

すべての演算 ω と引数 x について:

s(ω(x)) と ω(s(x)) は ker π を法として合同です。両方に π を適用すると、切断の法則により π(s(ω(x))) = ω(x)、π が準同型なので π(ω(s(x))) = ω(π(s(x))) = ω(x) です。
s(ω(x)) = ω(s(x)) となるのは、ω(s(x)) が s の像に含まれるとき、かつそのときに限ります。ω(s(x)) = s(y) なら、同じ計算により y = π(s(y)) = π(ω(s(x))) = ω(x) なので ω(s(x)) = s(ω(x)) です。逆に s(ω(x)) は常に像に含まれます。

同じ二段階を数式で書きます。 $n$ 項演算 $\omega$ と $x = (x_1, \dots, x_n)$ について、 $s(x) = (s(x_1), \dots, s(x_n))$ とします:

\begin{aligned} \pi\bigl(s(\omega_Q(x))\bigr) &= \omega_Q(x) && \text{section law} \\ \pi\bigl(\omega_A(s(x))\bigr) &= \omega_Q(\pi(s(x))) = \omega_Q(x) && \pi \text{ is a homomorphism} \end{aligned}

したがって $A$ に減法があれば $s(\omega_Q(x)) - \omega_A(s(x)) \in \ker \pi$ です。ある $y$ について $\omega_A(s(x)) = s(y)$ なら、 $\pi$ を適用して $y = \omega_Q(x)$ 、よって $\omega_A(s(x)) = s(\omega_Q(x))$ です。

したがって Section::check は切断の法則だけを検査し、check_ops は持ち上げた引数の上で π が準同型であることを検査します。第 2 点はそこから従います。Int では s の像は [-2^31, 2^31) であり、「結果が像に含まれる」とは「結果が回り込んでいない」ということです。

桁上がり

Int の加算では、第 1 点の差は s(a) + s(b) - s(a + b) = c(a, b)·2^32 で、c(a, b) ∈ {-1, 0, 1} は桁上がりです。s(a) + s(b) + s(e) を二通りに展開すると次を得ます

c(a, b) + c(a + b, e) = c(b, e) + c(a, b + e)

この恒等式は結合法則から来ます。 $m = 2^{32}$ 、 $s(a) + s(b) = s(a + b) + c(a, b)\,m$ と書き、三つの持ち上げの和を二通りにまとめます:

\begin{aligned} (s(a) + s(b)) + s(e) &= s(a + b) + s(e) + c(a, b)\,m \\ &= s(a + b + e) + \bigl(c(a + b, e) + c(a, b)\bigr)\,m, \\ s(a) + (s(b) + s(e)) &= s(a) + s(b + e) + c(b, e)\,m \\ &= s(a + b + e) + \bigl(c(a, b + e) + c(b, e)\bigr)\,m . \end{aligned}

両辺は ℤ で等しいので、 $m$ の係数は一致します。 $c$ の範囲は代表元の範囲から従います。 $s(a) + s(b) \in [-2^{32}, 2^{32} - 2]$ 、 $s(a + b) \in [-2^{31}, 2^{31})$ なので、 $c(a, b)\,m$ は $-3 \cdot 2^{31}$ と $3 \cdot 2^{31}$ の間に厳密に収まり、 $c(a, b) \in \{-1, 0, 1\}$ です。

したがって c は 2-コサイクルで、ℤ を ℤ/2^32 の 2^32ℤ による拡大として記述します。ℤ には有限位数の元がないのでこの拡大は分裂せず、どう代表元を選んでも s は準同型になりません。直接示すと、加法的な切断 $\sigma : \mathbb{Z}/m \to \mathbb{Z}$ があれば $m\,\sigma(1) = \sigma(m \cdot 1) = \sigma(0) = 0$ となり $\sigma(1) = 0$ ですが、これは $\pi(\sigma(1)) = 1$ に矛盾します。乗法では、ずれは積の上位ワードです。

正規形

n = s ∘ π : A -> A は正規形です: n(n(a)) = n(a)、a と n(a) は合同、そして a と b が合同であることと n(a) = n(b) は同値です。商の演算は代表元の上で s(ω_Q(x)) = n(ω_A(s(x))) として計算されます。つまり A で計算してから正規化します。回り込む Int の演算は A = ℤ の場合のこの計算です。Section::normalize は s と π から構成されるので、合同な二つの値に異なる正規形を与えることはありません。

`Section` が `Hom` ではない理由

切断は単射であり、その像の上では演算と一致するため、準同型と取り違えて合成してしまいがちです。別の証明書に分けることで違いが型に現れます: Section は π を Hom として持ち、π(s(q)) = q だけを約束します。

法則はどの代表元を選ぶかを決めません。[0, 2^32) と [-2^31, 2^31) はどちらも BigInt -> Int の切断を与えますが、Int の符号付きの順序を保つのは後者だけです。このような性質は別途検査が必要です。

採用しなかった代替案

型が実装する準同型 trait Hom[A, B]: 二つの型パラメータが必要ですが MoonBit の trait にはありません。また型の組ごとに準同型を一つしか許しませんが、組には普通いくつもあります。たとえば複素数上の恒等写像と共役です。
証明書のない普通の関数 (A) -> B: 検査済みの準同型と任意の変換を区別できず、合成しても責務の出所が記録されません。
Int -> BigInt のような代表元の持ち上げを準同型として扱うこと: 上のコサイクルの議論からそうではないとわかるので、専用の証明書 Section を持ちます。
検査の関係（厳密、緩い、許容誤差）を型に記録すること: 推論規則が強さごとに増えてしまいます。代わりに関係は検査時に選び、その代償は下の境界で述べます。

境界

単一ソートのシグネチャのみを扱います。加群（スカラーとベクトル）のような多ソート構造はこのサブシステムの範囲外です。
高階カインドがないため、関手的な持ち上げ（多項式、行列など）はそれぞれのパッケージが提供し、ここでは一般化しません。
法則は証明されず、検査されるだけです。証明書が保証するのは由来の追跡可能性であり、法則が成り立つことではありません。
then の健全性は、台集合ごとに S-代数が一つだけであることに依存します。組み込みのタグは trait の一貫性によってこれを満たしますが、Algebra::make の辞書は規約によるだけです。
証明書は check_by で使った関係を記録しないため、lax な写像や近似的な写像も厳密な準同型であるかのように合成されます。
固定幅の整数は ℤ や ℕ ではなく ℤ/2^k です。そこから ℤ への写像は切断なので、演算と一致するのは回り込みが起きない間だけです。
切断の法則はどの代表元を選ぶかを決めないため、順序の保存のような性質は別途検査する必要があります。