LSR 016 - 数学值与符号操作规范

基本信息

• LSR 编号 016

• 标题 数学值与符号操作规范

• 作者 Ziyang-Bai

• 状态 草案

• 类型 标准规范

• 创建日期 08-12-2026

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

摘要

定义统一数学基本类型 num 的值构造、符号声明、显式符号函数，以及 std.cas 的结构查询、替换规则、数学结构匹配和重写。精确数、符号表达式、关系和近似值使用同一基本类型；函数调用、容器和错误仍遵循各自的普通静态规则。

技术规范

1. 范围与数学值

num 表示数学值，包括精确整数、有理数、复数、符号、未求值数学调用、关系和带精度的近似值。实现可使用小整数、大整数、有理数、AST 或多精度数等不同内部表示，但表示差异不创建用户可见的独立基本数学类型。

数学运算默认精确、保域（Symbolic-First）。即使所有操作数都是具体数，支持域内尚不能精确完成的运算也可以保留未求值式，例如精确 sin(1)；不能因没有 sym 参与而强制近似。确定无定义的运算仍报数学错误 [1] [6]。

bool、text、rule、array、table、tuple 及数学容器保留其结构类型。vector<num>、matrix<num>、set<num> 的元素使用统一数学类型，不能把整个容器或元组隐式变成标量 num。区间使用 LSR-017 规定的 interval<num> [4]。

int、frac、real、complex 是 num 上的值约束。例如 x int、-> real、vector<int> 分别约束参数、返回值、容器元素；基本类型仍为 num 或 vector<num>。约束参与调用和返回校验，但不引入按值自动重载：基本签名及参数个数相同的函数不能仅靠约束静态分派。

函数类型兼容必须保留参数值约束及量纲契约，不能只因基本类型同为 num 而放宽受约束参数；数学集合等容器的元素约束同理。

2. 符号声明

sym 声明创建基本类型为 num 的符号值。

sym x
sym y, z

• 名称在当前作用域绑定为数学符号，其符号名称与声明标识符一致

• sym 默认声明复数标量；实性、正性和整数性由假设或值约束提供 [7]

• sym 不创建运行时可变变量；已有同名绑定时按普通声明冲突规则报错

• 已证明为整数的符号式可满足 int 约束，但循环、索引、FFI 等需要具体整数的操作还须能够具体求值

3. 直接构造与精确运算

数学字面量、符号以及已声明数学函数的结果直接构造 num，无需期望符号类型或自动提升阶段。

use std.math.{sin, max}

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

本规范支持的构造包括：

• 整数、分数和有限小数字面量，默认表示精确数

• sym 声明的符号及已有 num 值

• LSR-014 中适用于数学值的算术、关系和逻辑运算 [1]

• 已声明数学函数按其签名与支持域构造的结果或未求值调用

a 至 e 的基本类型均为 num。值已精确算出还是保留符号，不影响基本静态类型。内部保留不可变数学结构；普通算术构造可进行保域规范化，但不得借此删除未证明有定义的子式。

4. 普通值与数学值的边界

• bool 和 text 不因上下文期望 num 而隐式变成数学表达式

• => 的结果为 rule；=== 的结果为固定状态 std.cas.Equivalence [3]

• 赋值、模块导入、控制流和普通副作用调用不是可自动封装的数学节点

• is 只适用于明确提供引用同一性的对象；num 和数学容器不提供可观察对象身份

• as 是核心语言定义的显式转换；不得通过转换恢复已擦除的单位或近似输入精度

• 容器采用值语义。实现可共享存储或复制；仅 var 根路径提供可写子路径，不能通过元组、let 或只读闭包绕过值语义

• FFI 浮点声明是显式数值边界，返回带 ABI 工作精度的近似数学值；普通精确数学函数不得因隐藏的 FFI 调用而自动失去精确性

5. 数学函数与普通调用

调用必须先执行普通名称解析、参数绑定和类型检查，不因结果期望为 num 而跳过检查。

1. 目标必须解析为已声明的普通函数或显式构造的符号函数

2. 所有实参按源码顺序各求值一次，按普通调用规则绑定后检查类型、值约束和参数个数

3. 已声明数学函数在其支持域内默认精确执行；精确结果暂不可求时，可保留该数学调用及其参数

4. 普通函数仍执行函数体；副作用不会因为实参含符号而被隐式延迟或符号化

5. 未绑定名称、错误参数个数和不匹配类型按普通调用规则报错，不回退为未解释调用

值约束静态可证时提前检查，否则运行期验证；确定违反时报 DomainError 或 InvalidArgument，仍未决时报 Inconclusive。已声明数学接口的未知结果可以是未求值式，这不同于绕过该接口要求的参数约束。

