LSR 016 - Expr 构造与提升规范¶

基本信息¶

LSR 编号 016
标题 Expr 构造与提升规范
作者 Ziyang-Bai
状态草案
类型标准规范
创建日期 08-12-2026
归属项目编译器、标准库、CAS

摘要¶

定义 Lamina 中 Expr 的直接构造、普通值到 Expr 的提升边界、符号函数调用解析和 Expr 降级规则。目标是让 x + 1、sin(x)、max(x, y, 0) 等表达式在类型检查阶段有确定语义。

技术规范¶

1. 范围¶

本规范只定义 Expr 在 Lamina 类型系统和表达式构造阶段的行为。CAS 内部 AST 节点、化简规则、等价判定、求解算法和打印格式不由本规范定义。

Expr 是不可变符号表达式值。Expr 可以表示数字、符号、函数调用、集合、区间和由 LSR-014 定义的运算符表达式 [1]。区间的普通类型与命名构造函数由 LSR-017 定义 [5]。

2. 符号声明¶

sym 声明创建 Expr 类型的符号值。

sym x
sym y, z

sym 声明的名称在当前作用域绑定为 Expr
符号名称必须与声明标识符一致
sym 不创建运行时可变变量
已有同名绑定时，sym 必须按普通声明冲突规则报错

3. 直接构造¶

当表达式的期望类型为 Expr 时，允许从 Lamina 表达式直接构造 Expr。

sym x
let a Expr = x^2 + 1
let b Expr = sin(x) + 1
let c Expr = max(x, 0)

以下表达式可在 Expr 期望上下文中构造符号表达式：

整数、分数和有限小数字面量
sym 产生的符号
Expr 值
使用 LSR-014 运算符组成的表达式 [1]
函数调用
有限集合字面量和标准库区间构造调用
元组，前提是目标 Expr 构造规则支持元组表达式

4. 自动提升¶

Expr 自动提升只在表达式已经处于 Expr 上下文时发生。

sym x
let a = x + 1      # Expr
let b = 1 + 2      # num
let c Expr = 1 + 2 # Expr

自动提升规则：

任一操作数类型为 Expr 时，二元运算结果为 Expr
一元运算作用于 Expr 时，结果为 Expr
目标类型显式为 Expr 时，整个表达式按 Expr 构造
集合目标类型为 set<Expr> 时，元素可提升为 Expr [2]
普通全数值表达式不得因为语法形状自动提升为 Expr

5. 不提升的情况¶

下列情况不得自动提升为 Expr。

let a = 1 + 2
let b = sin(pi / 2)
let c = {1, 2, 3}

没有 Expr 操作数、Expr 期望类型或 sym 参与的普通数值表达式
已解析为普通标准库函数调用且实参不含 Expr 的表达式
bool、text、普通数组、普通矩阵和运行时对象
赋值、模块导入、控制流语句和副作用表达式

6. 函数调用解析¶

函数调用解析必须先执行普通名称解析，再决定是否构造符号函数调用。

解析顺序：

若调用目标解析为普通函数，且实参类型满足该函数签名，则按普通函数调用处理
若调用目标解析为普通函数，但任一实参为 Expr，并且没有可用的普通 Expr 重载，则构造符号函数调用
若调用目标未解析为普通函数，但当前上下文期望 Expr，则构造未解释符号函数调用
若调用目标未解析为普通函数，且当前上下文不期望 Expr，则报未绑定名称错误

sym x
let a = sin(pi / 2) # 普通函数调用
let b = sin(x)      # Expr 符号函数调用
let c Expr = f(x)   # 未解释符号函数调用
let d = f(1)        # 未绑定名称错误

标准库可以为常用数学函数提供 Expr 重载。若存在普通 Expr 重载，调用该重载；若不存在，则按符号函数调用构造，不得静默降级为数值调用。

7. 集合、区间和元组¶

集合、区间和元组在 Expr 上下文中的构造规则如下。

sym x
let roots set<Expr> = {-1, 1}
let domain Expr = std.interval_closed_open(0, 1)
let pair Expr = (x, x + 1)

set<Expr> 期望上下文中，集合元素可逐个提升为 Expr [2]
Expr 期望上下文中，标准库区间构造调用产生区间表达式
(a, b) 始终是元组；开区间写成 std.interval_open(a, b) [5]
含 Expr 端点的区间构造符号区间表达式；普通端点构造 interval<T>
元组是否可作为 Expr 节点由 CAS 支持域决定；不支持时必须报类型错误或不支持错误
无限集合、条件集和全集不由普通集合字面量自动构造

8. 比较与逻辑表达式¶

比较运算作用于 Expr 时，结果为符号关系表达式，不自动降级为 bool。

sym x
let a = x > 0          # Expr
let b = x > 0 and x < 1 # Expr 条件表达式
let c = 1 > 0          # bool

全普通值比较返回 bool
含 Expr 的比较返回 Expr
含 Expr 的 and、or、not 构造符号逻辑表达式
if、while 和 match 守卫需要 bool；传入 Expr 条件必须报类型错误，除非该语法显式允许符号条件

9. 降级与数值求值¶

Expr 不得隐式降级为 num、bool、text 或普通容器。

允许的降级入口必须显式：

代入并求值
evalf 或等价的显式近似求值函数
=== 数学等价判定 [3]
显式模式匹配或 CAS 查询接口

sym x
let expr = x + 1
let a = evalf(substitute(expr, x => 2))

x => 2 是 Binding<Expr, Expr>，其构造规则由 LSR-011 定义 [4]。Binding 本身不执行代入；代入必须通过 substitute 或等价的显式 CAS 接口完成。

变量未绑定、表达式超出支持域或无法证明时，求值接口必须返回错误或不可判定结果；不得把失败结果静默当作 0、false 或空集合。

10. 错误¶

实现至少应区分下列错误：

ExprUnboundName：非 Expr 上下文中调用未绑定函数或变量
ExprTypeMismatch：无法把表达式提升为目标 Expr 形态
ExprUnsupportedNode：CAS 不支持对应表达式节点
ExprAmbiguousSyntax：调用、索引或其他表达式形态仍无法由语法规则消歧
ExprImplicitDowngrade：试图把 Expr 隐式用作普通值

错误名称可以由实现映射到统一错误系统，但语义不得合并成普通内部错误。