算法 4 中的双栈算数表达式求值算法

[Higurashi]

《算法（第四版）》中介绍了 Dijkstra 双栈算术表达式求值算法：

public class Evaluate
{
    public static void main(String[] args)
    {
      Stack<String> ops  = new Stack<String>();
      Stack<Double> vals = new Stack<Double>();
      while (! StdIn.isEmpty())
      {  // 读取字符，如果是运算符则压入栈
          String s = StdIn.readString();
          if       (s.equals("("))                 ;
          else if (s.equals("+"))    ops.push(s);
          else if (s.equals("-"))    ops.push(s);
          else if (s.equals("*"))    ops.push(s);
          else if (s.equals("/"))    ops.push(s);
          else if (s.equals("sqrt")) ops.push(s);
          else if (s.equals(")"))
          {  // 如果字符为")"，弹出运算符和操作数，计算结果并压入栈
            String op = ops.pop();
            double v = vals.pop();
            if       (op.equals("+"))    v = vals.pop() + v;
            else if (op.equals("-"))    v = vals.pop() - v;
            else if (op.equals("*"))    v = vals.pop() * v;
            else if (op.equals("/"))    v = vals.pop() / v;
            else if (op.equals("sqrt")) v = Math.sqrt(v);
            vals.push(v);
          }  // 如果字符既非运算符也不是括号，将它作为 double 值压入栈
          else vals.push(Double.parseDouble(s));
      }
      StdOut.println(vals.pop());
    }
}

书中写道：

要证明它能够计算得到正确的值很简单：每当算法遇到一个被括号包围并由一个运算符和两个操作数组成的子表达式时，它都将运算符和操作数的计算结果压入操作数栈。这样的结果就好像在输入中用这个值代替了该子表达式，因此用这个值代替子表达式得到的结果和原表达式相同。我们可以反复应用这个规律并得到一个最终值。例如，用该算法计算以下表达式得到的结果都是相同的：

( 1 + ( ( 2 + 3 ) ＊ ( 4 ＊ 5 ) ) )
( 1 + ( 5 ＊ ( 4 ＊ 5 ) ) )
( 1 + ( 5 ＊ 20 ) )
( 1 + 100 )
101

我懂得它的意思，但总的来说，我觉得这种解释还是偏向于直观，并不算是一种严谨的证明（比较看重准确的人应该都能够理解这种情感）。所以我的问题是，如何真正证明它？或者至少是给出一个更加抽象的说明？

我尝试用循环不变式 /数学归纳法来证明，但没能理出一个清晰的思路。

如果可以的话，最好能够用偏数学的语言来说明，以避免歧义并趋于准确（当然，能够给出一个直观的解释以帮助理解也是很好的）。谢谢。

[GuuJiang]

假设全都是二元运算符(一元运算符的情况同理，你可以自行补充)

先定义辅助符号<==>，读作“在该算法意义下等价”
s1 <==> s2 表示对于表达式 s1 和 s2 应用上述算法得到的结果相等

第一步，先证明规约规则 1
X...<exp>...Y <==> X...eval(exp)...Y
其中 X 不包含左括号，sub 形如(<v1><op><v2>)，由入栈顺序可知，当碰到第一个右括号时，ops 的栈顶元素一定是 op ，vals 的栈顶元素一定是 v1 和 v2 ，根据算法实现，对 v1 和 v2 求值并重新入栈后，此时的栈状态、剩余表达式等和对右边的表达式应用算法时的状态是完全一致的，所以最终结果也是等价的
第二步，记 p(n)为含有 n 对括号的合法表达式，证明 p(n) <==> eval(p(n))，对 n 应用数学归纳法
1. 当 n=0 时，显然成立
2. 应用规约规则 1 可得 p(n+1) <==> p(n)

[Higurashi]

@GuuJiang #1 感谢回复。为了防止误解，我觉得我还是先问清楚几个问题比较好。

1. 这里的“规约规则”是不是指“归纳奠基”？
2. X...<exp>...Y <==> X...eval(exp)...Y 是什么意思？
3. eval(p(n)) 是指？

[GuuJiang]

@Higurashi
1. 规约规则就是字面上的意思，你可以理解为“把(1+1)变成 2”的这个过程，也就是这个算法主要在干的事
2. 表示由 X 、exp 和 Y 三部分组成的一个字符串，其中 X 不含左括号(自然也不含右括号)，exp 为一对括号包裹的最简表达式，Y 为剩余后缀，X 和 Y 可为空，这一段描述了这样一个事实“把一个表达式中的最左边一个右括号(由 X 中不含左括号来保证)及其匹配的左括号包含的这个表达式替换为该表达式的值，所得到的表达式对于该算法来说和原表达式是等价的”
举例说明的话就是一个形如 X(1+1)Y 的表达式等价于 X2Y
3. eval(s)表示 s 这个表达式的值，例如 eval("1+1")=2

[Higurashi]

@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)。
再次感谢。