Luna Flow
简体中文

hom API

作用

hom 子系统提供广义同态：一个 Hom[S, A, B] 是一个映射 A -> B，并带有“保持签名 S 中所有运算”的证书。Section[S, Q, A] 证明一个提升从商的每个类中恰好选出一个代表元。两种证书在本包外都无法伪造。未经证明的叶子是 Hom::postulate、Section::postulate，以及典范的 Hom::from_integer 与 Section::of_integral，后两者的义务落在 trait 实例上。

源码：src/hom.mbt、src/section.mbt。数学内容见 hom 设计。

本页示例假定有如下声明：

using @luna-generic {
  type Hom,
  type Section,
  type Algebra,
  type Op,
  type Prod,
  type Reduct,
  type AddMonoidSig,
  type MulMonoidSig,
  type AddGroupSig,
  type SemiringSig,
  type RingSig,
  semiring_to_add_monoid,
  semiring_to_mul_monoid,
  ring_to_semiring,
  ring_to_add_group,
  add_group_to_add_monoid,
}

let ints : Array[Int] = [0, 1, -1, 7, 2147483647, -2147483648]

let longs : Array[Int64] = [0L, 1L, -1L, 7L, 4294967296L, 9223372036854775807L]

签名标签

签名标签是空枚举，只在类型层出现，作为 Hom、Section、Algebra 与 Reduct 的参数 S。用户可以定义自己的标签。

AddMonoidSig

AddMonoidSig 是签名 0、+。

pub enum AddMonoidSig {
}

MulMonoidSig

MulMonoidSig 是签名 1、*。

pub enum MulMonoidSig {
}

AddGroupSig

AddGroupSig 是签名 0、+、neg。

pub enum AddGroupSig {
}

SemiringSig

SemiringSig 是签名 0、1、+、*。

pub enum SemiringSig {
}

RingSig

RingSig 是签名 0、1、+、*、neg。

pub enum RingSig {
}

代数字典

同一个 S 的两个字典必须按相同顺序列出相同的运算（名字与元数一致），否则 Algebra::prod 与 Hom::check_by 会 abort。

证书假定每个载体上只有一个 S-代数：同一载体上、同一 S 的所有字典必须以相同方式解释运算。then 经由中间载体复合，因此若中间载体上有两个不同的 Algebra::make 字典，复合得到的映射对哪一个都不保持。

Op

Op[A] 是单类别签名中的一个运算。

pub(all) struct Op[A] {
  name : String
  arity : Int
  eval : (Array[A]) -> A
}

arity == 0 表示常量。eval 恰好接收 arity 个参数。

Algebra

Algebra[S, A] 是签名 S 在载体 A 上的一种解释：按签名规定的顺序排列的一组 Op[A]。

pub struct Algebra[S, A] {
  // private fields
}

Algebra::make

Algebra::make(ops) 为自定义签名标签构造字典。

pub fn[S, A] Algebra::make(Array[Op[A]]) -> Algebra[S, A]

如上所述，每个标签与载体只保留一个字典。

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] } },
  ])
}

Algebra::add_monoid, Algebra::mul_monoid, Algebra::add_group, Algebra::semiring, Algebra::ring

这些函数从 A 的结构 trait 实例导出内置标签的字典。

pub fn[A : AddMonoid] Algebra::add_monoid() -> Algebra[AddMonoidSig, A]
pub fn[A : MulMonoid] Algebra::mul_monoid() -> Algebra[MulMonoidSig, A]
pub fn[A : AddGroup] Algebra::add_group() -> Algebra[AddGroupSig, A]
pub fn[A : Semiring] Algebra::semiring() -> Algebra[SemiringSig, A]
pub fn[A : Ring] Algebra::ring() -> Algebra[RingSig, A]

运算按标签的顺序列出：例如 RingSig 为 0、1、+、*、neg。trait 一致性保证每个标签与载体只有一个字典。

test "built-in dictionaries" {
  let int_ring : Algebra[RingSig, Int] = Algebra::ring()
  let id : Hom[RingSig, Int, Int] = Hom::id()
  assert_true(id.check(int_ring, int_ring, ints))
}

Algebra::prod

