是否存在判定AST形式算术函数单射性的算法？
首先得把单射的定义掰扯清楚：对单变量函数来说，只要输入不同输出就一定不同；对多变量函数，得看是单输出还是多输出——这俩的判定逻辑差得老远了，咱们分开说。
先搞定单变量的情况
你已经能把表达式转成AST了，那接下来的核心就是遍历AST做化简+单调性分析：
第一步：先给AST“瘦个身”
很多冗余运算会干扰判断，比如把x + 0直接换成x，x * 1换成x，x + (-x)换成0，x/x（x≠0）换成1。这一步能把很多复杂的AST简化成一眼就能看懂的形式，比如x + x/x化简后就是x + 1，一眼就知道是单射。
第二步：拆分定义域
算术函数里有除法的话，得先把分母为0的点去掉，把定义域拆成几个连续的区间（比如1/x的定义域是(-∞,0)和(0,+∞)两个区间）。
第三步：分析每个区间的单调性
对化简后的AST求导（用AST遍历的方式求导，比如加法节点的导数是左右子节点导数相加，乘法节点用乘积法则），然后判断导数在区间内是不是恒正或者恒负：
- 如果导数恒正，函数在这个区间严格递增；恒负则严格递减。
- 还要检查不同区间的函数值范围有没有重叠：比如
1/x在(-∞,0)的值域是(-∞,0)，在(0,+∞)的值域是(0,+∞)，完全不重叠，所以整个定义域内是单射；但x²在(-∞,0)递减，(0,+∞)递增，值域都是[0,+∞)，重叠了，所以不是单射。
举几个例子：
x + 1：导数是1（恒正），整个定义域严格递增，是单射。x/x：化简后是常数1，不管输入啥（x≠0）输出都一样，不是单射。x + x/x：化简后是x+1，和第一个例子一样，是单射。
再来说多输入的情况
这里得分两种场景，差别特别大：
场景1：多输入单输出的函数
先给你泼个冷水：只要输入变量个数≥2，这类函数几乎不可能是单射——除非它本质上只依赖一个变量（比如f(x,y)=x，这其实就是单变量函数）。为啥？因为你总能找到不同的输入组合得到相同的输出：
- 比如
f(x,y)=x+y，(1,2)和(2,1)输出都是3； - 比如
f(x,y)=x*y，(2,3)和(3,2)输出都是6； - 哪怕是看起来“独特”的
f(x,y)=x + πy，你取(0,1)和(π,0)，输出都是π，输入不同但输出相同。
所以如果你的多输入函数是单输出，先检查它是不是只依赖一个变量——是的话按单变量方法处理，不是的话直接判定为非单射。
场景2：多输入多输出的函数（n输入对应n输出）
这种情况才有可能是单射，核心思路是雅可比矩阵分析：
- 求偏导数构建雅可比矩阵：对每个输出函数，分别对每个输入变量求偏导（用AST遍历的方式，求偏导时把其他变量当常数处理），把这些偏导数排成一个n×n的矩阵。
- 计算雅可比行列式：把行列式展开成一个算术函数（AST形式），然后化简这个行列式的AST。
- 判断行列式是否恒不为0：
- 如果行列式是常数0，那函数肯定不是单射；
- 如果行列式不是常数0，还要检查它在定义域内有没有零点（比如找分子的根，同时排除分母为0的点）。如果行列式在整个定义域内都不为0，那函数在每个连通的定义域分支上是局部单射；要是再能确认函数是满射（或者没有不同输入映射到同一输出），那就是全局单射。
举个例子：f(x,y)=(x+y, x-y)，雅可比矩阵是[[1,1],[1,-1]]，行列式是-2（恒不为0），所以这个函数是单射（其实是双射）。
实现时的关键细节
不管是单变量还是多变量，AST遍历的核心都是节点类型的针对性处理：
- 常数节点：直接返回数值，方便化简；
- 变量节点：记录变量名，用于求导/偏导；
- 加减乘除节点：递归处理左右子节点，先化简再做后续分析。
另外，符号分析是单调性/行列式判断的关键——比如判断导数是否恒正，可以通过找导数的零点，然后在每个区间取测试点看符号；判断行列式是否恒不为0，就是看它的分子有没有根（有理函数的情况）。
内容的提问来源于stack exchange，提问作者Robin Davis