use std.math.{sin}

sym x
let a num = sin(1)
let b num = sin(x)

两个调用使用同一个数学接口。a 可以保留精确调用，b 可以保留含符号的调用；均不自动转为近似值，也不要求另一套符号重载。

6. 显式符号函数

std.cas 提供：

func symbolic_function(name text, arity int) -> func

arity 为可具体求值的非负整数，int 是值约束。返回的函数值具有固定参数个数，每个参数及返回值的基本类型均为 num；其名称和参数个数是符号函数结构的一部分。调用时按普通规则检查参数个数和类型，然后构造未解释数学调用，不执行用户副作用。

import std.cas

sym x
let f = cas.symbolic_function("f", 1)
let pair = cas.symbolic_function("pair", 2)
let a num = f(x)
let b num = pair(x, 1)

没有上述声明或其他普通绑定时，f(x) 即使出现在 let a num = ... 中也必须报未绑定名称错误。显式符号函数与普通函数不能仅因显示名称相同而混淆；结构比较还应区分调用目标及其已声明的参数个数。

CAS 代入、匹配和重写是立即执行的普通接口，不自动变成未求值调用。它们与 LSR-018 的终止函数一样遵循普通实参检查和错误传播 [5]。

7. 集合、区间和元组

import std

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

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

let pair = (x, x + 1)

• 集合仍是 set<num>，不提升为标量；无限集合、条件集和全集不由有限集合字面量自动构造 [2]

• 普通和符号端点使用同一 interval<num> 数学值语义；默认成员域为实数，整数端点不使区间成为整数范围。端点须满足 real 约束，构造上下文不隐式给符号添加实性；上例 upper 可为已证明实性的符号，而不必是具体数值

• 端点顺序未知时保留符号区间，代入后继续判定；已知倒置区间为空，同端点按开闭规则处理 [4]

• (a, b) 始终为元组，开区间使用 std.interval_open(a, b)

• 异量纲组合可使用静态元组；元组不因含数学元素而变为标量数学节点

8. 关系、逻辑与结构查询

==、!=、<、<=、>、>= 在适用的 num 上构造类型为 num 的数学关系，包括全数值操作数。实序关系必须满足实数等有序数域要求，不为任意复数提供顺序 [7]。

import std.cas

sym x
let a num = x > 0
let b num = x > 0 and x < 1
let c num = 1 > 0
let d bool = cas.same_structure(x, x)
let e = (x + 0) === x

• bool 上的 and、or、not 保持普通布尔规则及短路语义；关系上的对应操作构造数学逻辑表达式

• if、while 接受 bool 或数学关系；关系自动判真，仍未知时报 Inconclusive 或明确的未决条件错误，数字不作真假转换

• 普通控制流只执行已确定分支，不将分支副作用隐式符号化

• 数学 vector、matrix、set、interval 整体 ==、!= 构造 num 关系；逐元素比较使用适用的点运算符，结果元素是关系值，即 vector<num> 或 matrix<num> [1]

• 普通 bool、text、rule 及固定状态的相等仍返回 bool

• 普通 tuple、array、table 若提供布尔结构相等，其内部数学值递归使用结构比较，不调用构造关系的 ==

• === 与 std.cas.equivalent 返回 cas.Equivalent、cas.Different 或 cas.Unknown，不能将证明未决当作不等价 [3]

std.cas 的基础结构查询为：

func same_structure(a num, b num) -> bool

支持的容器可提供同名重载。比较数学节点种类、运算符或调用目标、参数个数及有序子节点；符号按名称比较。精确数字叶按数学数值比较，不依赖小整数、大整数、有理数或复数等内部表示。近似节点按表示值、近似类别、目标工作精度等语义结构区分，并与精确叶区别。

结构查询不进行代数证明、不受证明预算或 profile 影响。集合去重、哈希、规则和匹配必须递归使用同一结构相等关系，不得调用构造数学关系的 == 或有限证明 ===。数学结构不是源码文本：空白、注释、括号拼写和原文字面量形式不参与比较；比较的是求值及构造后已有的节点和顺序，不保证保留原源码的代数写法。

9. CAS 替换规则

rule 是内建不可变的替换规则类型。lhs => rhs 保存两个 num 数学值，由代入或重写接口显式应用。

• 构造时按先左后右的顺序各求值一次；应用时直接读取已保存值，不重新执行原表达式

• => 使用固定二元形式；a => b => c 为语法错误，以 rule 作为任一操作数为类型错误

• 规则可绑定名称、作为函数参数或返回值，也可存入 set<rule>

