LARA

Translation Correctness for Expressions

Notation

Functions:

  • evaluation: $eval\ :\ Expression \to Int$
  • compilation: $[\![ \_ ]\!]\ :\ Expression \to List[Instruction]$
  • virtual machine: $run\ : \ List[Instruction] \to List[Int] \to List[Int]$

For simplicity we will omit environments mapping variables

  • does not affect this proof

We often write X instead of List(X) when X is one element

Also, we often use same symbol '*' for

  • operator in the tree
  • operator in instruction sequence
  • corresponding mathematical operator

Key Facts

Evaluation of expressions:

\begin{equation*}
   eval(e_1 * e_2) = eval(e_1) * eval(e_2)
\end{equation*}

Translation:

\begin{equation*}
   [\![ e_1 * e_2 ]\!] = [\![e_1]\!] ::: [\![e_2]\!] :::\ {*}
\end{equation*}

Here

  • the last occurrence of is the imul instruction
  • $e_1*e_2$ denotes a tree with node type $*$ and children $e_1$, $e_2$

run-virtual machine: From definition of $run$ and by induction on $L_1$,

\begin{equation*}
    run\ (L_1 ::: L_2)\ S = run\ L_2\ (run\ L_1\ S)
\end{equation*}

Of course

\begin{equation*}
    run\ (* ::: L)\ (S:::x_1:::x_2) = run\ L\ (S:::x)
\end{equation*}

where $x$ is the result of computing $x_1*x_2$, and

\begin{equation*}
    run\ (c ::: L)\ S = run\ L\ (S:::c)
\end{equation*}

for constant $c$, and

\begin{equation*}
    run\ EmptyList\ S = S
\end{equation*}

Correctness Theorem

For every $e$,

\begin{equation*}
   run\ [\![ e ]\!]\ List()\ \ =\ \ List(eval(e))
\end{equation*}

Attempt at Inductive Proof

Induction on structure of $e$

\begin{equation*}\begin{array}{l}
   run\ [\![e_1 * e_2]\!]\ S = \\
   run\ ([\![e_1]\!] ::: [\![e_2]\!] ::: *)\ S = \\
   run\ ([\![e_2]\!] ::: *)\ (run\ [\![e_1]\!]\ S) = \\
   ?
\end{array}\end{equation*}

Induction Hypothesis

For every expression $e$ and every list of integers $S$,

\begin{equation*}
   run\ [\![ e ]\!]\ S\ \ =\ \ S ::: eval(e)
\end{equation*}

Inductive Proof

\begin{equation*}\begin{array}{l}
   run\ [\![e_1 * e_2]\!]\ S = \\
   run\ ([\![e_1]\!] ::: [\![e_2]\!] ::: *)\ S = \\
   run\ ([\![e_2]\!] ::: *)\ (run\ [\![e_1]\!]\ S) = \\
   run\ ([\![e_2]\!] ::: *)\ (S ::: eval(e_1)) = \\
   run\ (*)\ (run\ [\![e_2]\!]\ (S ::: eval(e_1))) = \\
   run\ (*)\ (S ::: eval(e_1) ::: eval(e_2)) = \\
   S ::: (eval(e_1) * eval(e_2)) = \\
   S ::: eval(e_1 * e_2)
\end{array}\end{equation*}