Algebra::prod(a, b) 是 Prod[A, B] 上逐分量的积代数。

pub fn[S, A, B] Algebra::prod(Algebra[S, A], Algebra[S, B]) -> Algebra[S, Prod[A, B]]

每个运算用 a 作用于 fst，用 b 作用于 snd。当 a 与 b 列出的运算不同时中止。

积类型

Prod

Prod[A, B] 是带有字段 fst 与 snd 的二元积载体。

pub(all) struct Prod[A, B] {
  fst : A
  snd : B
} derive(Eq, @debug.Debug)

运算逐分量进行。Prod 实现 Add、Mul、Neg、Sub、Zero 与 One；当两个分量都实现时，它也实现 AddMonoid、MulMonoid、AddGroup、Semiring 与 Ring。

Prod::add, Prod::sub, Prod::mul, Prod::neg, Prod::zero, Prod::one

这些方法是逐分量运算，也可以通过 +、-、*、一元 - 以及 Zero / One trait 使用。

pub fn[A : Add, B : Add] Prod::add(Prod[A, B], Prod[A, B]) -> Prod[A, B]
pub fn[A : Sub, B : Sub] Prod::sub(Prod[A, B], Prod[A, B]) -> Prod[A, B]
pub fn[A : Mul, B : Mul] Prod::mul(Prod[A, B], Prod[A, B]) -> Prod[A, B]
pub fn[A : Neg, B : Neg] Prod::neg(Prod[A, B]) -> Prod[A, B]
pub fn[A : Zero, B : Zero] Prod::zero() -> Prod[A, B]
pub fn[A : One, B : One] Prod::one() -> Prod[A, B]
(a,b)+(a′,b′)=(a+a′,b+b′),(a,b)(a′,b′)=(aa′,bb′),0=(0,0),1=(1,1).(a, b) + (a', b') = (a + a', b + b'), \qquad (a, b)(a', b') = (aa', bb'), \qquad 0 = (0, 0), \qquad 1 = (1, 1).

Prod::equal, Prod::not_equal, Prod::to_repr

这些方法逐分量比较并为调试渲染 Prod；新代码中请使用 ==、!= 与 inspect。

pub fn[A : Eq, B : Eq] Prod::equal(Prod[A, B], Prod[A, B]) -> Bool
pub fn[A : Eq, B : Eq] Prod::not_equal(Prod[A, B], Prod[A, B]) -> Bool
pub fn[A : @debug.Debug, B : @debug.Debug] Prod::to_repr(Prod[A, B]) -> @debug.Repr
test "prod" {
  let p : Prod[Int, Double] = { fst: 2, snd: 0.5 }
  let q : Prod[Int, Double] = { fst: 3, snd: 4.0 }
  assert_eq(p * q + Prod::one(), { fst: 7, snd: 3.0 })
  assert_true(p != q)
}

同态

Hom

Hom[S, A, B] 是带证书的映射 A -> B，证书表明它保持 S 的每个运算。

pub struct Hom[S, A, B] {
  // private fields
}

该证书的含义是：对 S 中每个元数为 nn 的运算 ω\omega 以及所有 x1,…,xnx_1, \dots, x_n，

f(ωA(x1,…,xn))=ωB(f(x1),…,f(xn)).f(\omega_A(x_1, \dots, x_n)) = \omega_B(f(x_1), \dots, f(x_n)).

只有本包能构造 Hom 值。叶子是 Hom::postulate 与 Hom::from_integer；其他所有构造器都是推理规则。

Hom::postulate

Hom::postulate(f) 不加证明地把 f 当作 S-同态，并产生一个证明义务。

pub fn[S, A, B] Hom::postulate((A) -> B) -> Hom[S, A, B]

调用者承诺：对 S 的每个运算 op 与所有参数 xs，有 f(op_A(xs)) == op_B(xs.map(f))。即使该映射只用宽松或容差关系检查，这一承诺始终是严格相等。每次调用都应配一个 check 测试。

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

test "postulate and check" {
  assert_true(int64_to_int().check(Algebra::ring(), Algebra::ring(), longs))
}

Hom::apply

h.apply(x) 应用底层映射。

