tutorial. 多变量函数与正则性[math-0008]

◆:function构造函数引用并附上两个标量输入、一个标量输出的签名。它没有定义f的实现。c2(f)声明二阶连续可微；它是计算前提，不是从名字自动推断的事实。

对x求偏导，结果是 ${\partial }_1\left(f(x,y)\right)$。

结果保留f在第一个参数槽的符号偏导。系统知道外层表达式如何求导，却不知道f的具体数值函数。若参数本身是复合表达式，链式法则会同时计算该参数的导数。

$2x\times {\partial }_1\left(f(x^2,y)\right)$

该结果包含2*x的链式因子。两个调用位置即使传入相同变量，也作为不同参数槽处理；这来自函数应用的结构，不是字符串替换。

不同计算需要不同阶数的可微性。一次求导通常需要differentiable；连续交换混合二阶偏导需要C2。下面展示在缺少C2时计算会留下诊断：

这里的报告状态会指出尚缺的正则性事实。文档使用show才能继续把失败当作示例展示；正常构建仍会拒绝无效推导。

一个独立参数不能随坐标变化。涉及分母时还需要非零事实：

$x^2$

参数声明表达a对坐标保持不变；nonzero(a)才授权约去分母。缺少后者时，简化器不会冒险把a/a改成1。

未知函数可以显示，也可以保留符号偏导；它不会被假装成有限多项式。多项式积分pass会拒绝它，而关系式计算会在有对应规则和前提时继续处理。失败类型告诉作者缺的是输入定义、正则性前提还是算法规则。

有限规则也可以作为逻辑关系查询，参见用miniKanren查询数学规则。