LSR 013 - 集合类型规范

基本信息

  • LSR 编号 013

  • 标题 集合类型规范

  • 作者 Ziyang-Bai

  • 状态 草案

  • 类型 标准规范

  • 创建日期 08-09-2026

  • 归属项目 编译器、标准库、CAS

摘要

定义 Lamina 集合类型。集合表示有限、无序、去重、同构的值集合；可用于数学表达、CAS 多结果返回和标准库容器。

技术规范

1. 范围

本规范定义有限集合 set<T>。实区间使用 interval<num> [5]；无限集合、条件集、全集和带重数集合由对应的 CAS 或标准库规范定义专门表示。

集合用于无序、去重的同构结果；元组按固定位置区分多个结果，支持同构与异构的元素组合 [4]。需要顺序或重数的结果使用向量，或由具体接口定义包含值与重数的组合。

2. 集合类型

集合类型写作 set<T> [1]。

sym x
let a set<int> = {1, 2, 3}
let b set<num> = {x, x + 1}

  • set<T> 表示元素类型为 T 的集合

  • 集合元素必须具有确定的结构相等语义，不要求其 == 返回 bool

  • 集合不保证迭代顺序

  • 集合中不存在重复元素

  • 集合值默认不可变

  • set<int> 中的 int 是元素值约束，基本类型为 set<num>；set<frac>、set<real>、set<complex> 同理，不建立按数域分裂的基本集合类型

  • 约束参与赋值、调用和返回校验；静态可证时提前检查，其余运行期验证。确定违反时报 DomainError 或 InvalidArgument，未决时报 Inconclusive；不能仅凭约束选择同基本签名的重载

  • 集合采用值语义；仅可通过允许修改的 var 根路径更新集合，其他绑定、元组元素和只读捕获保留旧值。共享、复制和唯一所有权优化不影响该语义，is 不用于观察集合存储身份

3. 集合字面量

集合字面量使用花括号。

let ints = {1, 2, 3}
let nums = {1, 1/2, 3}
let empty set<num> = {}

  • 非空集合按元素类型统一推导 set<T>

  • 空集合必须由上下文推出元素类型，否则需要显式类型标注

  • 无法统一元素类型时报错

  • 集合字面量中的结构重复元素只保留一个；表达式按源码顺序各求值一次，去重不省略副作用求值

4. 元素类型统一

集合元素必须统一为单一元素类型。

  • 精确数、符号表达式、关系和近似值的基本类型均为 num，混合后得到 set<num>，不发生整数到有理数或符号专用类型的提升

  • int、frac、real、complex 约束只限制元素值；不得按内部小整数、大整数、有理数或 AST 表示分裂集合类型

  • text、bool、rule、元组和其他结构类型仍保留自身类型；不能与 num 无条件统一

  • 不具备确定结构相等语义的类型不得作为集合元素；若不能统一元素类型或没有所需结构比较规则，必须报错

5. 集合运算

运算

说明

示例

in / not in

元素从属

2 in {1,2,3}

subset

子集判断

{1,2} subset {1,2,3}

|

并集

{1,2} | {2,3}

&

交集

{1,2} & {2,3}

-

差集

{1,2} - {2}

xor

对称差

{1,2} xor {2,3}

  • |、&、-、xor 的两个操作数必须是集合，元素类型必须相同或可统一，结果为统一后的 set<T>

  • in / not in 的右侧必须是集合，左侧元素类型必须可与右侧集合元素类型统一，结果为 bool

  • subset 的两个操作数必须是集合，元素类型必须相同或可统一，结果为 bool

  • 本规范有限集合的从属、子集、交并差和去重均按第 6 节的结构规则识别元素；不隐式进行数学等价证明。数学上等价但结构不同的元素可以同时存在

6. 集合相等

集合的数学相等关系与容器结构查询是不同操作。

