Luna Flow
简体中文

luna-generic

本手册记录 Luna-Flow/luna-generic 计划中的 v0.4.0 版本。

概览

luna-generic 为 Luna 项目提供通用代数 trait 与默认数值类型实例。

当前版本的重点有三项：

  • FromNat 与 FromInteger 以目标侧 trait 的形式描述从 ℕ、ℤ 出发的唯一同态。
  • Integral 是 ℤ 或其商 ℤ/2^k，normalize 必须是其典范映射的截面。
  • lift_to 与 Section 把“选取代表元”与同态区分开。

安装

moon add Luna-Flow/luna-generic@0.4.0

然后在你的 moon.pkg 中导入 "Luna-Flow/luna-generic"。本包需要 MoonBit 工具链 0.10 或更新版本（moonc ≥ 0.10）。

页面

本仓库是位于 src 的一个 MoonBit 包，文档中称为 core。它的证书子系统 Hom 与 Section 有自己的页面，称为 hom。

部分教程API设计
core：trait、转换、实例教程API设计
hom：同态与截面教程API设计

导出 Trait

  • AddMonoid, MulMonoid
  • AddGroup, MulGroup
  • Semiring、Ring、Field（可交换：ab=baab = ba）
  • FromNat, FromInteger
  • Integral, Nat
  • Num
  • 已废弃：NatHomomorphism、IntegralHomomorphism

导出操作与默认类型

  • 操作 trait: One, Zero, Inverse, Conjugate
  • 默认数值类型: Int, Int16, Int64, UInt, UInt16, UInt64, BigInt, Float, Double

整数模型

  • Integral 覆盖有符号整数、无符号整数以及 BigInt
  • Nat 涵盖代表元非负的整数类型：UInt、UInt16 与 UInt64
  • 定宽整数是 ℤ/2^k；FromInteger::from_integer 按模 2^k 约化
  • Integral::normalize 以 BigInt 形式选出一个值的代表元，且 from_integer(normalize(x)) == x
  • 无符号整数实例只到 Semiring

转换

  • FromInteger::from_integer 是从 ℤ 出发的典范映射：对 BigInt 精确，对定宽整数取模，对 Float 与 Double 舍入
  • lift_to(x) 提升到代表元后映入目标；它是函数，不是同态
  • NatHomomorphism::from_nat 与 IntegralHomomorphism::from_integral 已废弃，请改用 FromNat、FromInteger 与 lift_to

广义同态

  • Hom[S, A, B]：保持签名 S 的映射证书，只能经由 Hom::postulate（产生证明义务）、典范映射 Hom::from_integer 或推理规则构造
  • Section[S, Q, A]：证明一个提升从商的每个类中恰好选出一个代表元的证书；Section::of_integral 是整数类型的典范截面
  • 签名标签：AddMonoidSig、MulMonoidSig、AddGroupSig、SemiringSig、RingSig
  • 代数字典 Algebra[S, A]、运算 Op[A]、积类型 Prod[A, B]、约化见证 Reduct[S, T]
  • Hom::check / Hom::check_by 以样本测试同态律，支持严格、lax 与近似三种强度
  • 详见 hom API、教程、设计

core 教程基于这些 trait 编写小型泛型算法；core API列出所有导出的 trait 与实例；core 设计说明层级与转换为何如此设计。

  • 初次接触本包：先读 core 教程，再读 hom 教程。
  • 在库中使用：把 core API 与 hom API 放在手边；每个 trait 都列出了实例必须满足的定律。
  • 参与贡献：在修改 trait 或添加推理规则之前，请阅读两份设计页面 core 与 hom。

校验

建议的发布前检查：

moon check
moon test