hom チュートリアル

Hom[S, A, B] は、S が列挙する演算を整合させる写像 A -> B です。和を変換したものは変換したものの和になる、といった具合です。このページでは宣言、検査、組み合わせ方を示します。この設計の理由はhom 設計にあります。

クイックスタート

Hom は luna-generic に含まれています。core チュートリアルのとおりにパッケージをインストールしてインポートしてください。このページの例は次の宣言を使います:

using @luna-generic {
  type Hom,
  type Section,
  type Algebra,
  type Op,
  type AddMonoidSig,
  type SemiringSig,
  type RingSig,
  ring_to_add_group,
  lift_to,
}

最小の実用的なプログラムは、準同型を一つ宣言して検査します:

fn int64_to_int() -> Hom[RingSig, Int64, Int] {
  Hom::postulate(x => x.to_int())
}

test "quick start" {
  let samples = [0L, 1L, -1L, 7L, 2147483647L, 4294967296L, 9223372036854775807L]
  assert_true(int64_to_int().check(Algebra::ring(), Algebra::ring(), samples))
  inspect(int64_to_int().apply(4294967301L), content="5")
}

日常的なタスク

葉の準同型: `postulate` 一つにつき検査を一つ

上のように Int64 を Int に切り詰めると、値が回り込んでも + と * の整合性が保たれるので、極端なサンプルでも検査に通ります。Int を Int64 に広げるとそうはなりません。2147483647 + 1 は Int では回り込みますが Int64 では回り込まないので、サンプルの和があふれた時点で検査は失敗します。

test "widening is not a homomorphism" {
  let widen : Hom[RingSig, Int, Int64] = Hom::postulate(x => x.to_int64())
  let samples = [0, 1, -1, 2147483647]
  assert_false(widen.check(Algebra::ring(), Algebra::ring(), samples))
}

Hom::postulate はすべてあなたが行う約束です。リポジトリで postulate を検索すればすべて列挙され、それぞれに対応する check テストを置くべきです。

小さな準同型から組み立てる

test "composition" {
  let h = int64_to_int()
  let low : Hom[RingSig, Int64, Int16] = Hom::postulate(x => Int16::from_int(x.to_int()))
  let p = Hom::pair(h, low) // Int64 -> Prod[Int, Int16]
  let back = p.then(Hom::fst()) // same as h
  let additive = h.forget(ring_to_add_group)
  inspect(p.apply(65537L).snd, content="1")
  inspect(back.apply(4294967301L), content="5")
  inspect(additive.apply(-1L), content="-1")
}

合成、忘却、対の構成、射影、昇格は新しい約束を生みません。これらはすべての証明書を正確なものとして扱うため、以下の <= や許容誤差付きの検査しか通らない写像は、合成後に改めて検査する必要があります。

準同型ではない変換を検査する

Int を BigInt に変換すると値はすべて保たれますが、回り込む演算は保たれません。2147483647 + 1 は Int では負、BigInt では正です。このような変換は Hom ではなく Section で記述します。Section は戻り道も記録し、行って戻ると元の値になることを検査します:

test "section" {
  let s : Section[RingSig, Int, BigInt] = Section::of_integral().to_ring()
  let samples = [0, 1, -1, 2147483647, -2147483648]
  assert_true(s.check(samples))
  assert_true(s.check_ops(Algebra::ring(), Algebra::ring(), samples))
}

値を変えてしまう変換（符号を落とすものや Float を経由して丸めるものなど）は check に失敗します。

s.is_representative(b) は、ある BigInt がこの変換で得られる値かどうかを判定します。結果がそのような値であるとき、変換後の演算は元の演算と正確に一致します:

test "representatives" {
  let s : Section[RingSig, Int, BigInt] = Section::of_integral().to_ring()
  inspect(s.is_representative(s.lift(7) + s.lift(1)), content="true") // no wrap-around
  inspect(s.is_representative(s.lift(2147483647) + s.lift(1)), content="false") // Int wrapped
}

証明書が不要なら、lift_to で任意の FromInteger 対象に変換できます:

test "lift_to" {
  let x : Double = lift_to(-7)
  inspect(x, content="-7")
}

保存の強さを選ぶ

test "lax homomorphism" {
  let abs : Hom[AddMonoidSig, Double, Double] = Hom::postulate(x => x.abs())
  let samples = [0.0, 1.5, -2.0, 3.25]
  // |x + y| <= |x| + |y|: subadditive, a lax homomorphism
  assert_true(abs.check_by(Algebra::add_monoid(), Algebra::add_monoid(), samples, (l, r) => l <= r))
}

浮動小数点の対象には許容誤差を使います。結果に対する相対誤差は非負の入力に適しています。符号付きの入力では x + y が打ち消し合って小さくなる一方、丸め誤差は |x| + |y| に比例したままです:

test "approximate homomorphism" {
  let h : Hom[SemiringSig, BigInt, Float] = Hom::from_integer()
  let close = (l : Float, r : Float) => {
    (l - r).abs() <= (1.0e-6 : Float) * ((1.0 : Float) + r.abs())
  }
  let samples = [0, 1, 3, 1000, 16777217].map(BigInt::from_int)
  assert_true(h.check_by(Algebra::semiring(), Algebra::semiring(), samples, close))
  assert_false(h.check(Algebra::semiring(), Algebra::semiring(), samples))
}

16777217 は $2^{24} + 1$ で、Float が保持できない最初の整数なので、厳密な検査は失敗し、許容誤差の検査は通ります。

さらに進んで

独自シグネチャ

enum MaxSig {}

fn max_int() -> Algebra[MaxSig, Int] {
  Algebra::make([
    Op::{ name: "max", arity: 2, eval: xs => if xs[0] > xs[1] { xs[0] } else { xs[1] } },
  ])
}

test "custom signature" {
  // doubling is monotone, so it preserves max (as long as it does not wrap)
  let double : Hom[MaxSig, Int, Int] = Hom::postulate(x => 2 * x)
  assert_true(double.check(max_int(), max_int(), [-5, 0, 3, 1000]))
}

両側の辞書が同じ演算を同じ順序で並べていれば、Hom と check は台集合が一つの任意のシグネチャで使えます。タグと台集合ごとに辞書は一つにします。同じタグの異なる意味に対して検査した証明書は合成できません。

型で決まらない写像

ℤ からの標準写像は一意なので FromInteger trait に置かれています。ほかの準同型のほとんどは一意ではありません。型は自分自身への構造を保つ写像を複数持てます。たとえば複素数上の恒等写像と複素共役です。そのような写像は trait インスタンスではなく明示的な Hom の値として書き、選択が呼び出し箇所で見えるようにしてください。

よくある落とし穴

BigInt から数値型への変換には Hom::from_integer を使います。すべての入力で成り立ちます。
機械整数からの変換の検査には Section::of_integral を、値だけが必要なら lift_to を使います。Int -> Int64 のような拡大を Hom::postulate で包まないでください。準同型ではありません。
check のサンプルには境界値を含めます: 0、1、負数、固定幅型ではオーバーフローに近い値。
<= や許容誤差で検査した写像も、合成では厳密なものとして扱われます。合成結果を再度検査してください。
二項演算の検査はサンプルのすべての組をテストするので、数十個のサンプルでも数千回の評価になります。

次のステップ

hom API にはすべての構成子、規則、検査が載っています。
hom 設計では、切断が保存するものと、ℤ への持ち上げが準同型になりえない理由を証明しています。
core チュートリアルでは、組み込みシグネチャの元になっている trait を扱います。