LSR 017 - 区间类型规范¶

基本信息¶

LSR 编号 017
标题区间类型规范
作者 Ziyang-Bai
状态草案
类型标准规范
创建日期 08-21-2026
归属项目编译器、标准库、CAS

摘要¶

定义 Lamina 的实区间类型 interval<num>、四个标准库构造函数、端点开闭性、成员判断和符号端点语义。区间通过普通函数调用构造，元组和数组继续使用各自的字面量语法。

技术规范¶

1. 区间类型¶

interval<num> 表示由下界、上界和两个端点的开闭标志组成的有界实数集合。

let closed_domain interval<num> = std.interval_closed(0, 1)
let domain interval<num> = std.interval_open_closed(0, 1)

端点的基本静态类型统一为 num，并须满足实标量值约束；小整数、大整数、有理数、近似值和符号表达式是内部表示差别，不决定成员域
区间默认包含边界之间的实数，而不是仅包含与端点表示相同的值；整数端点不会产生 interval<int>，例如 1/2 属于 closed_domain
int、frac、real、complex 是值约束，不是不同的基本数学类型；不由端点的这些约束或底层表示推断整数成员域
带量纲端点须具有相同的静态维度，并在比较前换算到统一尺度；区间保留该静态量纲要求，运行期裸数不能恢复已擦除的量纲
复数不具有无条件实数顺序；确定非实或不属于标量支持域的端点不能用于构造本区间
区间遵循值语义，保留构造时的端点值和开闭标志；后续修改端点来源绑定不改变既有区间，不规定可观察的共享存储身份

2. 构造函数¶

std 模块提供四个区间构造函数。

函数	含义
`std.interval_closed(a, b)`	闭区间，包含两个端点
`std.interval_open(a, b)`	开区间，不包含两个端点
`std.interval_closed_open(a, b)`	包含下界，不包含上界
`std.interval_open_closed(a, b)`	不包含下界，包含上界

无量纲端点的四个构造函数具有下列签名：

func interval_closed(lower real, upper real) -> interval<num>
func interval_open(lower real, upper real) -> interval<num>
func interval_closed_open(lower real, upper real) -> interval<num>
func interval_open_closed(lower real, upper real) -> interval<num>

real 是 num 的实标量值约束，参数基本类型均为 num。带量纲形式使用同维度实标量端点，按相同规则构造区间，不因量纲产生数值表示类型或按值重载。

两个端点表达式按源码从左到右各求值一次，先按普通调用规则绑定再检查。实性和量纲静态可证时提前检查，其余运行期验证；确定违反约束时报 DomainError 或 InvalidArgument，实性仍未决时报 Inconclusive。实端点之间的未知顺序则按第 4 节保留，不等同于实性校验失败。

3. 表面语法¶

区间构造采用普通的限定名函数调用语法 [1]。

源码	语法含义
`(a, b)`	二元素元组 [2]
`[a, b]`	二元素数组
`f(a, b)`	两实参函数调用
`std.interval_open(a, b)`	开区间构造函数调用

interval_closed、interval_open、interval_closed_open 和 interval_open_closed 是 std 模块的标准导出名。通过 use std.{interval_closed, interval_open, interval_closed_open, interval_open_closed} 导入后可以省略 std. 前缀。

4. 边界与空区间¶

下界小于上界时，区间按构造函数指定的开闭性确定成员
下界等于上界且由 interval_closed 构造时，区间只包含该端点
下界等于上界且至少一端开放时，区间为空
下界大于上界时，区间为空，不报倒置边界错误，也不自动交换端点
上下界顺序或相等性未决时，保留端点及开闭标志形成符号区间；代入或假设补充后继续按同一规则判断，不能把未决当成倒置或空集

空区间保留 interval<num> 类型和相应静态量纲。边界判定比较各数值当前的数学表示值；精确与近似混合时不先舍入、不引入容差，结论不追溯到近似之前的原式。