let relation = {1, 2, 3} == {3, 2, 1}
let identical = std.cas.same_structure({1, 2, 3}, {3, 2, 1})

  • 集合的整体 == 和 != 构造基本类型为 num 的数学关系，不返回容器去重所需的布尔比较结果；已知数字集合的关系可判真，但关系类型仍为 num

  • 关系的两个集合元素类型必须相同或可统一；数学相等忽略元素顺序。条件位置自动判真，证明未决时报 Inconclusive

  • std.cas.same_structure 对集合的重载返回 bool，忽略迭代顺序，要求包含相同的结构元素；示例中 identical 为 true

  • 内部去重、哈希键、从属及匹配直接递归使用同一结构规则，不调用构造关系的 ==，不调用 ===、std.cas.equivalent 或有限预算证明

  • num 的精确数字叶按数值比较，不依赖内部整数或有理数表示；符号表达式按语义结构比较，不能因尚未证明不同就归并

  • 近似节点按当前表示值、近似类别、目标工作精度等语义结构区分，并与精确叶区别；不得把显示小数精确化后作为原元素的结构键，全局证明预算不参与结构键

  • rule 按 LSR-016 [7] 定义的左右 num 结构比较；元组按 LSR-012 [4] 逐位置递归比较，内部数学值不使用关系构造操作

  • 基于哈希的实现必须使哈希与上述结构相等一致，不能由存储地址或遍历顺序决定去重

  • 某一 CAS 操作若明确承诺按数学等价归并，须自行使用 LSR-007 [6] 的固定三态结果处理；只有 cas.Equivalent 可作为已证明等价，cas.Unknown 不表示不同，也不改变本集合类型的结构去重规则

7. 集合推导式

集合推导式产生集合值。

let squares = { x^2 for x in {1, 2, 3} }

  • 推导式结果元素按表达式类型统一

  • 推导式输入必须可迭代

  • 集合推导式结果按第 6 节的结构规则自动去重

  • 集合推导式不得产生无限集合

8. 多结果返回

Lamina 函数返回单个值。多个同类数学结果按无序、去重的集合语义组织时，返回类型为 set<T> [2]。

func roots(expr num, var num) -> set<num>
func solve(eq num, var num) -> set<num>

  • 按固定位置区分的结果使用元组，支持同构与异构的元素组合

  • 需要排序或保留重复值的结果使用向量；需要显式重数时，由接口定义值与重数的组合

  • 普通数学函数直接返回结果值；类型冲突、操作超出支持域及求值失败沿 LSR-018 [3] 的错误传播规则处理

CAS 中有限可枚举的解集使用 set<num>，复数根遵循 LSR-010 [8]；两个接口还须检查各自要求的表达式、关系和求解变量等支持域，不是所有 num 都是合法输入。

sym x
let rs = roots(x^2 - 1, x)    # {-1, 1}

  • 求解接口证明解集为空时，返回空 set<num> 作为正常结果

  • 求解接口必须在当前算法与预算内确认完整解集后返回结果；完整性处于待定状态时，诊断 SetResultInconclusive 并沿错误路径传播

  • 若结果有定义域条件，条件表达由调用的具体标准库规范定义

9. 有限性

set<T> 表示有限集合；可结构比较的元组可作为集合元素 [4]。

  • 实区间使用 interval<num>，整数端点不使区间成为有限整数枚举；条件集和全集等数学对象应由 CAS 或标准库定义专门表示 [5]

  • CAS 在确认结果有限且枚举完整后返回 set<T>；未决求解状态沿错误路径传播，不返回伪装为完整解集的部分集合

10. 诊断

  • SetElementTypeMismatch：集合元素类型统一失败

  • SetOperandTypeMismatch：集合运算的操作数类型校验失败

  • 元素类型必须具备结构相等语义，校验失败时必须诊断；基于哈希的实现还须满足该类型的结构哈希契约

  • SetResultInconclusive：完整解集判定处于待定状态

错误名称可映射到 LSR-018 [3] 的统一诊断与故障传播机制。

11. 引用