index. Grove数学语言:表示、计算与核验[math]
数学页面把输入语法、运算对象和排版结果分开表示。Formula读取公式文本;Semantic保存可计算的结构及其条件;Notation描述数学输出。Scheme连接这些表示,执行明确的计算步骤,并保留来源与诊断。
表示与执行[#132]
- Formula、Semantic与Notation:三种表示各自承担什么职责。
- 在Scheme中执行数学计算:构造IR、运行pipeline并读取计算结果。
推导与微分算子[#133]
- 推导、搜索与独立核验:对推导链求导、搜索目标并独立重放。
- 从向量场计算Cartesian算子:从分量构造grad、div、curl与Laplacian。
- 向量分量与显式偏导:检查向量值、坐标分量及偏导项。
- Cartesian算子的计算追踪:查看pass、规则路径和证书。
多项式与一般函数[#134]
- 多项式积分与Poisson特解:用专用多项式表示计算积分与特解。
- 多变量函数与正则性:处理符号偏导、链式法则与参数。
以关系组织数学知识[#135]
- 用miniKanren查询规则:将规则与目录事实组合为关系查询。
- 查询没有入向引用的页面:以同一查询机制检查项目中的孤立树。
- 关系查询参考:DSL、规则目录与项目谓词的速查。