• 规则的 == 返回 bool：两侧分别结构相等时为 true，!= 为其取反

• set<rule> 按两侧结构相等去重；任何等价查询的预算不改变去重结果

• table{...} 中的 => 仍是表项键值分隔符，由表字面量语法解析

import std.cas

sym x, y
let replacement rule = x => 2
let replacements set<rule> = {replacement, y => 3, x => 2}

func replace(expr num, replacement rule) -> num {
    return cas.substitute(expr, replacement)
}

let a num = replace(x + 1, x => 2)

replacements 去重后保存 x => 2 与 y => 3。a 保存结构替换得到的 2 + 1，后续化简使用显式接口。

10. 代入

std.cas 导出以下普通函数：

func substitute(expr num, replacement rule) -> num
func substitute(expr num, replacements set<rule>) -> num

单条规则等价于单元素规则集合。代入按源码顺序对所有实参各求值一次，绑定并校验后再执行结构替换。

• 规则左侧与原表达式当前整棵子树做结构比较

• 命中时，以已保存的右侧作为该整棵子树的最终结果，结束这棵子树的处理；不再遍历插入值

• 未命中时，按子节点原顺序递归处理；每个原节点至多访问一次

• 集合内规则同时作用于原表达式，选择由当前子树与左侧的结构相等决定，不依赖集合枚举顺序

• 遍历前校验全部规则；相同左侧对应多个结构各异的右侧时诊断 ExprConflictingRules，即使冲突左侧没有出现在输入中也不能跳过

• 空规则集或无命中时返回原数学值；输入及规则在调用前后保持原值

• 输出保留结构替换产生的形态，不隐式数值化或代数化简；明确无定义或不支持的操作仍按错误契约处理

import std.cas

sym x, y
let a = cas.substitute(x + y, {x => y, y => 2})
let b = cas.substitute(x + 1, {(x + 1) => 9, x => 2})
let c = cas.substitute(x + y, {x => 3, y => 4})
let d = cas.substitute(x, {})

结果结构依次为 y + 2、9、3 + 4、x。cas.substitute(x, {x => 1, x => 2}) 报 ExprConflictingRules，不任意选择其中一条。

11. 数学模式匹配与重写

std.cas 导出以下普通函数。模式本身是 num 数学值，不是源码字符串或语法 token 模式。

func match_expr(expr num, pattern num, variables set<num>) -> table<text, num>?
func rewrite(expr num, replacement rule, variables set<num>) -> num

11.1 模式变量与匹配

• variables 显式列出 sym 产生的符号，每项必须出现在模式中，重写时必须出现在规则左侧

• 这些符号可捕获完整数学子树，其余符号按名称作字面结构匹配

• 同一变量重复出现时，各次捕获必须结构相等；捕获保存于结果表，不修改符号的原有绑定

• 其余节点按第 8 节递归比较；必须支持算术、幂及函数调用节点

• 比较既有数学节点顺序和数值语义，不检查源码文字，也不调用有限等价证明来猜测匹配

• 实参按源码顺序各求值一次，再检查类型、支持域及模式变量集合；非法变量集合诊断 ExprInvalidPatternVariables

match_expr 将整个输入与完整模式匹配一次：成功返回完整捕获表，键集合恰好对应所有模式变量名；变量集合为空且成功时返回空表；结构匹配失败返回 null。类型冲突、不支持节点及求值失败继续传播错误，不作为普通未匹配。

import std.cas

sym x, y, base, exponent, u
let pair = cas.symbolic_function("pair", 2)
let powers = cas.match_expr(x^2, base^exponent, {base, exponent})
let repeated = cas.match_expr(pair(x, x), pair(u, u), {u})
let different = cas.match_expr(pair(x, y), pair(u, u), {u})
let literal = cas.match_expr(y^2, x^2, {})
let exact = cas.match_expr(x^2, x^2, {})
let whole = cas.match_expr(x^2 + 1, base^exponent, {base, exponent})

powers 捕获 "base" 为 x、"exponent" 为 2；repeated 捕获 "u" 为 x；different、literal、whole 为 null；exact 为空捕获表。使用显式符号调用检查重复捕获，避免依赖加法构造是否已合并同类项。

11.2 捕获值重写

rewrite 先求值各实参一次并检查规则及模式变量，再基于原表达式安排一次左到右、子节点先于父节点的遍历。子节点完成后，用处理后的子节点组成当前节点，再匹配规则左侧。

• 命中时，以完整捕获表同时替换右侧的模式变量，所得数学值作为当前节点结果

• 右侧属于 variables 的符号使用捕获值，其余符号保持字面数学符号含义

• 使用规则已经保存的右侧；捕获值作为整体子树插入，保留内部结构

