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`` 类型的符号值。

.. code-block:: text

   sym x
   sym y, z


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

3. 直接构造
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

.. code-block:: text

   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`` 上下文时发生。

.. code-block:: text

   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``。

.. code-block:: text

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


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

6. 函数调用解析
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


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

解析顺序：

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

.. code-block:: text

   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`` 上下文中的构造规则如下。

.. code-block:: text

   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``。

.. code-block:: text

   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 查询接口

.. code-block:: text

   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`` 隐式用作普通值

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

11. 引用
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

.. [1] :doc:`LSR-014 - 运算符规范 <LSR-014>` - 定义运算符 token、优先级、集合、区间和显式乘法
.. [2] :doc:`LSR-013 - 集合类型规范 <LSR-013>` - 定义集合类型、多结果返回和 ``set<Expr>`` 元素提升
.. [3] :doc:`LSR-007 - 数学等价判定规范 <LSR-007>` - 定义 ``Expr`` 上的 ``===`` 判定语义
.. [4] :doc:`LSR-011 - 代数数据类型规范 <LSR-011>` - 定义 ``Binding`` ADT 与表达式位置的 ``=>``
.. [5] :doc:`LSR-017 - 区间类型规范 <LSR-017>` - 定义区间构造函数、类型统一和符号区间边界