5. 成员判断¶

in 和 not in 判断值是否位于区间内。

let half = (1/2) in std.interval_closed(0, 1)
let excluded = 0 in std.interval_open_closed(0, 1)
let reversed = std.interval_closed(1, 0)

左操作数须为 num 标量并满足区间的实性和静态量纲要求；确定不相容时沿错误路径传播
闭端点使用包含相等的比较，开端点使用严格比较；实数成员域不受端点或待判断值的内部表示影响
普通端点和符号端点采用同一数学值语义，in 和 not in 构造基本类型为 num 的成员关系；示例中 half 可判为真，excluded 可判为假，reversed 为空
已确定为空的区间不包含任何满足成员输入约束的值；未知端点顺序或未知比较保留在关系中
条件位置按核心规则自动判真；结论仍未决时报 Inconclusive，不能将未知关系转成 false，也不能将普通数字作真假转换

6. 相等性与哈希¶

区间是数学集合，整体 == 和 != 构造基本类型为 num 的数学关系；std.cas.same_structure 的区间重载才是返回 bool 的显式结构查询。

数学相等比较区间表示的实数集合；确定为空的两个区间表示同一集合，不要求其原始端点结构相同。关系在条件位置自动判真，仍未决时报 Inconclusive
静态量纲、端点值结构和两个开闭标志均相同时，两个区间结构相同；类型兼容性仍须先校验
结构查询和内部哈希匹配对端点直接使用与 std.cas.same_structure 一致的递归比较，不调用会构造关系的相等运算，也不进行有限预算等价证明
精确数字叶按数值比较，不依赖内部表示；近似端点保留表示值、近似类别和工作精度等结构区别，并与精确叶区别
哈希须与结构比较一致；全局证明预算不参与键，存储地址不能作为数学端点或区间的身份
结构不同的区间仍可能表示同一实数集合，例如不同倒置边界产生的空区间；不能把结构不相同误当成已证明集合不同

7. 与序列和集合的关系¶

类型或函数	语义
`interval<num>`	由实数端点限定的实数集合，不隐含整数步进
`range(start, end)` [3]	独立的整数步进序列，按接口检查整数约束及具体可求值性
`set<T>` [4]	有限、已枚举、无序且去重的值集合

8. 符号端点¶

含符号端点的区间仍为 interval<num>，不提升为另一符号类型 [5]。构造函数只接收明确绑定的值，期望数学参数不会使未绑定的名字自动成为符号。

func segment(x real) -> interval<num> {
    return std.interval_closed_open(0, x)
}

let numeric = std.interval_closed(0, 1)

segment 的参数基本类型为 num；已证明为实数的符号式可以满足 real 约束，无需先具体求值
sym 默认声明复数标量；用于实区间端点前须通过假设或约束满足实性，不能仅因写在端点位置就隐式变为实数
未知顺序保留在同一类型的区间值中；代入后若下界大于上界即为空，同端点依开闭性判断
符号区间成员关系与数字区间成员关系具有同一基本类型 num；只有具体使用位置要求确定真值时才必须判定

9. 诊断¶

实现至少区分下列错误：

IntervalArityMismatch：构造函数的端点数量错误
IntervalBoundTypeMismatch：端点类型无法统一
IntervalBoundNotOrdered：端点确定不满足实标量支持域或所需量纲条件
Inconclusive：端点实性或需要确定真值的成员判断仍未决；仅边界顺序未决不使构造失败
IntervalMembershipTypeMismatch：待判断值与区间的标量或量纲要求不兼容

错误名称可以映射到实现的统一诊断系统。

10. 语法迁移¶

原区间写法	标准构造函数
`[a, b]`	`std.interval_closed(a, b)`
`(a, b)`	`std.interval_open(a, b)`
`[a, b)`	`std.interval_closed_open(a, b)`
`(a, b]`	`std.interval_open_closed(a, b)`