@GuuJiang #3
我大概懂了，现在做一点总结。
假设全都是二元运算符（包括一元运算符的情况类似）。
定义辅助符号<==>，读作“在该算法意义下等价”。如 s1 <==> s2 表示对于表达式 s1 和 s2 应用上述算法得到的结果相等。
第一步：证 X exp Y <==> X eval(exp) Y ，exp 表示形如 (v1 op v2) 的由 v1 、op 、v2 组成的子表达式（ v1 、v2 、op 分别表示两个字面值和一个操作符），X 、Y 分别表示算数表达式除 exp 后的前面部分和后面部分，且 X 中不包含右括号，eval(exp) 表示算法对子表达式 exp 求值后的结果。
在算法遇到 exp 中的右括号时，算法将 exp 中的 v1 、v2 弹出进行计算得到 eval(exp) 并将其入栈，因为 X 中不包含右括号，所以，算法解析 X eval(exp) Y 至 eval(exp) 入栈时，其结果与算法解析 X exp Y 至将 exp 求值后完全相同，所以 X exp Y <==> X eval(exp) Y 。
第二步：记 p(n) 为含有 n 对括号的合法表达式、p(n-1) 为算法对 p(n) 求值时遇到第一个右括号后出栈求解再入栈得到的新表达式（注意到此时括号会减少一对），由第一步的证明有 p(n) <==> p(n-1) <==> p(n-2) ... <==> p(1) <==> p(0)，不难知道算法能够正确处理不包括括号（只包含一个字面值）的 p(0)，所以算法能够正确处理 p(n)。
再次感谢。