tutorial. 从向量场计算Cartesian算子[math-0004]

空间计算依赖坐标的类型、顺序和正则性。Grove不会从向量箭头猜这些信息；作者显式构造空间、分量和前提，计算器才展开算子。

声明有序Cartesian空间[#93]

这里◆:space的三个参数定义有序坐标；◆:components需要三个Semantic标量值和对应空间。v是具体向量场(x²,y,z)，不是排版用的列向量。

其Semantic term是：

(components (^ (var x) (num "2")) (var y) (var z))

有序空间作为值的requirement携带。它不会因为被写入v就自动启用；下面的计算显式把r3放入假设列表。

example. 计算空间算子[#94]

  • grad of x²+y²+z²: (2x2y2z)
  • div of (x²,y,z): 2x+2
  • Laplacian of x²+y²+z²: 6

结果分别是(2x,2y,2z)、2x+2、以及6。算子先展开成坐标偏导，再由标量规则计算。分量求值并没有通过预设答案替换。

counterexample. 结果为什么要求differentiable[#95]

梯度、散度和旋度至少需要一阶导数；Laplacian需要二阶正则性。坐标空间提供独立坐标事实，但场是否可微仍需作者声明。以下故意缺少所需条件：

(1)Δ(x2+y2+z2)=6

Derivation (71 steps)[#96]

Components

(1)Δ(x2+y2+z2)=∇·(∇(x2+y2+z2))Laplacian Scalar Components=∇·((∂∂x(x2+y2+z2)∂∂y(x2+y2+z2)∂∂z(x2+y2+z2)))Gradient Components=∂∂x(∂∂x(x2+y2+z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Divergence Components

Partial

(2)∂∂x(∂∂x(x2+y2+z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))=∂∂x(∂∂x(x2+y2)+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Sum=∂∂x(∂∂x(x2)+∂∂x(y2)+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Sum=∂∂x(2x1×∂∂x(x)+∂∂x(y2)+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Power rule=∂∂x(2x×∂∂x(x)+∂∂x(y2)+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Power One=∂∂x(2x×1+∂∂x(y2)+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Variable=∂∂x(2x+∂∂x(y2)+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Multiply One=∂∂x(2x+2y1×∂∂x(y)+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Power rule=∂∂x(2x+2y×∂∂x(y)+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Power One=∂∂x(2x+2y×0+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Independent=∂∂x(2x+0+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Multiply Zero=∂∂x(2x+∂∂x(z2))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Add Zero=∂∂x(2x+2z1×∂∂x(z))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Power rule=∂∂x(2x+2z×∂∂x(z))+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Power One=∂∂x(2x+2z×0)+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Independent=∂∂x(2x+0)+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Multiply Zero=∂∂x(2x)+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Add Zero=∂∂x(2)×x+2∂∂x(x)+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Product rule=0x+2∂∂x(x)+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Constant=0+2∂∂x(x)+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Zero Multiply=0+2×1+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Variable=0+2+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Multiply One=2+∂∂y(∂∂y(x2+y2+z2))+∂∂z(∂∂z(x2+y2+z2))Zero Add=2+∂∂y(∂∂y(x2+y2)+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Sum=2+∂∂y(∂∂y(x2)+∂∂y(y2)+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Sum=2+∂∂y(2x1×∂∂y(x)+∂∂y(y2)+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Power rule=2+∂∂y(2x×∂∂y(x)+∂∂y(y2)+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Power One=2+∂∂y(2x×0+∂∂y(y2)+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Independent=2+∂∂y(0+∂∂y(y2)+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Multiply Zero=2+∂∂y(0+2y1×∂∂y(y)+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Power rule=2+∂∂y(0+2y×∂∂y(y)+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Power One=2+∂∂y(0+2y×1+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Differentiate Variable=2+∂∂y(0+2y+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Multiply One=2+∂∂y(2y+∂∂y(z2))+∂∂z(∂∂z(x2+y2+z2))Zero Add=2+∂∂y(2y+2z1×∂∂y(z))+∂∂z(∂∂z(x2+y2+z2))Power rule=2+∂∂y(2y+2z×∂∂y(z))+∂∂z(∂∂z(x2+y2+z2))Power One=2+∂∂y(2y+2z×0)+∂∂z(∂∂z(x2+y2+z2))Differentiate Independent=2+∂∂y(2y+0)+∂∂z(∂∂z(x2+y2+z2))Multiply Zero=2+∂∂y(2y)+∂∂z(∂∂z(x2+y2+z2))Add Zero=2+∂∂y(2)×y+2∂∂y(y)+∂∂z(∂∂z(x2+y2+z2))Product rule=2+0y+2∂∂y(y)+∂∂z(∂∂z(x2+y2+z2))Differentiate Constant=2+0+2∂∂y(y)+∂∂z(∂∂z(x2+y2+z2))Zero Multiply=2+0+2×1+∂∂z(∂∂z(x2+y2+z2))Differentiate Variable=2+0+2+∂∂z(∂∂z(x2+y2+z2))Multiply One=2+2+∂∂z(∂∂z(x2+y2+z2))Zero Add=4+∂∂z(∂∂z(x2+y2+z2))Evaluate Constant=4+∂∂z(∂∂z(x2+y2)+∂∂z(z2))Differentiate Sum=4+∂∂z(∂∂z(x2)+∂∂z(y2)+∂∂z(z2))Differentiate Sum=4+∂∂z(2x1×∂∂z(x)+∂∂z(y2)+∂∂z(z2))Power rule=4+∂∂z(2x×∂∂z(x)+∂∂z(y2)+∂∂z(z2))Power One=4+∂∂z(2x×0+∂∂z(y2)+∂∂z(z2))Differentiate Independent=4+∂∂z(0+∂∂z(y2)+∂∂z(z2))Multiply Zero=4+∂∂z(0+2y1×∂∂z(y)+∂∂z(z2))Power rule=4+∂∂z(0+2y×∂∂z(y)+∂∂z(z2))Power One=4+∂∂z(0+2y×0+∂∂z(z2))Differentiate Independent=4+∂∂z(0+0+∂∂z(z2))Multiply Zero=4+∂∂z(0+∂∂z(z2))Add Zero=4+∂∂z(0+2z1×∂∂z(z))Power rule=4+∂∂z(0+2z×∂∂z(z))Power One=4+∂∂z(0+2z×1)Differentiate Variable=4+∂∂z(0+2z)Multiply One=4+∂∂z(2z)Zero Add=4+∂∂z(2)×z+2∂∂z(z)Product rule=4+0z+2∂∂z(z)Differentiate Constant=4+0+2∂∂z(z)Zero Multiply=4+0+2×1Differentiate Variable=4+0+2Multiply One=4+2Zero Add=6Evaluate Constant

Simplify

(3)6

诊断说明缺失前提或不完整的坐标声明。on-error让此处把失败作为教材内容展示。

向量排版和向量语义[#97]

Notation的列布局只表达怎么显示：

(1)(a+bcd)

Semantic的components则表达一个恰有三个标量分量、依赖特定有序空间的向量对象。列布局可以包含任意内容，但不能用于math-compute；Semantic向量可以参与加法、数乘、点积和叉积。

检查计算证书[#98]

curl/grad 类空间计算都会保留可重放证书。当前散度计算 replay：#t

独立重放检查每个rewrite edge；测试套件另有独立的精确多项式解释器，用来避免只用生产规则验证生产规则。

remark. 范围[#99]

这里实现的是欧氏Cartesian坐标。将名字换成r,θ,z不会自动得到柱坐标度量；一般曲线坐标、联络和边界条件都需要不同的语义与算法。

向量表示细节见分量与显式偏导；运算过程可沿计算追踪查看pass、规则路径和证书。多项式积分与Poisson特解展示另一类多项式运算。