pub fn[S, A, B] Hom::apply(Hom[S, A, B], A) -> B
test "apply" {
  inspect(int64_to_int().apply(4294967301L), content="5")
}

Hom::id

Hom::id() 是恒等同态。

pub fn[S, A] Hom::id() -> Hom[S, A, A]

Hom::then

h.then(g) 是复合：先 h，后 g。

pub fn[S, A, B, C] Hom::then(Hom[S, A, B], Hom[S, B, C]) -> Hom[S, A, C]

若 ff 与 gg 保持 ω\omega，则 g∘fg \circ f 也保持：

g(f(ω(x)))=g(ω(f(x)))=ω(g(f(x))).g(f(\omega(x))) = g(\omega(f(x))) = \omega(g(f(x))).

Hom::forget

h.forget(r) 沿 Reduct[S, T] 见证遗忘结构。

pub fn[S, T, A, B] Hom::forget(Hom[S, A, B], Reduct[S, T]) -> Hom[T, A, B]

保持 S 每个运算的映射也保持更小签名 T 的运算。

Hom::pair, Hom::fst, Hom::snd

Hom::pair(f, g) 把 x 映为 { fst: f(x), snd: g(x) }；Hom::fst() 与 Hom::snd() 是从 Prod 出发的投影。

pub fn[S, A, B, C] Hom::pair(Hom[S, A, B], Hom[S, A, C]) -> Hom[S, A, Prod[B, C]]
pub fn[S, A, B] Hom::fst() -> Hom[S, Prod[A, B], A]
pub fn[S, A, B] Hom::snd() -> Hom[S, Prod[A, B], B]

它们满足 pair(f, g).then(fst()) = f 与 pair(f, g).then(snd()) = g。

test "composition rules" {
  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)
  let back = p.then(Hom::fst())
  let additive = h.forget(ring_to_add_group)
  inspect(back.apply(4294967301L), content="5")
  assert_true(additive.check(Algebra::add_group(), Algebra::add_group(), longs))
}

Hom::to_add_group

h.to_add_group() 把群之间的加法幺半群同态升级为加法群同态。

pub fn[A : AddGroup, B : AddGroup] Hom::to_add_group(Hom[AddMonoidSig, A, B]) -> Hom[AddGroupSig, A, B]

没有新的义务：f(−x)+f(x)=f(−x+x)=f(0)=0f(-x) + f(x) = f(-x + x) = f(0) = 0，所以 f(−x)=−f(x)f(-x) = -f(x)。

Hom::to_ring

h.to_ring() 把环之间的半环同态升级为环同态。

pub fn[A : Ring, B : Ring] Hom::to_ring(Hom[SemiringSig, A, B]) -> Hom[RingSig, A, B]

没有新的义务，计算与 to_add_group 相同。

Hom::from_integer

Hom::from_integer() 是 FromInteger 给出的典范映射 ℤ → R，以证书形式提供。

pub fn[R : FromInteger] Hom::from_integer() -> Hom[SemiringSig, @bigint.BigInt, R]

它对每个输入都成立；当 R 是环时用 to_ring 升级。Float 与 Double 目标只在舍入意义下满足它。对定宽源，先用 Section::of_integral 提升。

test "from_integer" {
  let h : Hom[RingSig, BigInt, Int] = Hom::from_integer().to_ring()
  let samples = [0, 1, -1, 2147483647].map(BigInt::from_int)
  assert_true(h.check(Algebra::ring(), Algebra::ring(), samples))
}

截面

截面沿同态 proj : A -> Q 把商 Q 提升回 A，满足 proj(lift(q)) == q。提升本身不是同态，但它在 proj 的核的意义下保持每个运算，并且当结果本身是代表元时严格保持。

截面律会拒绝离开参数所在类的提升，但不规定选哪个代表元：[0, 2^32) 与 [-2^31, 2^31) 都是 BigInt -> Int 的截面，只有后者保持有符号序。

Section

Section[S, Q, A] 沿投影 proj : A -> Q 把商 Q 提升回 A。

pub struct Section[S, Q, A] {
  // private fields
}
π(s(q))=qfor every q∈Q.\pi(s(q)) = q \quad \text{for every } q \in Q.