• 不再次遍历新插入的右侧或捕获子树；父节点仍可匹配包含子节点重写结果的结构

• 每个原节点只尝试一次，计划完成即返回；匹配失败保留当前节点及已处理子节点，无命中时返回原值

• 输入和规则保持原值；成功时返回完整结果，失败按普通错误路径传播，不返回伪装成成功的部分结果

import std.cas
use std.math.{sin, cos}

sym x, y, u
let a = cas.rewrite(sin(x), sin(u) => cos(u), {u})
let b = cas.rewrite(sin(x + 1), sin(u) => u^2, {u})
let c = cas.rewrite(sin(x), sin(u) => u + y, {u})
let d = cas.rewrite(sin(sin(x)), sin(u) => u + 1, {u})
let e = cas.rewrite(sin(x), sin(u) => sin(sin(u)), {u})

输出结构依次为 cos(x)、(x + 1)^2、x + y、(x + 1) + 1、sin(sin(x))。末例的插入结构不会再次重写。

12. 显式求值、近似与查询

求值不再表示从一种符号基本类型降级到数值类型。精确求值、保域化简和近似计算的结果都可以是 num，应由所调用接口明确区分行为：

• substitute 只执行第 10 节的结构代入

• std.cas.simplify 返回保域化简后的 num；std.cas.simplify_formal 显式采用声明支持的形式代数域，不承诺逐点保域 [3]

• std.math.approximate(value, precision=100) 显式请求目标十进制有效位数的近似值；precision int 必须是可具体求值的正整数 [6]

• same_structure 返回 bool；match_expr 返回捕获表或 null；=== 和 equivalent 返回固定三态 [3]

• 文本、具体机器数值或普通容器的提取必须通过声明相应目标返回类型和支持域的接口，不进行隐式真假或容器转换

import std.cas
use std.math.{approximate}

sym x
let expr num = x + 1/3
let exact num = cas.substitute(expr, x => 2)
let value num = approximate(exact, precision=100)

approximate 成功时按请求精度计算，但不保证正确舍入或认证误差界；误差估计和认证均为可选能力。近似操作数触发局部传播时，使用参与近似值的最高工作精度，未知符号部分继续保留；新精度不能恢复原输入信息。

近似标记和工作精度须保留，不能把显示小数精确化后当作原数学对象。精确与近似比较无损比较各自现有存储数值，不先舍入、不引入容差；结论仅关于表示值 [3]。

具体数值提取接口检查所需符号绑定、支持域和结果完整性，失败按接口契约诊断。普通数学运算不能仅因尚有未知符号而失败。求解接口证明解集为空时返回空 set<num>，不得把未决求解伪装为空集；匹配失败的 null、证明未决的 cas.Unknown 和运行时错误分别具有独立含义。

13. 错误

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

• ExprUnboundName：调用未绑定函数或变量，在任何期望类型上下文中均报错

• ExprTypeMismatch：数学操作收到不兼容基本类型，或试图把普通容器等隐式作为标量数学值

• ExprUnsupportedNode：显式 CAS 执行接口不支持对应数学节点

• ExprAmbiguousSyntax：调用、索引等形态不能由语法规则消歧

• ExprConflictingRules：同时代入具有相同左侧和不同右侧的规则

• ExprInvalidPatternVariables：模式变量的节点种类或出现位置违反第 11.1 节要求

• DomainError / InvalidArgument：确定违反数学定义域、参数或值约束

• Inconclusive：必须判定的条件或必须验证的约束仍未决

编译时能够确定的类型和语法错误必须直接诊断。运行时数学错误使用 LSR-018 的 MathError 与 raise，虚拟机故障沿同一规范的故障路径传播 [5]。错误名称可以映射到统一系统，但必须保留错误类别的独立语义；不得借助自动符号化吞掉普通调用错误。

14. 引用

[1] (1,2,3)

LSR-014 - 运算符规范 - 定义数学运算、关系、逻辑及普通调用

[2]

LSR-013 - 集合类型规范 - 定义 set<num>、解集及结构去重

[3] (1,2,3,4,5)

LSR-007 - 数学等价判定规范 - 定义三态证明、保域和形式代数入口

[4] (1,2)

LSR-017 - 区间类型规范 - 定义实数区间及符号端点

[5] (1,2)

LSR-018 - Never 底类型与 raise 终止效应规范 - 定义运行时数学错误及虚拟机故障传播

[6] (1,2)

LSR-004 - 标准库 - 定义 std.math.approximate 与 std.cas 接口

[7] (1,2)

LSR-010 - 虚数单位与复数规范 - 定义复标量、主值及顺序限制