Evaluation of reverse Polish notation

Question

We only consider the reverse Polish notation as an arithmetic expression.

Formally, RNP is a sequence consisted of numbers and arithmetic operators: $+,-,*,/$, and its syntax is: $$\newcommand\RNF{\mathrm{RNF}}\newcommand\num{\mathrm{number}}\newcommand\op{\mathrm{operator}}\RNF=\num\,\big\vert\,\RNF,\RNF,\op$$ and its value $$\newcommand\eval{\operatorname{eval}}\eval\num=\num$$ $$\eval\RNF_1,\RNF_2,\op=\eval\RNF_1\ \op\ \eval\RNF_2$$

The following pseudo code to evaluate $\eval\RNF$ is quoted from K&R:

while (next operator or operand isn't empty)
  if (it's a number)
    push it
  else if (it's an operator, say +,-,*,/)
    pop operands
    do operation
    push result

The algorithm is somewhat straightforward, but it's not as evident as considered. I found it difficult to formulate a loop invariant for the outer while-loop, and it's quite hard to prove the algorithm through Floyd-Hoare logic.

Through some search work, I found a related question, about the unambiguity of RPN. Unfortunately, I don't think the answer to that question is a rigorous proof.

Answer 1

How do you define the semantics of RPN? Ignoring the print commands, I would imagine a recursive definition that, given a sequence of operations, tells you what the state of the stack is like. From this definition it is straightforward to prove the correctness of the algorithm. In order to add prints, the recursive definition should also include the sequence of numbers printed. To add errors, the recursive definition should give either a pair as above or the error symbol.

Edit: Here is how you would formally define the semantics, which in the simplified case are a partial mapping from a sequence of operations to a sequence of numbers (the stack). It is only partial since sometimes arguments might be missing.

The function $F$ is defined as follows. First, $F(\lambda)=\lambda$, where $\lambda$ is the empty sequence. $F(\sigma,n) = F(\sigma),n$, where $\sigma$ is a sequence. If $F(\sigma) = \tau,a,b$ then $F(\sigma,+) = \tau,a+b$. If $|F(\sigma)| \leq 1$, then $F(\sigma,+)$ is undefined. Other arithmetic operations are handled in a similar fashion, only you need to make sure not to divide by zero.

Given the semantics, the proof of correctness is rather boring, and I'd rather not spell it out. The loop invariant is essentially the function $F$.