Section::postulate

Section::postulate(proj, lift) 把 lift 当作 proj 的截面加以信任，并产生一个证明义务。

pub fn[S, Q, A] Section::postulate(Hom[S, A, Q], (Q) -> A) -> Section[S, Q, A]

调用者承诺对每个 q 有 proj.apply(lift(q)) == q；proj 自带其 Hom 义务。

test "section postulate" {
  let truncate : Hom[RingSig, Int64, Int] = Hom::postulate(x => x.to_int())
  let widen = Section::postulate(truncate, x => x.to_int64())
  assert_true(widen.check(ints))
}

Section::of_integral

Section::of_integral() 是整数类型的典范截面。

pub fn[Z : Integral] Section::of_integral() -> Section[SemiringSig, Z, @bigint.BigInt]

proj 为 FromInteger::from_integer，lift 为 Integral::normalize。义务落在这些实例上。当 Z 是环时使用 to_ring。

Section::lift, Section::proj

s.lift(q) 是 q 的选定代表元；s.proj() 是到商的投影。

pub fn[S, Q, A] Section::lift(Section[S, Q, A], Q) -> A
pub fn[S, Q, A] Section::proj(Section[S, Q, A]) -> Hom[S, A, Q]

Section::normalize

s.normalize(a) 即 lift(proj(a))，a 的范式。

pub fn[S, Q, A] Section::normalize(Section[S, Q, A], A) -> A

两个值同余当且仅当它们的范式相等。

Section::is_representative

s.is_representative(a) 判断 a 是否为其类的选定代表元，即 normalize(a) == a。

pub fn[S, Q, A : Eq] Section::is_representative(Section[S, Q, A], A) -> Bool

在这样的结果上，提升与 A 的运算完全一致。

test "representatives" {
  let s : Section[RingSig, Int, BigInt] = Section::of_integral().to_ring()
  let big = BigInt::from_int64(4294967296L)
  inspect(s.lift(-1), content="-1")
  inspect(s.proj().apply(big + BigInt::from_int(5)), content="5")
  inspect(s.normalize(big + BigInt::from_int(5)), content="5")
  assert_true(s.is_representative(s.lift(7) + s.lift(1)))
  assert_false(s.is_representative(s.lift(2147483647) + s.lift(1)))
}

Section::then

s.then(next) 先用 s 把 Q 提升到 A，再用 next 把 A 提升到 B。

pub fn[S, Q, A, B] Section::then(Section[S, Q, A], Section[S, A, B]) -> Section[S, Q, B]

投影是先 next.proj 后 s.proj。没有新的义务：设 s,ts, t 为两个提升、πs,πt\pi_s, \pi_t 为它们的投影，则 πs(πt(t(s(q))))=πs(s(q))=q\pi_s(\pi_t(t(s(q)))) = \pi_s(s(q)) = q。

Section::forget, Section::to_add_group, Section::to_ring

这些推理规则改变投影的签名；提升保持不变。

pub fn[S, T, Q, A] Section::forget(Section[S, Q, A], Reduct[S, T]) -> Section[T, Q, A]
pub fn[Q : AddGroup, A : AddGroup] Section::to_add_group(Section[AddMonoidSig, Q, A]) -> Section[AddGroupSig, Q, A]
pub fn[Q : Ring, A : Ring] Section::to_ring(Section[SemiringSig, Q, A]) -> Section[RingSig, Q, A]

它们沿用 Hom::forget、Hom::to_add_group 与 Hom::to_ring。

Section::check

s.check(samples) 在每个样本上测试截面定律 proj(lift(q)) == q。

pub fn[S, Q : Eq, A] Section::check(Section[S, Q, A], Array[Q]) -> Bool

Section::check_ops

s.check_ops(quotient, cover, samples) 对每个运算、在由 samples 组成的所有元组上测试 proj(op_A(xs.map(lift))) == op_Q(xs)。

pub fn[S, Q : Eq, A] Section::check_ops(Section[S, Q, A], Algebra[S, Q], Algebra[S, A], Array[Q]) -> Bool

这把 proj 作为代表元上的同态来检验。当两个字典列出的运算不同时中止。

