LSR 000 - Lamina 核心语言规范（草案）¶

1. 语言定位¶

Lamina 是静态强类型、表达式导向的数学 DSL/脚本语言，支持单位系统、符号运算和局部类型推导。

数学运算采用 Symbolic-First：默认保留精确数值或精确符号表达式，并允许未求值结果。显式调用 approximate 才进入近似求值；已有近似值参与运算时，按第 11 节局部传播。

数学值统一使用基本静态类型 num。整数、有理数、复数、符号式和近似数可以采用不同内部表示，编译器可为已知值选择专门化实现。值约束、量纲和容器形状继续承担各自的检查职责。

一个 .lm 文件就是一个模块。模块可绑定动态库 [1]；普通数学调用遵循本规范的精确语义，原生数值边界按声明显式转换。

2. 核心关键字¶

let , var , const , unit , func , return , in , not , loop , while , break , continue , if , else , sym , import , use , as , and , or , static

3. 运算符总览¶

Lamina 运算符 token、优先级和结合性由 LSR-014 定义 [7]。本节保留核心语言中常用运算符的总览。

3.1 基础算术与优先级¶

算术运算符： + , - , * , / , // , % , ^
优先级（高到低）：
1. ^ （幂运算）
2. * （乘法）, / (除法), % (取余), // (整除)
3. + , -

3.2 逻辑与比较¶

数学关系：==、!=、<、<=、>、>=，构造 num 关系值
广播关系：.==、.!=、.<、.<=、.>、.>=，逐元素构造关系
普通 bool 上的 and、or、not、! 执行布尔逻辑；数学关系上的对应运算构造逻辑表达式
if、while 和守卫位置对关系执行判真；未决沿错误路径传播，普通数字不作真假转换
数学容器的整体相等与逐元素关系分别使用未加点和加点运算符；一般复数或矩阵不具有默认的实数顺序
优先级统一按 LSR-014 [7]：幂高于一元运算，比较高于 and，and 高于 or；比较采用非链式二元形式

3.3 赋值与绑定¶

赋值： =
绑定： let （只读）， var （可变）
符号声明：sym，基本类型为 num，默认表示复数标量
优先级：最低

3.4 矩阵与向量运算符¶

线性代数： * , \ , / , ^
元素广播： .* , ./ , .+ , .- , .^
关系广播： .== , .!= , .< , .<= , .> , .>=
转置： ' （共轭转置）， .' （非共轭转置）
优先级和结合性统一由 LSR-014 [7] 定义；矩阵幂仍须满足方阵和整数指数条件

3.5 集合相关运算符¶

从属： in , not in
子集： subset
并交差： | , & , -
对称差： xor

3.6 函数与流程运算符¶

Lambda 箭头： ->
CAS 替换规则： => （由 LSR-016 [8] 定义）
管道： |>
成员访问： .

let first = value |> transform
let second = value |> combine(extra)

管道分别降级为 transform(value) 与 combine(value, extra)。左操作数先求值一次，其余实参按源码顺序求值。普通方法调用沿用声明的成员解析规则。

3.7 运算符分派与歧义约束¶

