# Evaluation of reverse Polish notation

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


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.

-

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$.

-
It's only a sequence of $+,-,\times,/$ and numbers. –  Frank Science Feb 23 '13 at 5:03
That's the syntax, not the semantics. –  Yuval Filmus Feb 23 '13 at 5:05
Sorry, it's just the arithmetic result. I've just kicked out the excess stones, say errors. Now I want to clarify the semantics. Since I'm unfamiliar with these theories, I hope you can help me to check whether the edited question is complete. –  Frank Science Feb 23 '13 at 5:11
If you don't know what you want to prove, naturally you can't prove it. Why are you interested in this in the first place? Personally, I find it obvious that the algorithm "works", and I find the exercise of formally formulating the semantics and doing the straightforward proof quite pointless. –  Yuval Filmus Feb 23 '13 at 5:25
I think it's okay now. I think the algorithm is not evident since it uses a stack to emulate the calculation, not just calculate the RNF recursively. I want to prove an algorithm, not thoroughly rigorously just as in Hoare logic, but partly rigorously. For example, we should point out the loop invariant. –  Frank Science Feb 23 '13 at 5:30