hom 教程

Hom[S, A, B] 是一个映射 A -> B，它让 S 列出的运算保持一致：转换一个和，等于各项转换后再求和，依此类推。本页演示如何声明、检验和组合它们。为什么这样设计见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 中是正数。这样的转换用 Section 而不是 Hom 来描述。它同时记录了回去的路，并检验去了再回来能得到原来的值：

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 中。其他大多数同态并不唯一：一个类型可以有多个到自身的保结构映射，例如复数上的恒等映射与复共轭。把这样的映射写成显式的 Hom 值，而不要写成 trait 实例，这样选择在调用处始终可见。

常见陷阱

从 BigInt 转成数值类型时使用 Hom::from_integer；它对所有输入成立。
用 Section::of_integral 检查从机器整数出发的转换，只需要值时用 lift_to。不要把 Int -> Int64 这样的扩宽包进 Hom::postulate：它不是同态。
check 的样本要包含边界值，例如 0、1、负数，以及定宽类型接近溢出的值。
用 <= 或容差检查的映射在复合时仍被当作精确映射。请再次检查复合结果。
二元运算的检查会测试样本的每一对，所以几十个样本就意味着数千次求值。

下一步

hom API 列出了每个构造器、规则和检查。
hom 设计证明了截面保持什么，以及为什么到 ℤ 的提升不可能是同态。
core 教程介绍了内置签名所依据的 trait。