test "section checks" {
  let s : Section[RingSig, Int, BigInt] = Section::of_integral().to_ring()
  assert_true(s.check(ints))
  assert_true(s.check_ops(Algebra::ring(), Algebra::ring(), ints))
}

lift_to(x) 把整数值提升后映入任意 FromInteger 目标，不发放证书；它列在 core API 中。

约化见证

Reduct

Reduct[S, T] 见证每个 S-结构也是 T-结构，因此 S-同态也是 T-同态。

pub struct Reduct[S, T] {
  // private fields
}

Reduct 只能由本包构造。

semiring_to_add_monoid, semiring_to_mul_monoid, ring_to_semiring, ring_to_add_group, add_group_to_add_monoid

这些常量是内置签名之间的包含关系。

pub let semiring_to_add_monoid : Reduct[SemiringSig, AddMonoidSig]
pub let semiring_to_mul_monoid : Reduct[SemiringSig, MulMonoidSig]
pub let ring_to_semiring : Reduct[RingSig, SemiringSig]
pub let ring_to_add_group : Reduct[RingSig, AddGroupSig]
pub let add_group_to_add_monoid : Reduct[AddGroupSig, AddMonoidSig]

Reduct::refl, Reduct::then

Reduct::refl() 是 S 到自身的平凡包含；r.then(r2) 复合包含关系。

pub fn[S] Reduct::refl() -> Reduct[S, S]
pub fn[S, T, U] Reduct::then(Reduct[S, T], Reduct[T, U]) -> Reduct[S, U]
test "reducts" {
  let r : Reduct[RingSig, AddMonoidSig] = ring_to_add_group.then(add_group_to_add_monoid)
  let h = int64_to_int().forget(r)
  assert_true(h.check(Algebra::add_monoid(), Algebra::add_monoid(), longs))
}

定律检查

Hom::check

h.check(src, dst, samples) 在 S 的每个运算上以精确相等测试同态定律。

pub fn[S, A, B : Eq] Hom::check(Hom[S, A, B], Algebra[S, A], Algebra[S, B], Array[A]) -> Bool

要求 B : Eq。它就是以 == 为关系的 check_by。

Hom::check_by

h.check_by(src, dst, samples, rel) 对每个运算、在由 samples 组成的所有元组上测试 rel(f(op_A(xs)), op_B(f(xs)))。

pub fn[S, A, B] Hom::check_by(Hom[S, A, B], Algebra[S, A], Algebra[S, B], Array[A], (B, B) -> Bool) -> Bool

rel 决定保持的强度：严格同态用相等，次可加映射等宽松同态用 <=，映到浮点目标的近似同态用容差。元数为 n 的运算在 samples.length()^n 个元组上测试。当 src 与 dst 列出的运算不同时中止。

test "check_by" {
  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))
  assert_false(abs.check(Algebra::add_monoid(), Algebra::add_monoid(), samples))
}

语义说明

  • 定宽整数源类型（Int、Int64、UInt 等）是 ℤ/2^k，而不是整数环。从它们到 BigInt 不存在半环同态，因此提升到 ℤ 是截面而不是同态。同样的论证排除了 Int -> Int64 这类拓宽，而 Int64 -> Int 这类截断是环同态。
  • 推理规则按严格同态来复合证书。只满足松弛（<=）或容差定律的映射，复合之后必须重新检验。
  • Float 与 Double 目标只在舍入误差内满足同态律，应使用 check_by 加容差。参见 core API 的嵌入说明。

已弃用

Hom::from_nat

Hom::from_nat() 为 NatHomomorphism::from_nat 发放证书。

#deprecated
pub fn[N : Nat, R : NatHomomorphism] Hom::from_nat() -> Hom[SemiringSig, N, R]

对定宽源它不是同态。替代方案：Hom::from_integer 配合 Section::of_integral，不需要证书时用 lift_to。

Hom::from_integral

Hom::from_integral() 为 IntegralHomomorphism::from_integral 发放证书。

#deprecated
pub fn[Z : Integral, R : IntegralHomomorphism] Hom::from_integral() -> Hom[SemiringSig, Z, R]

因同样的理由弃用，替代方案相同。