运算符	仅适用类型	语义	歧义处理
`/`	`num`	数值除法	若操作数不满足数值或矩阵规则，编译报错
`\`	`matrix`	矩阵左除（解 `A X = B` ）	左值必须可作为系数矩阵，维度不匹配或系统无解时报错
`/`	`matrix`	矩阵右除（解线性系统）	左值必须是矩阵，右值可用于右除，否则报错
`^`	`num` 标量	幂运算	集合对称差使用 `xor`
`^`	`matrix`	矩阵幂（整数指数）	非方阵或非整数指数报错
`xor`	`set`	集合对称差	集合对称差统一使用 `xor`
`==`、`!=`	`num` 及数学容器	构造整体相等或不等关系	结构比较使用 `std.cas.same_structure`；普通布尔、文本、元组等按各自契约比较
`<`、`<=`、`>`、`>=`	满足相应顺序支持域的标量	构造顺序关系	实数顺序须满足实性；矩阵和向量的逐元素顺序使用加点算子
`.*` `./` `.+` `.-` `.^`	`vector` / `matrix` 与标量或同形状容器	元素级广播 / 哈达玛运算	维度不兼容报错
`.==` `.!=` `.<` `.<=` `.>` `.>=`	`vector` / `matrix` 与标量或同形状容器	元素级关系广播	返回同形状 `vector<num>` / `matrix<num>` 关系容器，维度不兼容报错

3.8 一元运算符¶

一元 +、- 保持数学值的基本类型 num。幂先于一元负号结合，因此 -2^2 表示 -(2^2)，(-2)^2 以负数为底数。逻辑非对数学关系构造否定，对普通 bool 取布尔反。

4. 变量、类型与推导¶

4.1 类型系统¶

局部表达式采用自底向上的基本类型推导；声明、调用和 Lambda 可向下提供参数类型、值约束及静态量纲。数学值的内部表示变化不改变基本类型 num。

4.2 局部类型推导规则¶

允许推导：局部 let/var 绑定、for 推导式局部变量
必须显式：函数参数类型、函数返回类型、模块导出符号类型
Lambda 的推导规则由 LSR-006 [4] 定义；元组解构绑定的推导规则由 LSR-012 [3] 定义
基本类型必须确定；值约束和量纲另行校验，不能因暂时无法数值求出数学结果而拒绝合法的未求值表达式

4.3 声明语法¶

变量声明统一 let|var|const name type = expr 或者 let|var|const name = expr 。

let：只读绑定；值语义容器经该绑定及其子路径只读
var：可重新绑定，并可经可写根路径修改值语义容器；其他既有值保持原状
const：编译期只读常量；初始化可以得到精确数值，也可以得到编译期已构造的未求值数学表达式

let a = 10
let pi_val real = 3.1415
let fraction = 3/2
const TAU = 2 * pi

let c = 5/4
let name = "LSR"

var counter = 0
counter = counter + 1

a = 20   # 编译报错

4.4 核心数据类型¶

类型	说明	字面量 / 示例
`num`	精确数、符号式、数学关系和近似值的统一基本数学类型	`42`、`114.514`、`1/2`、`sqrt(2)`、`x^2 + 1`
`array`	编程式数组类型	`[2,5,3]`
`text`	文本	`"i love lamina"`
`bool`	布尔逻辑	`true` , `false`
`set`	无序去重集合	`{1,2,3}`
`(T1, T2)`	固定长度、有序的元组 [3]	`(1, "a")`
`vector`	一维数学值容器（1 索引）	`vec[1,2,3]`
`table`	哈希表（任意可哈希键）	`table{"x" => 1}`
`matrix`	二维数学值容器（1 索引）	`mat[1,2;3,4]`
`rule`	CAS 替换规则 [8]	`x => 2`

num 的源代码标注可以附带下列值约束：

标注	基本类型	值约束
`int`	`num`	整数标量
`frac`	`num`	有理数标量
`real`	`num`	实数标量
`complex`	`num`	复数标量

约束描述数学性质，不指定机器位宽或存储布局。let count int = 3、func f(x real) -> num 和 vector<int> 分别约束绑定值、参数和容器元素，其基本类型仍为 num 或 vector<num>。整数、有理数、实数和复数的包含关系用于证明值约束。

静态可确定的违反须提前诊断；其余在绑定、调用、返回或容器操作要求该约束时校验。确定违反报 DomainError 或 InvalidArgument，仍未决报 Inconclusive。已证明为整数的符号式可以满足 int，但循环、索引或 FFI 取值还要求得到具体值。

函数契约保留参数和返回值的约束及量纲；基本类型相同不免除这些检查。静态重载根据基本类型和参数数量解析，不通过猜测运行期值来选择仅约束不同的重载。函数值兼容性必须满足相应约束契约。

普通有限小数和科学计数法字面量表示其十进制文本的精确值。精确算术、符号构造和显式近似均使用 num；类型语法不再提供独立的 Expr 类型。原生声明中的表示选择及范围规则由 LSR-003 [1] 定义。

4.5 可空类型¶

T? 表示普通值或 null。空值检查使用布尔结果；在 s != null 的真分支或 s == null 的假分支中，绑定收窄为 T，其他路径继续保留可空约束。该规则也适用于 num?，与数学关系构造区分。

var s text? = null

if s != null {
    let value text = s
} else {
    s = "ready"
}

4.6 复合值与修改¶

4.6.1 值语义¶

数组、元组和数学容器按值语义使用。赋值、传参、返回和闭包捕获保留既有值；修改一个绑定不改变其他绑定、嵌套成员或捕获中保存的值。数学表达式本身不可变。

实现可采用复制、共享存储、写时分离或唯一所有权原地更新。规范只约束可观察结果；数学容器不承诺共享地址或对象身份，is 仅用于明确具有引用身份的对象。

4.6.2 赋值与修改¶

var original = table{"x" => 1}
var changed = original
changed["x"] = 9

修改后 original["x"] 保持 1，changed["x"] 为 9。共享存储属于实现优化，不改变上述结果。

4.6.3 参数与返回¶

参数默认只读。函数可创建局部可写值，通过返回值交付修改结果。

func bump(src table[text, int]) -> table[text, int] {
    var result = src
    let value = result["n"]
    if value != null {
        result["n"] = value + 1
    }
    result
}

var original = table{"n" => 0}
let changed = original |> bump

调用后 original 保持原值，changed 保存增加后的值。输入参数、返回值及嵌套容器都遵循同一值语义。

4.6.4 可写路径¶

修改路径须以可写 var 绑定为根，并经可写容器位置到达目标。let、只读参数、只读闭包捕获及元组位置不提供可写子路径。可先将其中的值绑定到局部 var，再修改该局部值。

本规则适用于 array、vector、matrix、table 和 set。原生边界默认只读借用；需要修改时须按 LSR-003 [1] 取得显式独占访问或返回新值，维持其他值不变。

4.7 容器齐次性约束¶

vector 与 matrix 的数学元素基本类型统一为 num；元素采用不同精确或近似表示不使容器产生不同基本类型。

vector<int>、matrix<real> 等写法对每个元素施加值约束
数值容器的元素须具有相同静态量纲和刻度；不同刻度先通过 as 显式转换
线性代数或数值后端还须检查标量支持域、形状及具体数值可用性

use std.math.{sqrt}

let lengths = vec[1<m>, 2<m>, 3<m>]
let exact_values = vec[1, 1/2, sqrt(2)]

lengths 的元素同量纲，exact_values 的元素均为 num。混合长度和速度等异量纲数据时，使用量纲静态可知的元组；动态异量纲表或包装由可选扩展定义。

5. 量纲系统¶

5.1 声明与运算¶

单位通过尖括号 <> 附加于数学值的字面量，或写在 num<m> 等声明中。量纲是数学基本类型上的静态约束；编译器检查量纲代数和加减的一致性，保持数值表示独立。

int<m>、real<m> 等标注同时施加数域和量纲约束，其基本数学类型仍为 num。

let dist = 10<m>
let time = 2<s>
let spd = dist / time

# let error = 5<m> + 2<s>   # Dimensional Mismatch

5.2 显式单位转换¶

单位转换必须使用 as ：

let v = 20<m/s>
let v_kmh = v as <km/h>

5.2.1 用户自定义单位¶

用户可使用 unit 声明新单位，支持两种形式：

抽象基单位： unit U
派生单位： unit V = expr<...>

unit score
unit token

unit km = 1000<m>
unit min = 60<s>
unit N = 1<kg*m/s^2>
unit level = 100<score>

约束：

单位名在当前命名空间内唯一
单位定义要求无环（如 unit a = 2<b> 且 unit b = 3<a> 形成环）
抽象基单位可直接创建；派生单位需可归约到已知单位组合（SI 或抽象基单位）
派生单位必须可归约到已知单位组合（SI 或已声明抽象单位）
定义成功后可参与 as <...> 转换（仅限同量纲）

5.3 底层表示¶

编译期追踪 SI 基维度及用户基单位的量纲指数，并保留转换所需的刻度
无量纲值具有零量纲，乘除分别合并或抵消指数
相同量纲不同刻度通过 as 显式转换；数学关系与等价查询的内部比较按规范尺度无损处理
单位转换和剥离在数值代码生成前降级为数值操作；运行期普通数值无需携带单位标签
未求值数学表达式可保留符号量纲信息，以维护定义性和后续推导；这不要求所有具体数值共享同一种表示
运行期单位字符串和动态物理量包装由可选扩展提供，扩展须明确静态值与动态值的转换，不能从已擦除的裸数值恢复单位

5.4 量纲剥离（to scalar）¶

带量纲值剥离为纯数值的语法与边界由 LSR-008 [6] 定义。

let dist = 10<m>
let raw = dist as num
let raw_keep = dist as scalar

let speed = 20<m/s>
let raw_kmh = (speed as <km/h>) as scalar

规则：

默认剥离到 num 使用 SI 基准量值
as scalar 仅移除量纲标签，不进行数值缩放
若需要特定单位下的纯数值，先做单位转换再剥离
as num<_> 在新规范中非法，必须使用 as num

6. 函数¶

6.1 函数签名¶

函数签名语法为 func name(param Type, ...) -> ReturnType。数学形参和返回标注的基本类型为 num；int、real 等标注保留其值约束。

func kinetic_energy(m num<kg>, v num<m/s>) -> num<J> {
    return 1/2 * m * v^2
}

func second2hour(s num<s>) -> num<h> {
    return s as <h>
}

普通函数按声明检查并执行；约束或控制流未决时给出诊断。已声明的数学求值接口可以返回未求值数学结果，不把任意副作用函数隐式转成符号调用。

6.2 实参绑定与具名实参¶

调用支持位置实参和 name = expr 具名实参。位置实参依声明顺序绑定，具名实参依参数名绑定；位置实参须位于具名实参之前。未知参数名、重复绑定、数量错误和遗漏必需参数均产生诊断。

调用目标和全部实参按源码从左到右各求值一次，再将已得值绑定到参数并检查基本类型、值约束及量纲。参数名是允许具名调用的接口的一部分；通过函数值调用时须保留声明的参数绑定信息。

use std.math.{approximate, sqrt}

let exact = sqrt(2)
let rounded = approximate(exact, precision = 100)

具名实参只选择参数位置，不创建赋值表达式或自动偏应用。标准库存在多个调用形式时，分别按已声明的参数数量解析。

6.3 Lambda 的规范边界¶

Lambda 的语法、类型推导、捕获和管道交互由 LSR-006 [4] 定义。

7. 控制流与推导式¶

7.1 条件执行与 if 表达式¶

if 条件接受普通 bool 或 num 数学关系。条件位置对关系执行判真，结论为真或假时选择对应路径，仍未决时报 Inconclusive。普通数字不作真假转换。语句位置可以省略 else；条件为假时继续后续语句。

if residual > tolerance {
    raise("残差超过容差")
}

在赋值、函数实参、返回值或函数尾表达式位置，if 用于产生值，必须包含 else。正常返回分支须具有可统一的基本类型；数学分支统一为 num，并校验目标值约束及量纲。终止分支按 LSR-018 [9] 的底类型规则参与统一。分支只执行一次，不把未决条件或分支副作用隐式转为符号分段式。

let abs_val = if x < 0 {
    -x
} else {
    x
}

7.2 loop 定次循环¶

loop { ... } 是无界循环；loop count { ... } 是定次循环。次数须能求值为非负整数。

import std

var counter = 0
loop 3 {
    counter = counter + 1
}

loop {
    std.println(counter)
    break
}

规则：

次数在进入循环前求值一次，零次不执行循环体
静态已知的负数或非整数次数须提前报错；动态值进入循环前校验，次数仍未决时报 Inconclusive
continue 完成本次迭代并进入下一次计数，不能跳过计数推进
break 立即结束当前循环；正常定次循环的循环体最多进入指定次数

7.3 while 条件循环¶

while cond { ... } 在 cond 为 true 时重复执行循环体。

var i = 0
while i < 5 {
    i = i + 1
}

规则：

每轮迭代前重新计算 cond
cond 接受普通 bool 或可判真的数学关系；未决和非条件值按第 7.1 节诊断
支持 break 与 continue

7.4 for 迭代与推导式¶

迭代： for 名字 in 可迭代对象 {...}

可迭代对象提供 begin()、next(iterator) 和 end() 协议。遍历对象在进入循环时求值一次，游标与结束位置先比较，再读取当前元素；空序列不读取元素。continue 须推进到下一元素，break 立即结束。

import std

let values = vec[2, 4, 32, 5, 6]
for value in values {
    std.println(value)
}

推导式语法： 表达式 for 变量 in 可迭代对象 if 守卫条件

# 向量推导
let squares = vec[x^2 for x in range(1, 10) if x % 2 == 0]

# 集合推导
let abs_set = {abs(x) for x in vec[-1, 1, 2, -2]}

# 矩阵推导
let M = mat[i * j for i in range(1,3); for j in range(1,3)]

规则：

推导式内部为独立词法作用域
外部变量只读捕获，局部可写副本的修改不回写外部值
遍历对象单次求值；守卫按第 7.1 节判真，未决不能当作假

8. 向量与矩阵计算¶

8.1 定义、拼接与索引¶

let A = mat[1,2,3;4,5,6;7,8,9]
let v = vec[1,2,3]

let horizontal = mat[A, A]
let vertical = mat[A; A]
let element = A[2,3]

mat 构造中的块按逗号横向、分号纵向拼接，须满足对应维度。普通 [A, A] 保持数组语义。向量和矩阵的索引从 1 开始，索引须为具体可求值整数并在有效范围内。

8.2 切片¶

let row2 = A[2,*]
let col3 = A[*,3]
let submat = A[1..2,2..3]

* 在切片位置选择整轴，.. 在下标中表示包含两个端点的索引范围；相关端点须能求值为有效整数索引。切片保留容器类型和量纲，并遵循值语义。

8.3 算术与关系广播定义¶

标准线性代数算子： * , \ , / , ^
元素广播算子： .* , ./ , .+ , .- , .^
关系广播算子： .== , .!= , .< , .<= , .> , .>=
\ 与 / 分别定义为左除与右除： A \ B 解 A X = B ， B / A 解 X A = B
矩阵与标量分派依据容器结构和运算支持域；未知数学值可保留未求值运算，实际数值操作仍须检查形状和数域
==、!= 构造数学容器的整体关系；顺序比较只支持声明的标量顺序，逐元素关系使用加点算子

let X = A \ B
let Y = B / A

let shifted = A .+ 10
let elementwise = A .* A
let product = A * A
let flags = vec[1,2,3] .> 1

矩阵乘法检查内维度；flags 是逐元素数学关系组成的 vector<num>，每项可在条件位置判真。

8.4 常用操作¶

dot(v1, v2)      # 点积
cross(v1, v2)    # 叉积（3维）
norm(v)          # 范数
v1 .+ v2         # 逐元素加法
v .* 2           # 标量广播
matmul(A, v)     # 矩阵-向量乘
matmul(A, B)     # 矩阵-矩阵乘
inv(A)           # 逆矩阵
det(A)           # 行列式

9. 集合与逻辑¶

运算符	含义	示例
`in` / `not in`	元素从属	`2 in {1,2,3}`
`subset`	子集关系	`{1,2} subset {1,2,3}`
`\|` , `&` , `-` , `xor`	并、交、差、对称差	`{1,2} xor {2,3}`

有限 set<T> 的成员查找与子集查询按 LSR-013 的结构元素身份返回 bool，去重不调用有限数学证明。实区间的成员判断构造 num 关系，按 LSR-017 在条件位置判真；两类容器不混用成员契约。

预定义数学常量： pi , e , phi

整数、有理数、实数和复数的全集使用显式的 CAS 集合表示；Z、Q、R、C 在数域说明中作为数学记号。普通花括号仍构造有限集合，不以特殊元素名隐式改为全集。

10. 数域与值约束¶

整数、有理数、实数和复数的数学包含关系为 Z ⊂ Q ⊂ R ⊂ C。这些数域用于值约束和假设，不构成不同基本静态类型。

默认数学运算保持精确，1/2 是有理数，0.5 是同一精确数值的十进制写法。超出已实现精确求值能力时保留数学调用或表达式；确定无定义时沿数学错误路径传播。

use std.math.{sqrt}

let rational = 2 + 1/2
let decimal = 1/2 + 0.5
let radical = sqrt(2)
let imaginary = 2.0 + 3I

sym x
let polynomial = 5/2 + x

以上数学结果的基本类型均为 num。编译器可分别采用整数、有理数、代数数或符号结构表示；容器同样不按这些表示差别拆分数学元素类型。

sym 默认复数标量；实性、正性、整数性须来自已知值、约束或显式假设。复数主值约定由 LSR-010 定义；一般复数不使用实数顺序。

11. 数学值与显式近似¶

数学值的构造、结构操作和求值由 LSR-016 [8] 定义。精确数和符号式共享基本类型 num，未解释函数须显式声明或构造，名称拼写错误按普通解析规则诊断。

默认求值保留原定义域。x/x、0*(1/x) 等变换需要相关非零性和定义性前提；显式形式代数操作按其声明的数学支持域执行。

use std.cas.{substitute}
use std.math.{approximate, sqrt}

sym x
let polynomial = x^2 + 1
let value = substitute(polynomial, x => 3)
let exact = sqrt(2)
let rounded = approximate(exact, precision = 100)

precision 是目标十进制有效位数，须为正整数。成功近似按请求精度计算，误差估计、认证误差界和正确舍入保证均为可选扩展；核心不把目标工作精度等同于结果已证明正确的位数。

近似操作数触发局部近似传播，采用参与近似值的最高工作精度，精确子项按需要数值化；尚未绑定的符号部分可以保留。提高工作精度只影响后续计算，不能恢复既有输入已丢失的信息。表示值、近似类别和工作精度须按数学值语义保留，不能仅凭格式化文本把结果冒充为原式的精确值。

关系判真和等价查询均比较现有表示值。精确与近似混合比较须无损进行，不先舍入到共同精度；容差比较使用独立接口。结论描述现有值，不追溯到近似前的原表达式。

12. 相等性语义¶

数学值及数学容器的 ==、!= 构造整体关系，结果的基本类型为 num
std.cas.same_structure 返回 bool，按语义结构递归比较；精确数叶按数值，近似节点保留其近似类别、表示值和工作精度区别，内部存储布局不参与比较
=== 和 std.cas.equivalent 返回 std.cas.Equivalence 的 Equivalent、Different 或 Unknown，按 LSR-007 [5] 执行有限证明
bool、text、规则、固定状态及普通元组等按自身契约提供布尔相等；元组中的数学值递归使用结构比较
集合去重、哈希和模式匹配使用稳定的内部结构相等；Unknown 不是不等价结论，证明预算不影响结构键
is 只观察具有明确引用身份的对象；数学值与值语义容器不依赖共享地址

import std.cas

sym x
let relation = x + x == 2*x
let structural = cas.same_structure(x + x, 2*x)
let proof = (x + x) === 2*x

relation 是数学关系，structural 是布尔结构查询，proof 是三态证明结果。条件位置可对关系判真；证明状态须按固定状态值显式处理。

13. 序列与模块系统¶

13.1 序列生成¶

func square(x num) -> num {
    return x^2
}

let values = range(1,10)
let squares = values |> map(square)

range 是独立的整数序列接口，参数和元素具有整数值约束；数学区间始终表示实数集合。管道把左侧插入第一个实参，不要求 map(square) 自身先产生偏应用闭包。

13.2 命名空间与模块¶

import ：加载模块并绑定模块对象；标准库模块导入见 [2]。 use ：从模块导入符号到当前作用域（冲突时报错）。

import std.math
import physics.quantum

let val = math.sin(math.pi / 2)

use std.math.{sin, cos, pi, e}
use std.linalg.{det}

let wave = sin(pi * x) + cos(e * x)
let D = det(matrix_A)

use std.constants.{G as GRAVITY}